# Algorithmic Model Theory

## Model Constructions and Model-Theoretic Games in Special Classes of Structures

This is also the title of a DFG-funded research project, which emphasises the close relationship between the model theory of well-behaved classes of structures, combinatorial techniques for model constructions within these classes, and the manageability of Ehrenfeucht-Fraisse techniques. Among the key aspects of the game-based model-theoretic analysis are locality phenomena in the spirit of Gaifman’s locality theorem. But certain mechanisms for the hierarchical analysis of suitable structures can facilitate the modular analysis of strategies in Ehrenfeucht-Fraisse games even in cases where Gaifman locality itself fails, for instance because Gaifman distance induces a trivial metric. Considerable progress in this direction has been achieved in the work of Alexander Kartzow with extensions of Ehrenfeucht-Fraisse techniques to certain classes of complex configuration graphs, to which Gaifman locality as such does not apply. Another breakthrough in the game-based analysis of definability issues concerns an affirmative solution to the question whether the guarded fragment of first-order logic captures all first-order properties that are invariant under guarded bisimulation equivalence over the class of all finite structures [O10], which had long been open. Here as in [BGO10], finite model constructions and transformations allow us to reduce key issues to finite relational structures that display limited forms of hypergraph acyclicity. Two entirely different routes to the construction of finite bisimilar covers with very different acyclicity constraints in [O10] and in [BGO10] have thus led to a whole range of far-reaching results in the finite model theory of guarded logics. Ongoing research focusses on constructions and applications of hypergraph coverings, e.g., in the model theory of modal and guarded logics. The wider theme is persued in a new DFG project: |

## Construction and Analysis in Hypergraphs of Controlled Acyclicity

DFG project (2013-2018). Acyclicity conditions play an important role as tractability criteria in various settings of logic in computer science and of algorithmic model theory. Often, ideal forms of acyclicity are available through a process of unfolding (e.g., of transition systems or game graphs into trees). Fully acyclic unfoldings are, however, typically unavailable in settings where only finite structures are admissible. For such applications, especially in the realm of finite model theory, the focus must therefore be on suitable relaxations of full acyclicity that can be realised in finitary coverings (partial unfoldings), and methods that make available in these relaxed scenarios the good algorithmic aand model-theoretic properties that are familiar from fully acyclic unfoldings. The new project puts the development of constructions and methods at the center, with a view to a more systematic understanding and to extending the reach of corresponding model-theoretic techniques to further application domains. At the level of basic research the project is geared to draw on logical and model-theoretic methods as well as on new connections with techniques from discrete mathematics (e.g., permutation groups, the combinatorics of graphs and hypergraphs, discrete geometry, combinatorial and algebraic methods). |

## Bibliography

[O10]M. Otto.Highly acyclic groups, hypergraph covers and the guarded fragment, preprint, 2010, 42 pages. Journal version of LICS 2010 paper, JACM, 59:1, 2012. Abstract [BGO10] V. Barany, G. Gottlob and M. Otto. Querying the Guarded Fragment, Proceedings of Logic in Computer Science, LICS 2010 Abstract BibTeX entry |

## Model Checking on Generalisations of Pushdown Graphs

