TU Darmstadt Mathematik Fachgebiete Logic group Research Algorithmic Model Theory Model Constructions / Games FO on Configuration 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).

[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