Publikationen

2009

• V. Bárány, Ł. Kaiser, and A. Rabinovich. Cardinality quantifiers in MLO over trees. In Proceedings of the 18th EACSL Annual Conference on Computer Science Logic, CSL '09 (E. Grädel and R. Kahle, Eds.), vol. 5771 of LNCS, pp. 117–132. Springer, 2009.                                 
  Abstract   BibTeX

  We study an extension of monadic second-order logic of order with the uncountability quantifier “there exist uncountably many sets''. We prove that, over the class of finitely branching trees, this extension is equally expressive to plain monadic second-order logic of order. Additionally we find that the continuum hypothesis holds for classes of sets definable in monadic second-order logic over finitely branching trees, which is notable for not all of these classes are analytic. Our approach is based on Shelah's composition method and uses basic results from descriptive set theory. The elimination result is constructive, yielding a decision procedure for the extended logic. Furthermore, by the well-known correspondence between monadic second-order logic and tree automata, our findings translate to analogous results on the extension of first-order logic by cardinality quantifiers over injectively presentable Rabin-automatic structures, generalizing the work of Kuske and Lohrey.

  @inproceedings{BKR09,
       author = {Vince Bárány and Łukasz Kaiser and Alexander Rabinovich},
       title = {Cardinality quantifiers in MLO over trees},
       booktitle = {Proceedings of the 18th EACSL Annual Conference on Computer Science Logic, CSL '09},
       editor = {Erich Grädel and Reinhard Kahle},
       publisher = {Springer},
       series = {LNCS},
       volume = {5771},
       year = {2009},
       pages = {117–132},
       url = {http://logic.rwth-aachen.de/~kaiser/msoc_trees.pdf},
  }
  

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative $\mu$-Calculus. Theory of Computing Systems, 2009.                                 
  Abstract   BibTeX

  We investigate quantitative extensions of modal logic and the modal $\mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $\mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $\mu$-calculus.

  @article{FGK09,
       author = {Diana Fischer and Erich Grädel and Łukasz Kaiser},
       title = {Model Checking Games for the Quantitative $\mu$-Calculus},
       journal = {Theory of Computing Systems},
       year = {2009},
       note = {Special Issue of STACS 2008},
       url = {http://logic.rwth-aachen.de/~kaiser/quantitative_games_journal.pdf},
  }
  

• E. Grädel, Ł. Kaiser, and R. Rabinovich. Directed Graphs of Entanglement Two. In Proceedings of the 17th International Symposium on Fundamentals of Computation Theory, FCT '09, vol. 5699 of LNCS, pp. 169–181. Springer, 2009.                                 
  Abstract   BibTeX

  Entanglement is a complexity measure for directed graphs that was used to show that the variable hierarchy of the propositional modal $\mu$-calculus is strict. While graphs of entanglement zero and one are indeed very simple, some graphs of entanglement two already contain interesting nesting of cycles. This motivates our study of the class of graphs of entanglement two, as these are both simple in a sense and already complex enough for modelling certain structured systems. Undirected graphs of entanglement two were already studied by Belkhir and Santocanale and a structural decomposition for such graphs was given. We study the general case of directed graphs of entanglement two and prove that they can be decomposed as well, in a way similar to the known decompositions for tree-width, DAG-width and Kelly-width. Moreover, we show that all graphs of entanglement two have both DAG-width and Kelly-width three. Since there exist both graphs with DAG-width three and graphs with Kelly-width three, but with arbitrary high entanglement, this confirms that graphs of entanglement two are a very basic class of graphs with cycles intertwined in an interesting way.

  @inproceedings{GKR09,
       author = {Erich Grädel and Łukasz Kaiser and Roman Rabinovich},
       title = {Directed Graphs of Entanglement Two},
       booktitle = {Proceedings of the 17th International Symposium on Fundamentals of Computation Theory, FCT '09},
       publisher = {Springer},
       series = {LNCS},
       volume = {5699},
       year = {2009},
       pages = {169–181},
       url = {http://logic.rwth-aachen.de/~kaiser/entanglement2.pdf},
  }
  

• Ł. Kaiser. Synthesis for Structure Rewriting Systems. In Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science, MFCS '09, vol. 5734 of LNCS, pp. 415–427. Springer, 2009.                                 
  Abstract   BibTeX

  The description of a single state of a modelled system is often complex in practice, but few procedures for synthesis address this problem in depth. We study systems in which a state is described by an arbitrary finite structure, and changes of the state are represented by structure rewriting rules, a generalisation of term and graph rewriting. Both the environment and the controller are allowed to change the structure in this way, and the question we ask is how a strategy for the controller that ensures a given property can be synthesised. We focus on one particular class of structure rewriting rules, namely on separated structure rewriting, a limited syntactic class of rules. To counter this restrictiveness, we allow the property to be ensured by the controller to be specified in a very expressive logic: a combination of monadic second-order logic evaluated on states and the modal $\mu$-calculus for the temporal evolution of the whole system. We show that for the considered class of rules and this logic, it can be decided whether the controller has a strategy ensuring a given property, and in such case a finite-memory strategy can be synthesised. Additionally, we prove that the same holds if the property is given by a monadic second-order formula to be evaluated on the limit of the evolution of the system.

  @inproceedings{K09,
       author = {Łukasz Kaiser},
       title = {Synthesis for Structure Rewriting Systems},
       booktitle = {Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science, MFCS '09},
       publisher = {Springer},
       series = {LNCS},
       volume = {5734},
       year = {2009},
       pages = {415–427},
       url = {http://logic.rwth-aachen.de/~kaiser/graph_games_short.pdf},
  }
  

2008

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative $\mu$-Calculus. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 301–312, 2008.                                 
  Abstract   BibTeX

  We investigate quantitative extensions of modal logic and the modal $\mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $\mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $\mu$-calculus.

  @inproceedings{FGK08,
       author = {Diana Fischer and Erich Grädel and Łukasz Kaiser},
       title = {Model Checking Games for the Quantitative $\mu$-Calculus},
       booktitle = {Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008},
       editor = {Susanne Albers and Pascal Weil},
       pages = {301–312},
       year = {2008},
  }
  

• Ł. Kaiser. Logic and Games on Automatic Structures. PhD thesis, RWTH Aachen, 2008.                                 
  Abstract   BibTeX

  The evaluation of a logical formula can be viewed as a game played by two opponents, one trying to show that the formula is true and the other trying to prove it false. This correspondence is exploited algorithmically to evaluate formulas of first and second-order logic on finite structures. We extend the game-based algorithmic approach to first-order logic on infinite structures that arise in computer science. Such structures are stored and manipulated by a computer, thus elements and relations must be represented in a finite way. We study a prominent class of finitely presentable structures, namely automatic structures.

  Automatic structures consist of elements represented by words over a finite alphabet. Relations within these structures are represented by synchronous automata that perform step-by-step transitions on tuples of symbols from the alphabet. A prominent example of an automatic structure is Presburger arithmetic, for which the natural way of writing numbers as sequences of digits and the standard column addition method constitute an automatic presentation.

  An important property of automatic structures is that first-order logic is decidable on these structures. To develop the correspondence between games and logic on automatic structures, we first look for suitable extensions of first-order logic that remain decidable. We study the notion of game quantification and extend the notions of open and closed game quantifiers, introduced in the model theory of infinitary logics, to a regular game quantifier. We show that this game quantifier preserves regularity on automatic presentations and investigate its expressive power. We identify the classes of structures on which first-order logic extended with this quantifier collapses to pure first-order logic. For better understanding of the classes where this is not the case, we introduce the notion of inductive automorphisms and show that they preserve relations defined using the game quantifier.

  Model-checking games for the above extension of first-order logic can be defined in a more natural way than for pure first-order logic. Towards this, we extend the classical two-player parity games to a multiplayer setting where two coalitions play against each other with a particular kind of hierarchical imperfect information about actions of the players. In contrast to the classical case, in hierarchical games it is essential that players alternate. We show that otherwise the problem which coalition wins a hierarchical game is undecidable. Nevertheless, there is an important aspect in which they are similar to classical games: hierarchical games are robust with respect to changes of the representation of winning condition.

  One reason for this robustness of hierarchical games is that only a finite memory is needed to reduce games with complex winning conditions to games with simpler ones. While this technique has been well-known for games with finitely many priorities, our approach is the first to extend it to games with infinitely many priorities on infinite arenas. We generalize the classical notion of latest appearance record to a new memory structure, which we show to be sufficient for winning Muller games with a finite or co-finite number of sets in the Muller condition, and additionally for a few other classes of games with infinitely many priorities. Certain classes of winning conditions on infinitely many priorities admit descriptions in terms of generalized Zielonka trees. We investigate such conditions and show that the correspondence between the number of branches of a Zielonka tree and the memory needed for strategies generalizes to the case of infinitely many priorities.

  A basic way of extending first-order logic is by adding generalized Lindström quantifiers. We address the following question: which generalized unary quantifiers can be added to first-order logic without introducing non-regular relations on automatic structures. We answer this question by giving a complete characterization of such quantifiers in terms of definability using cardinality and modulo counting quantifiers. We show that these quantifiers indeed preserve regularity on all automatic structures, including the non-injective omega-automatic ones. As a corollary we answer a question of Blumensath and prove that all countable omega-automatic structures are in fact finite-word automatic. Further, we study cardinality quantifiers on a large class of generalized-automatic structures. We use the composition method for monadic second-order logic to show that on such structures cardinality quantifiers collapse to first-order logic.

  @phdthesis{Kaiser08,
       author = {Łukasz Kaiser},
       title = {Logic and Games on Automatic Structures},
       year = {2008},
       school = {RWTH Aachen},
       type = {Ph.D. Thesis},
       url = {http://www.logic.rwth-aachen.de/~kaiser/diss.pdf},
  }
  

• Ł. Kaiser, S. Rubin, and V. Bárány. Cardinality and counting quantifiers on omega-automatic structures. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 385–396, 2008.                                 
  Abstract   BibTeX

  We investigate structures that can be represented by omega-automata, so called omega-automatic structures, and prove that relations defined over such structures in first-order logic expanded by the first-order quantifiers `there exist at most $\aleph_0$ many', 'there exist finitely many' and 'there exist $k$ modulo $m$ many' are omega-regular. The proof identifies certain algebraic properties of omega-semigroups. As a consequence an omega-regular equivalence relation of countable index has an omega-regular set of representatives. This implies Blumensath's conjecture that a countable structure with an $\omega$-automatic presentation can be represented using automata on finite words. This also complements a very recent result of Hjörth, Khoussainov, Montalban and Nies showing that there is an omega-automatic structure which has no injective presentation.

  @inproceedings{BKR08,
       author = {Łukasz Kaiser and Sasha Rubin and Vince Bárány},
       title = {Cardinality and counting quantifiers on omega-automatic structures},
       booktitle = {Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008},
       editor = {Susanne Albers and Pascal Weil},
       url = {http://www.logic.rwth-aachen.de/~kaiser/cardinality_automatic.pdf},
       pages = {385–396},
       year = {2008},
  }
  

2007

• E. Grädel and Ł. Kaiser. What kind of memory is needed to win infinitary Muller games? In Interactive Logic (J. van Benthem, B. Löwe, and D. Gabbay, Eds.), vol. 1 of Texts in Logic and Games. Amsterdam University Press, 2007.                                 
  Abstract   BibTeX

  In an influential paper entitled “How much memory is needed to win infinite games'', Dziembowski, Jurdziński, and Walukiewicz have shown that there are Muller games of size $O(n)$ whose winning strategies require memory of size at least $n!$. This shows that the LAR-memory, based on the latest appearance records introduced by Gurevich and Harrington, is optimal for solving Muller games. We review these results and reexamine the situation for the case of infinitary Muller games, i.e. Muller games with infinitely many priorities. We introduce a new, infinite, memory structure, based on finite appearance records (FAR) and investigate classes of Muller games that can be solved with FAR-memory.

  @inproceedings{GK07,
       author = {Erich Grädel and Łukasz Kaiser},
       title = {What kind of memory is needed to win infinitary Muller games?},
       editor = {Johan van Benthem and Benedikt Löwe and Dov Gabbay},
       booktitle = {Interactive Logic},
       series = {Texts in Logic and Games},
       volume = {1},
       publisher = {Amsterdam University Press},
       year = {2007},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/memory_kinds.pdf},
  }
  

2006

• Ł. Kaiser. Game Quantification on Automatic Structures and Hierarchical Model Checking Games. In Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006 (Z. Esik, Ed.), vol. 4207 of LNCS, pp. 411–425. Springer, 2006.                                 
  Abstract   BibTeX

  Game quantification is an expressive concept and has been studied in model theory and descriptive set theory, especially in relation to infinitary logics. Automatic structures on the other hand appear very often in computer science, especially in program verification. We extend first-order logic on structures on words by allowing to use an infinite string of alternating quantifiers on letters of a word, the game quantifier. This extended logic is decidable and preserves regularity on automatic structures, but can be undecidable on other structures even with decidable first-order theory. We show that in the presence of game quantifier any relation that allows to distinguish successors is enough to define all regular relations and therefore the game quantifier is strictly more expressive than first-order logic in such cases. Conversely, if there is an automorphism of atomic relations that swaps some successors then we prove that it can be extended to any relations definable with game quantifier. After investigating it's expressiveness, we use game quantification to introduce a new type of combinatorial games with multiple players and imperfect information exchanged with respect to a hierarchical constraint. It is shown that these games on finite arenas exactly capture the logic with game quantifier when players alternate their moves but are undecidable and not necessarily determined in the other case. In this way we define the first model checking games with finite arenas that can be used for model checking first-order logic on automatic structures.

  @inproceedings{K06,
       author = {Łukasz Kaiser},
       title = {Game Quantification on Automatic Structures and Hierarchical Model Checking Games},
       booktitle = {Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006},
       publisher = {Springer},
       series = {LNCS},
       editor = {Zoltan Esik},
       volume = {4207},
       pages = {411–425},
       year = {2006},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/game_quantifier_logic.pdf},
  }
  

2005

• Ł. Kaiser. Confluence of Right Ground Term Rewriting Systems is Decidable. In FOSSACS 2005, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (V. Sassone, Ed.), vol. 3441 of LNCS. Springer, 2005.                                 
  Abstract   BibTeX

  Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper we prove that confluence of a fairly large class of systems, namely right ground term rewriting systems, is decidable. We introduce a labelling of variables with colours and constrain substitutions according to these colours. We show how right ground rewriting systems can be reduced to simple systems with coloured variables. Such systems can be analysed using reduction-automata techniques which leads to an interesting decision procedure for confluence.

  @inproceedings{KaiserFossacs05,
       author = {Łukasz Kaiser},
       title = {Confluence of Right Ground Term Rewriting Systems is Decidable},
       booktitle = {FOSSACS 2005, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures},
       publisher = {Springer},
       series = {LNCS},
       editor = {Vladimiro Sassone},
       volume = {3441},
       year = {2005},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/rgtrs.pdf},
  }