Model constructions / games

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).


[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

Acyclicity in Hypergraphs and Relational Structures

Finite Model Theory of Guarded Logics

Expressive Power of Monadic Second-Order logic

Automata Theory and Algebraic Language Theory