Ramifications of tools for Ehrenfeucht-Fraisse game analysis and structural analysis can be combined to show decidability of the FO model checking problem over structurally rich classes of infinite graphs generated by restricted computational models. The computational source of these graph classes makes them interesting from the point of view of model checking applications and offers a degree of controllability (e.g., by certain generalised pumping arguments). Alexander Kartzow’s work explores techniques for a modular analysis of Ehrenfeucht-Fraisse games similar to those familiar from Gaifman’s theorem for certain classes of configuration graphs (nested pushdown trees/collapsible pushdown graphs) where Gaifman locality does not apply. These classes are interesting from a model-theoretic perspective. They are the only known natural classes with uniformly decidable modal mu-caluclus theories which contain graphs with undecidable monadic second-order theories. Decidability of the FO model checking for nested pushdown trees (classically: uniform decidability of their FO theories) is shown in [K09], both through such adaptations of a quasi-local Ehrenfeucht-Fraisse analysis, and through model theoretic interpretations and tree-automaticity. The latter approach extends to second-order collapsible pushdown graphs as shown in [K10a]. A new hierarchy of higher-order nested pushdown trees, which may be seen as a sub-hierarchy of that of collapsible pushdown graphs, offers further applications of the quasi-local approach; decidability of FO model checking for level 2 nested pushdown trees is established in [K10b]. Technically this result relies on the application of pumping techniques for level 2 pushdown graphs in the Ehrenfeucht-Fraisse analysis of nested pushdown trees (of level 2). Bibliography[K09] A. Kartzow FO Model Checking on Nested Pushdown Trees [PDF with Appendix], Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009 BibTex entry [K10a] A. Kartzow, Collapsible Pushdown Graphs of Level 2 are Tree-Automatic [PS with appendix], 27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010 BibTex entry [K10b] PhD – Thesis: A. Kartzow First-Order Model Checking on Generalisations of Pushdown Graphs, Submitted to the Fachbereich Mathematik at Technische Universität Darmstadt in December 2010 |

## Acyclicity in Hypergraphs and Relational Structures

Acyclicity criteria have long been recognised as a natural condition that guarantees tractability, for instance for query evaluation (see [BFMY83] for a seminal paper). Since a hypergraph is acyclic if, and only if, it is tree-decomposable, there is also an obvious connection with tree representations through model-theoretic interpretations in trees. Bounded treewidth and various generalisations have been extensively explored as criteria for tractability in model checking. From a hypergraph theoretic point of view, the natural notion of hypergraph bisimulation poses the problem which degree of hypergraph acyclicity can be achieved in finite bisimilar coverings of finite hypergraphs – just as in the graph case, outright acyclicity can usually only be achieved in infinite coverings. But while finite graphs always admit even polynomially bounded finite bisimilar covers that are locally acyclic [O04], local acyclicity is not in general achievable in finite hypergraphs coverings. The new cover construction in [O10] provides finite hypergraph covers in which evry small induced sub-hypergraph is acyclic. That construction is based on a new idea for the construction of Cayley groups that avoid not just short cycles in the usual sense but even cycles that – irrespective of their length – make only few nontrivial transitions between distinct subsets of generators. Model constructions involving these groups were applied to the finite model theory of the guarded fragment in [O10]. Earlier hypergraph coverings constructed in [HO03] had achieved conformality in finite covers, while [O09] provided another, weaker degree of size-bounded acyclicity in the sense that any small cyclic configurations in the cover would be tree-decomposable in projection to the base. This latter notion of coverings has been perfected in a new construction of feasible complexity in [BGO10], with important applications to the algorithmic model theory of guarded logics (see here). The structure theory of the resulting classes of hypergraphs and relational structures of controlled acyclicity is an interesting field for further study – interesting both from the point of view of discrete mathematics and algorithmic model theory. Further research questions concern the possibly of more uniform variants of the construction in [O10] (holding a promise of new model-theoretic applications in the spirit of those explored in [HO03]) as well as the application of the existing construction to the algorithmic and finite model theory of various candidate logics in the vicinity of modal and guarded logics. Bibliography[BFMY83] Catriel Beeri, Ronald Fagin, David Maier, Mihalis Yannakakis: On the Desirability of Acyclic Database Schemes J. ACM 30(3): 479-513 (1983) [O04] M. Otto, Modal and Guarded Characterisation Theorems over Finite Transition Systems, Annals of Pure and Applied Logic, volume 130, 2004, pp.~173-205. Abstract BibTeX entry [O10]M. Otto.Highly acyclic groups, hypergraph covers and the guarded fragment, preprint, 2010, 42 pages. Journal version of LICS 2010 paper, invited for JACM, December 2010. Abstract [HO03] I. Hodkinson and M. Otto, Finite Conformal Hypergraph Covers and Gaifman Cliques in Finite Structures, Bulletin of Symbolic Logic, volume 9, 2003, pp. 387-405. Abstract BibTeX entry [O09] M. Otto, Avoiding incidental homomorphisms into guarded covers, Technical Report no. 2600, TU Darmstadt, 2009 [BGO10] V. Barany, G. Gottlob and M. Otto. Querying the Guarded Fragment, Proceedings of Logic in Computer Science, LICS 2010 Abstract BibTeX entry |

