Definability and model checking : the role of orders and compositionality

  • Definierbarkeit und Model Checking : die Rolle von Ordnungen und Kompositionalität

Ganzow, Tobias; Grädel, Erich (Thesis advisor)

Aachen : Publikationsserver der RWTH Aachen University (2011, 2012)
Dissertation / PhD Thesis

Aachen, Techn. Hochsch., Diss., 2011


Finite model theory and descriptive complexity theory are concerned with assessing the expressive power of logics over finite models and with relating the descriptive resources needed for defining a class of structures to the computational complexity of the corresponding decision problem. In recent years, also the model theory and computational handling (e.g. of the model checking problem) of finitely representable infinite structures have gained much interest. In the first part of this thesis we study how the expressive power of logics over finite structures is affected by the presence of orders. We will first review the concept of order-invariant definability where we allow formulae to use an additional order-relation that is not present in a given structure in such a way that the truth of the formula in the structure does not depend on the actual interpretation of the order relation, and show that, in the context of monadic second-order logic, order-invariance yields more expressive power than adding modulo-counting quantifiers. Second, we investigate structures with weaker forms of orderings, namely locally ordered graphs, in which only the neighbourhoods of the vertices are linearly ordered. Using recent results on reachability algorithms by Reingold, we are able to show that the transitive closure of the edge relation in such graphs is definable in deterministic transitive closure logic (DTC) in a two-sorted setting, and this observation is the key to linking the descriptive power of DTC with counting to the computational power of logspace-bounded Turing machines. The second part of the thesis is concerned with techniques for model checking weak monadic second-order logic (WMSO) on the class of so-called inductive structures that allow for a finite representation via systems of equations, and which includes structures relevant for verification purposes such as the infinite binary tree, infinite lists, etc. Our new approach presents an algorithmic alternative to automata-theoretic methods, which exhibit certain drawbacks, and is based on a purely logical decomposition technique using the defining equations. Further, the deployed techniques can be extended to obtain a model checking algorithm for the extension of WMSO by an unbounding quantifier, and thus establish the decidability of its model checking problem on the class of inductive structures.