Publikationen

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},
       url = {http://www.logic.rwth-aachen.de/~kaiser/quantitative_games.pdf},
       pages = {301–312},
       year = {2008},
  }
  

• Ł. 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-Verlag, 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-Verlag},
       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-Verlag, 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-Verlag},
       series = {LNCS},
       editor = {Vladimiro Sassone},
       volume = {3441},
       year = {2005},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/rgtrs.pdf},
  }