Publications

2012

• T. Ganzow. Definability and Model Checking: The Role of Orders and Compositionality. PhD thesis, RWTH Aachen University, 2012.                                 
  Abstract   BibTeX

  Finite model theory and descriptive complexity theory are concerned with assessing the expressive power of logics over finite models and wih relating the descriptive resources needed for defining a class of struc tures t the computational complexity of the corresponding decision problem. In recent years, also the model theory and computational handling (e.g. of the m odl checking problem) of finitely representable infinite structures have gai ned muchinterest. In the first part of this thesis we study how the expressive pow r of logics over finite structures is affected by the presence of orders. We w il first review the concept of order-invariant definability where we allow formul aeto use an additional order-relation that is not present in a given structure i such a way that the truth of the formula in the structure does not depend on t e actual interpretation of the order relation, and show that, in the context o 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.

  @phdthesis{Ganzow12,
       author = {Tobias Ganzow},
       school = {{RWTH} Aachen University},
       title = {{Definability and Model Checking: The Role of Orders and Compositionality}},
       url = {http://www.logic.rwth-aachen.de/pub/ganzow/diss.pdf},
       year = {2012},
  }
  

2010

• T. Ganzow and Ł. Kaiser. New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures. In Proceedings of the 19th Annual Conference of the European Association for Computer Science Logic, CSL 2010 (A. Dawar and H. Veith, Eds.), vol. 6247 of Lecture Notes in Computer Science, pp. 366–380. Springer, 2010.                                 
  Abstract   BibTeX

  Weak monadic second-order logic is a very expressive logic which has been used successfully for verification of software and hardware systems. Moreover, structures of bounded clique width have a decidable weak MSO theory which allows to specify and verify detailed correctness properties. However, one obstacle to a wide application of WMSO verification techniques in practice is that the prevalent model-checking algorithms are based on tree automata, and hence require to encode the structure of interest in the binary tree which is often a cause of inefficiency. We present a new algorithm for model-checking weak MSO on inductive structures, a certain kind of structures of bounded clique width, together with a proof of its decidability which follows from Shelah's composition method. Our algorithm directly manipulates formulas and checks them on the structure of interest without the need to encode it in the binary tree. In fact, the model-checking problem is reduced to solving a finite reachability game. In addition to the new algorithm, we also show that our method can be extended to obtain decidability of weak MSO extended with the unbounding quantifier on the binary tree, which was open before.

  @inproceedings{GK10,
       author = {Tobias Ganzow and {\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 19th Annual Conference of the European Association for Computer Science Logic, CSL~2010}},
       editor = {Anuj Dawar and Helmut Veith},
       pages = {366--380},
       publisher = {Springer},
       series = {{Lecture Notes in Computer Science}},
       title = {{New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures}},
       url = {http://logic.rwth-aachen.de/~kaiser/weak_mso_composition.pdf},
       volume = {6247},
       year = {2010},
  }
  

2008

• A. Dermaku, T. Ganzow, G. Gottlob, B. J. McMahan, N. Musliu, and M. Samer. Heuristic Methods for Hypertree Decomposition. In Proceedings of the 7th Mexican International Conference on Artificial Intelligence, MICAI 2008, pp. 1–11, 2008.             
  BibTeX

  @inproceedings{DGGMMS08,
       author = {Artan Dermaku and Tobias Ganzow and Georg Gottlob and Benjamin J. McMahan and Nysret Musliu and Marko Samer},
       booktitle = {{Proceedings of the 7th Mexican International Conference on Artificial Intelligence, MICAI~2008}},
       pages = {1--11},
       title = {{Heuristic Methods for Hypertree Decomposition}},
       url = {http://dx.doi.org/10.1007/978-3-540-88636-5_1},
       year = {2008},
  }
  

• T. Ganzow and S. Rubin. Order-Invariant MSO is Stronger than Counting MSO in the Finite. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 313–324, 2008.                                 
  Abstract   BibTeX

  We compare the expressiveness of two extensions of monadic second-order logic (MSO) over the class of finite structures. The first, counting monadic second-order logic (CMSO), extends MSO with first-order modulo-counting quantifiers, allowing the expression of queries like “the number of elements in the structure is even''. The second extension allows the use of an additional binary predicate, not contained in the signature of the queried structure, that must be interpreted as an arbitrary linear order on its universe, obtaining order-invariant MSO. While it is straightforward that every CMSO formula can be translated into an equivalent order-invariant MSO formula, the converse had not yet been settled. Courcelle showed that for restricted classes of structures both order-invariant MSO and CMSO are equally expressive, but conjectured that, in general, order-invariant MSO is stronger than CMSO. We affirm this conjecture by presenting a class of structures that is order-invariantly definable in MSO but not definable in CMSO.

  @inproceedings{GR08,
       author = {Tobias Ganzow and Sasha Rubin},
       booktitle = {{Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS~2008}},
       editor = {Susanne Albers and Pascal Weil},
       pages = {313--324},
       title = {{Order-Invariant {MSO} is Stronger than Counting {MSO} in the Finite}},
       url = {http://www.logic.rwth-aachen.de/pub/ganzow/GR-STACS08.pdf},
       year = {2008},
  }