## Finite Model Theory of Guarded Logics

The generalised tree-model property of the guarded fragment [G99] explains some of the good algorithmic model-theoretic properties of the guarded fragment and some of its extensions. In light of the above, this crucial feature of guarded logics should be called acyclic model property, because a guarded tree-unfolding always yields a guarded bisimilar model whose hypergraph of guarded sets is acyclic. The obvious analogy here is that with the tree model property of basic modal logic: bisimilar tree unfoldings yielding models based on acyclic graphs (i.e., actual trees rather than tree-like relational structures, or acyclic graphs rather than acyclic hypergraphs). This analogy does not carry over easily to the finite model theory of modal and guarded logics, though: while basic modal logic even has the finite tree-model property, for the guarded fragment there cannot be any straightforward finite model analogue of its acyclic model property (see here). Characterisation theorem (fmt) Finite cover constructions and the analysis of guarded bisimulation and first-order Ehrenfeucht–Fraisse games have confirmed the long-standing conjecture that the guarded fragment GF is expressively complete for the class of all first-order properties of finite structures that are compatible with guarded bisimulation equivalence [O10] (the fmt analogue of the Andreka–van Benthem–Nemeti charaterisation). Finite model properties and small models An elegant proof of the finite model property for the guarded fragment GF in [G99] was extended to the clique guarded fragment CGF in [HO03] using conformal finite hypergraph covers; the same argument proved the Hrushovski–Herwig–Lascar style extension property for partial automorphisms (EPPA) for the class of conformal finite relational structures and, e.g., for the class of Ck-free graphs. Substantial extensions of the finite model property for GF were achieved in [BGO10] and [O10]. The weakly acyclic covers in [BGO10] show that GF has the finite model property also in restriction to any class defined in terms of forbidden homomorphic images of finitely many configurations – and thus shows that conjunctive queries are finitely controllable in the presence of guarded constraints. The acyclic covers of [O10] show that GF even has the finite model property in restriction to any class defined in terms of finitely many forbidden cyclic configurations. This is a strong results for the finite model theory of GF since infinite fully acyclic models can always be obtained by the abovementioned acyclic model property. Other key results of [BGO10] provide rather tight, feasible bounds on the size of small models for GF and CGF. Descriptive complexity A polynomial time canonisation procedure for finite relational structures up to guarded bisimulation equivalence in [BGO10] implies that there is a logic for the class of all guarded bisimulation closed PTime properties of finite structures, a positive solution to the fundamental problem of capturing Ptime in the guarded world. Bibliography[G99] E. Grädel. On the restraining power of guards. Journal of Symbolic Logic, vol. 64, pp. 1719–1742, 1999. [O10]M. Otto.Highly acyclic groups, hypergraph covers and the guarded fragment, preprint, 2010, 42 pages. Journal version of LICS 2010 paper, invited for JACM, December 2010. Abstract [HO03] I. Hodkinson and M. Otto, Finite Conformal Hypergraph Covers and Gaifman Cliques in Finite Structures, Bulletin of Symbolic Logic, volume 9, 2003, pp. 387-405. Abstract BibTeX entry [BGO10] V. Barany, G. Gottlob and M. Otto. Querying the Guarded Fragment, Proceedings of Logic in Computer Science, LICS 2010 Abstract BibTeX entry |

## Model Theory of Modal Logics over Special Frames

