Graph Classes of Bonded Shrubdepth

计算机科学的一项重要任务是自动验证系统的性质。系统可以是一台复杂的安全关键机器，也可以是飞机或原子工厂等建筑，也可以是城镇地图、软件或硬件。属性可以是，例如，在原子能工厂发生不想要的情况的风险低于某一概率。另一个例子是，一个城镇可以设置3个消防站，这样消防员最多可以通过5个其他地方到达镇上的任何地方。为了自动验证这些属性，必须对系统和属性进行正规化。计算机科学中系统的一种流行的形式主义是图，其元素被称为顶点。在图中，一些顶点由线成对连接，称为边。在形式化图性质的各种方法中，经典的方法是通过逻辑公式。公式是根据特定规则构建的字符序列，逻辑是所有这些公式的集合。例如，公式可以表示关于我们上面描述的消防站的性质(称为支配集)。一阶逻辑(FO)是一种流行的逻辑，它可以表示所有所谓的局部性质，如支配集。虽然有一个简单的蛮力算法可以测试每个图上的每一个FO性质，但它的性能超出了任何实际应用。对于一个小公式来说，在一个不太大的图上，它的运行时间会比大爆炸以来经过的时间还要长。问题是，它的运行时间按指数依赖于输入的大小，而至少多项式时间被认为是有效的。此外，有理论结果表明，多项式算法的存在是不可能的。解决这个问题的一个方法是改进我们的效率概念。其想法是，通常情况下，图表很大，公式很小。然而，即使考虑到公式的大小是恒定的，我们最终也会得到太大的运行时间，例如图的大小与公式大小的幂。我们的目标是开发一种算法，其运行时间是公式大小中的某个函数乘以结构的大小，而在我们的设置中，结构的大小要小得多，但由于复杂的理论限制，即使是这个目标似乎也无法实现。理论计算机科学中的一种既定方法是将我们自己限制在仍然经常出现在实践中的图子类上。一长串的研究确定了非常丰富的稀疏图类，允许有效地检查由FO公式表示的性质。稀疏图是指结构上只包含(或多或少)线性边数而不是顶点数的图。我们想将这些结果推广到稠密图。其思想是在稠密图中找到稀疏的内部结构，并将方法从稀疏情况推广到稠密图。初步结果让我们相信，灌木层深度是正确的概念。

An important task of computer science is automatic verification of properties of systems. A system can be a complex and security critical machine or construction as an airplane or an atomic plant, a map of a town, a piece of software or hardware. A property can be, e.g., that the risk of an unwanted situation at an atomic plant is below a certain probability. Another example is that 3 fire stations can be placed in a town so that the firefighters can reach any place in the town by passing at most 5 other places.In order to automatically verify such properties, the systems and the properties must be formalised. A popular formalism for systems in computer science are graphs whose elements are called vertices. In a graph, some vertices are pairwise connected by lines, called edges. Among various ways to formalise properties of graphs, a classical one is by formulae of a logic. A formula is a sequence of characters built up according to certain rules and a logic is the set of all such formulae. A formula can express, e.g., the property (called dominating set) about the fire stations that we described above. A popular logic is the first-order logic (FO), which can express all so-called local properties like dominating set.While there is a simple brute-force algorithm that can test every FO property on every graph, its performance is beyond any practical application. On a not too big graph for a small formula its running time would be more than the time passed since the Big Bang. The problem is that it running time depends on the size of the input exponentially while at least polynomial time is considered as efficient. Moreover, there are theoretical results implying that the existence of a polynomial algorithm is improbable.One way to cope with this problem is to refine our notion of efficiency. The idea is that typically the graph is big and the formula is small. However, even considering the size of the formula as constant we end up with too big running times such as the size of the graph to the power of the size of the formula. Our goal is to develop an algorithm whose running time is some function in the formula size times the size of the structure which is much smaller in our setting.Still even this goal seems to be unreachable due to complexity theoretical constraints. An established way in theoretical computer science is to restrict ourself to subclasses of graphs that still often appear in practice. A long line of research identified very rich sparse classes of graphs that allow an efficient checking of properties expressed by FO formulae. Sparse graphs are those which structurally contain only a (more or less) linear number of edges compared to the number of vertices.We want to extend those results to dense graphs. The idea is to find a sparse internal structure in a dense graph and to generalise methods from the sparse case to dense graphs. Preliminary results let us believe that the right notion for this is Shrub-depth.