Graph Classes of Bonded Shrubdepth

• Applicant: Dr. Roman Rabinovich
• Subject Area: Theoretical Computer Science ; Mathematics
• Term: from 2018 to 2019
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 420419861

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.

• DFG Programme: Research Fellowships
• International Connection: France
• Host: Professor Dr. Patrice Ossona de Mendez