Modal logics occur as restricted fragments of first-order logic that combine very good model theoretic and algorithmic properties with an expressiveness that ideally suits typical applications in, for instance, knowledge representation, temporal specification, analysis of multi-agent systems and games [GO06]. It would often be natural to consider classes of structures with special requirements on the underlying frames, which cannot be dealt with easily unless the relevant constraints are first-order definable. Examples of interesting non-elementary frame classes include the class of finite frames or classes of rooted transitive frames. Expressive completeness of suitable modal logics for the class of all bisimulation invariant first-order properties relative to such restricted classes can be shown with specially adapted techniques that combine the analysis of the bisimulation game with bisimulation respecting model transformations. In [DO09], we develop a variety of new results along these lines. Among these is the emergence of a novel modality that is necessary for expressive completeness over transitive frames without strict infinite paths but not bisimulation safe over the class of all frames. Further generalisations of the proof techniques used here show that over various classes of transitive frames without infinite strict paths, monadic second-order logic is no more expressive than first-order logic as far as bisimulation invariant properties are concerned. These results lead to ramifications of a classical theorem of de Jongh and Sambin in modal logic. [O04, DO05]. Model Theory of Modal Logics over Special Frames Bibliography[GO06] V. Goranko and M. Otto, Model Theory of Modal Logics, in: Handbook of Modal Logic, edited by P. Blackburn, F. Wolter, and J. van Benthem, Elsevier 2006, pp. 255-325. BibTeX entry [DO09] A. Dawar and M. Otto, Modal Characterisation Theorems over Special Classes of Frames, Annals of Pure and Applied Logic, volume 161, 2009, pp.~1-42. Abstract BibTeX entry [O04] M. Otto, Modal and Guarded Characterisation Theorems over Finite Transition Systems, Annals of Pure and Applied Logic, volume 130, 2004, pp.~173-205. Abstract BibTeX entry [DO05] A. Dawar and M. Otto, Modal Characterisation Theorems over Special Classes of Frames, Proceedings of 20th IEEE Symposium on Logic in Computer Science LICS 2005, pp 21-30. Abstract BibTeX entry |

## Expressive Power of Monadic Second-Order Logic

In the last two decades the beginnings of a model theory for monadic second-order logics were developed. Of particular interest are questions of definability and interpretability in given structures. On one hand, there are structures whose monadic theory is simple enough to admit a structure theory. All known examples of such structures have the property of being interpretable in a tree. On the other hand, there are structures whose monadic theory is extremely complicated. A prominent example are structures containing large definable grids. According to a conjecture of Seese these two extremes form a dichotomy: either a structure can be interpreted in a tree, or it contains a large grid. One emphasis of our work is on different kinds of interpretations. In particular, we try to characterise all structures that can be interpreted in a given one and to develop concrete combinatorial criteria for the existence ofan interpretation between two given (classes of) structures [BC10]. Considering the conjecture of Seese, interpretations in trees are of particular importance [B06]. A further topic of our work concerns variants of monadic second-order logic. An important extension of this logic is guarded second-order logic, which in general is strictly more expressive. According to a result of Courcelle, however, on countable sparse structures the expressive power of guarded second-order logic collapses to that of monadic second-order logic.[B10] Bibliography[BC10] Achim Blumensath and Bruno Courcelle, On the Monadic Second-Order Transduction Hierarchy, Logical Methods in Computer Science, 6(2010). [B06] Achim Blumensath, A Model Theoretic Characterisation of Clique-Width, Annals of Pure and Applied Logic, 142(2006), pp. 321-350. [B10] Achim Blumensath, Guarded Second-Order Logic, Spanning Trees, and Network Flows, Logical Methods in Computer Science, 6(2010). |

## Automata Theory and Algebraic Language Theory

There is a tight connection between automata and the monadic second-order theories of certain standard structures, like the order of the natural numbers or the infinite binary tree. In particular, Büchi and Rabin have shown that one can obtain decision procedures for these theories by translating formulae into automata. Automata theory has therefore become an essential tool in the investigation of monadic second-order logic. Besides using monadic second-order logic one can also characterise regular languages algebraically via homomorphisms into finite algebras. This point of view is particularly suited to the classification of fragments of monadic second-order logic and to the development of corresponding decision procedures. There are well-developed algebraic theories for languages of finite and infinite words. For languages of finite trees a preliminary theory has also been developed, but for infinite trees only partial results exists. We are currently actively working on such a theory. The main obstacle in the development of an algebraic language theory in this context are missing combinatorial tools, like Ramseyan factorisation theorems for trees. |