Graph Classes of Bonded Shrubdepth

粘合灌木深度的图形类别

• 批准号: 420419861
• 负责人: Dr. Roman Rabinovich
• 金额: --
• 依托单位: Fachgebiet Logik und Semantik
• 依托单位国家: 德国
• 项目类别: Research Fellowships
• 财政年份: 2018
• 资助国家: 德国
• 起止时间: 2017-12-31 至 2018-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/420419861?language=en
• 关键词: Graph; Classes; Bonded; Shrubdepth

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.

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