Algorithmic Solutions via Model Theoretic Interpretations

• Algorithmische Lösungskonzepte basierend auf modelltheoretischen Interpretationen

Abu Zaid, Faried; Grädel, Erich (Thesis advisor); Kuske, Dietrich (Thesis advisor)

Aachen (2016, 2017)
Dissertation / PhD Thesis

Dissertation, RWTH Aachen University, 2016

Abstract

Model theoretic interpretations are an important tool in algorithmic model theory. Their applications range from reductions between logical theoriesto the construction of algorithms for problems, which are hard in general but efficiently solvable on restricted classes of structures, like 3-Colorability on graphs of bounded treewidth. We investigate this tool in three different areas of Algorithmic Model Theory: automata-based decision procedures for logical theories, algorithmic meta-theorems, and descriptive complexity.One of the main focus points of this dissertation are automata based presentations of infinite objects, which are closely related to monadic second-order interpretations over set variables. We introduce automatic presentations with advice for several automata models. These are presentations where the automata have access to some fixed auxiliary information. We develop algebraic and combinatorial tools, which enable us to prove that certain structures cannot have an omega-automatic presentation with advice. Our main result is that the field of reals is not omega-automatic with any advice, which has been an open problem since the introduction of omega-automatic presentations.The result can also be understood as an answer to a weakened version of a question posed by Rabin, namely whether the field of reals is interpretable in the infinite binary tree. Further, we consider uniformly automatic classes of structures, which are classes generated by a fixed presentation and a set of advices. Prototypic examplesare the class of all finite graphs of treewidth bounded by some constant, the torsion-free abelian groups of rank 1, and the class of all countable linear orders. Uniformly automatic presentations are also found in the mechanics that build the foundation for several algorithmic meta-theorems.We investigate the efficiency of this approach by analysing the runtime of the generic automata-based model checking algorithm in terms of the complexity of the given presentation. We show that the runtime on a presentation of the direct product closure is only one exponential higher than the runtime on the presentation of the primal class. We apply these findings to show that first-order model checking is fixed parameter tractable on the classes of all finite Boolean algebras and the class of all finite abelian groups. In both cases the parameter dependence of the runtime is elementary. The runtime which we achieve on these classes is either provably optimal or outperforms the previously known approaches. Furthermore, we show that the runtime of the generic automata based algorithm for monadic second-order model checking on graphs of treedepth at most h has a (h+2)-fold exponential parameter dependence. This matches the runtime of the best known algorithms for model checking on these classes. In the last part of this dissertation we turn our attention to logics with a build-in interpretation mechanism. Polynomial time interpretation logic (PIL) is an alternative characterisation of choiceless polynomial time (CPT). CPT is currently considered the most promising candidate for a logic capturing PTIME. We contribute to the exploration of the expressive power of CPTby showing that there is a CPT-definable canonisation procedure on classes of structures with bounded abelian colours. A structure has bounded abelian colours if it is of bounded colour class size andthe automorphism group on every colour class is abelian. Examples emerge from the classical examples that separate fixed point logic with Counting from PTIME. The CFI-construction of Cai, Fürer, and Immerman, as well as the Multipedes of Blass, Gurevich, and Shelah have bounded abelian colours. Consequently, the isomorphism problem on these classes is solvable in CPT. For Multipedes this was an open question. In fact, Blass, Gurevich, and Shelah conjectured that the isomorphism problem for Multipedes might not besolvable by a CPT procedure.

Institutions

• Mathematical Fundamentals of Computer Science (Logic and Complexity) Teaching and Research Area [117220]
• Department of Mathematics [110000]