2015

• E. Grädel, Ł. Kaiser, W. Pakusa, and S. Schalthöfer. Characterising Choiceless Polynomial Time with First-Order Interpretations. In Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015.             
  BibTeX

  @inproceedings{GKPS15,
       author = {Erich Gr{\"{a}}del and \L{}ukasz Kaiser and Wied Pakusa and Svenja Schalth{\"{o}}fer},
       booktitle = {{Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}},
       title = {{Characterising Choiceless Polynomial Time with First-Order Interpretations}},
       url = {http://www.logic.rwth-aachen.de/pub/schalthoefer/GKPS15.pdf},
       year = {2015},
  }
  

• Ł. Kaiser, M. Lang, S. Lessenich, and C. Löding. A Unified Approach to Boundedness Properties in MSO. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) (S. Kreutzer, Ed.), vol. 41 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 441–456, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015.             
  BibTeX

  @inproceedings{KaLaLeLo15,
       author = {{\L}ukasz Kaiser and Martin Lang and Simon Lessenich and Christof L{\"o}ding},
       title = {{A Unified Approach to Boundedness Properties in MSO}},
       booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
       pages = {441--456},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       year = {2015},
       volume = {41},
       editor = {Stephan Kreutzer},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {http://logic.rwth-aachen.de/pub/lessenich/KaLaLeLo15.pdf},
  }
  

2013

• F. Abu Zaid, E. Grädel, Ł. Kaiser, and W. Pakusa. Model-Theoretic Properties of omega-Automatic Structures. Theory of Computing Systems, Special Issue dedicated to STACS 2012, 2013.             
  BibTeX

  @article{AGKP12,
       author = {Faried {Abu Zaid} and Erich Gr{\"a}del and \L{}ukasz Kaiser and Wied Pakusa},
       title = {Model-Theoretic Properties of omega-Automatic Structures},
       journal = {Theory of Computing Systems, Special Issue dedicated to STACS 2012},
       url = {http://www.logic.rwth-aachen.de/pub/abuzaid/modelprop.pdf},
       note = {published online 17 October 2013},
       doi = {http://dx.doi.org/10.1007/s00224-013-9508-6},
       year = {2013},
  }
  

2012

• F. Abu Zaid, E. Grädel, and Ł. Kaiser. The Field of Reals is not omega-Automatic. In Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012 (C. Dürr and T. Wilke, Eds.), 2012.                                 
  Abstract   BibTeX

  We investigate structural properties of omega-automatic presentations of infinite structures in order to sharpen our methods to determine whether a given structure is omega-automatic. We apply these methods to show that no field of characteristic 0 admits an injective omega-automatic presentation, and that uncountable fields with a definable linear order cannot be omega-automatic.

  @inproceedings{AGK12,
       author = {Faried {Abu Zaid} and Erich Gr{\"a}del and {\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science, STACS~2012}},
       editor = {Christoph D{\"u}rr and Thomas Wilke},
       isbn = {978-3-939897-35-4},
       title = {{The Field of Reals is not omega-Automatic}},
       url = {http://www.logic.rwth-aachen.de/pub/abuzaid/reals_not_automatic.pdf},
       year = {2012},
  }
  

• D. Berwanger, E. Grädel, Ł. Kaiser, and R. Rabinovich. Entanglement and the Complexity of Directed Graphs. Theoretical Computer Science, vol. 463(0), pp. 2–25, 2012.                                 
  Abstract   BibTeX

  Entanglement is a parameter for the complexity of finite directed graphs that measures to which extent the cycles of the graph are intertwined. It is defined by way of a game similar in spirit to the cops and robber games used to describe tree width, directed tree width, and hypertree width. Nevertheless, on many classes of graphs, there are significant differences between entanglement and the various incarnations of tree width. Entanglement is intimately related with the computational and descriptive complexity of the modal $\mu$-calculus. The number of fixed-point variables needed to describe a finite graph up to bisimulation is captured by its entanglement. This plays a crucial role in the proof that the variable hierarchy of the $\mu$-calculus is strict. We study complexity issues for entanglement and compare it to other structural parameters of directed graphs. One of our main results is that parity games of bounded entanglement can be solved in polynomial time. Specifically, we establish that the complexity of solving a parity game can be parametrised in terms of the minimal entanglement of subgames induced by a winning strategy. Furthermore, we discuss the case of graphs of entanglement two. While graphs of entanglement zero and one are very simple, graphs of entanglement two allow arbitrary nesting of cycles, and they form a sufficiently rich class for modelling relevant classes of structured systems. We provide characterisations of this class, and propose decomposition notions similar to the ones for tree width, DAG-width, and Kelly-width.

  @article{BGKR12,
       author = {Dietmar Berwanger and Erich Gr{\"a}del and {\L}ukasz Kaiser and Roman Rabinovich},
       journal = {Theoretical Computer Science},
       title = {{Entanglement and the Complexity of Directed Graphs}},
       url = {http://logic.rwth-aachen.de/~rabinovich/entangle.pdf},
       year = {2012},
       volume = {463},
       number = {0},
       pages = {2--25},
       note = {Special Issue on Theory and Applications of Graph Searching Problems},
       issn = {0304-3975},
       doi = {10.1016/j.tcs.2012.07.010},
  }
  

• D. Berwanger, Ł. Kaiser, and S. Lessenich. Solving Counter Parity Games. In Mathematical Foundations of Computer Science 2012 (B. Rovan, V. Sassone, and P. Widmayer, Eds.), vol. 7464 of Lecture Notes in Computer Science, pp. 160-171. Springer Berlin / Heidelberg, 2012.                                 
  Abstract   BibTeX

  We study a class of parity games equipped with counters that evolve according to arbitrary non-negative affine functions. These games capture several cost models for dynamic systems from the literature. We present an elementary algorithm for computing the exact value of a counter parity game, which both generalizes previous results and improves their complexity. To this end, we introduce a class of omega-regular games with imperfect information and imperfect recall, solve them using automata-based techniques, and prove a correspondence between finite-memory strategies in such games and strategies in counter parity games.

  @incollection{BKL12,
       author = {Dietmar Berwanger and {\L}ukasz Kaiser and Simon Lessenich},
       title = {Solving Counter Parity Games},
       booktitle = {Mathematical Foundations of Computer Science 2012},
       series = {Lecture Notes in Computer Science},
       editor = {Branislav Rovan and Vladimiro Sassone and Peter Widmayer},
       publisher = {Springer Berlin / Heidelberg},
       isbn = {978-3-642-32588-5},
       keyword = {Computer Science},
       pages = {160-171},
       volume = {7464},
       note = {10.1007/978-3-642-32589-2_17},
       year = {2012},
       url = {http://www.logic.rwth-aachen.de/pub/lessenich/counter_parity.pdf},
  }
  

• D. Fischer and Ł. Kaiser. Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems. Logical Methods in Computer Science, vol. 8(3), 2012.                                 
  Abstract   BibTeX

  We study the model-checking problem for a quantitative extension of the modal mu-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions that arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and allow the measurement of interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative mu-calculus, can be model checked with arbitrary precision on initialised linear hybrid systems. To this end, we develop new techniques for the discretisation of continuous state spaces based on a special class of strategies in model-checking games and present a reduction to a class of counter parity games.

  @article{FK12,
       author = {Diana Fischer and \L{}ukasz Kaiser},
       title = {Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems},
       journal = {Logical Methods in Computer Science},
       volume = {8},
       number = {3},
       year = {2012},
       ee = {http://dx.doi.org/10.2168/LMCS-8(3:21)2012},
       url = {http://arxiv.org/pdf/1209.1738.pdf},
  }
  

• Ł. Kaiser and S. Lessenich. A Counting Logic for Structure Transition Systems. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (P. Cégielski and A. Durand, Eds.), vol. 16 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 366–380, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2012.             
  BibTeX

  @inproceedings{KL12,
       author = {{\L}ukasz Kaiser and Simon Lessenich},
       title = {{A Counting Logic for Structure Transition Systems}},
       booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
       pages = {366--380},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-939897-42-2},
       issn = {1868-8969},
       year = {2012},
       volume = {16},
       editor = {Patrick C{\'e}gielski and Arnaud Durand},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {http://www.logic.rwth-aachen.de/pub/lessenich/itrs_qmu.pdf},
       urn = {urn:nbn:de:0030-drops-36848},
       doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.366},
       annote = {Keywords: Logic in Computer Science, Quantitative Logics, Model Checking},
  }
  

2011

• D. Berwanger, Ł. Kaiser, and S. Lessenich. Imperfect Recall and Counter Games. Technical Report. Laboratoire Spécification et Vérification, ENS Cachan, France, 2011.             
  BibTeX

  @techreport{BKL11,
       author = {Dietmar Berwanger and {\L}ukasz Kaiser and Simon Lessenich},
       institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France},
       month = {Sep.},
       number = {LSV-11-20},
       title = {{Imperfect Recall and Counter Games}},
       type = {Research Report},
       url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-20.pdf},
       year = {2011},
  }
  

• D. Berwanger, Ł. Kaiser, and B. Puchala. A Perfect-Information Construction for Coordination in Games. In 31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS '11, pp. 387-398. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.                                 
  Abstract   BibTeX

  We present a general construction for eliminating imperfect information from games with several players who coordinate against nature, and to transform them into two-player games with perfect information while preserving winning strategy profiles. The construction yields an infinite game tree with epistemic models associated to nodes. To obtain a more succinct representation, we define an abstraction based on homomorphic equivalence, which we prove to be sound for games with observable winning conditions. The abstraction generates finite game graphs in several relevant cases, and leads to a new semi-decision procedure for multi-player games with imperfect information.

  @inproceedings{BKP11,
       author = {Dietmar Berwanger and {\L}ukasz Kaiser and Bernd Puchala},
       booktitle = {31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS~'11},
       pages = {387-398},
       publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
       title = {{A Perfect-Information Construction for Coordination in Games}},
       url = {http://logic.rwth-aachen.de/~puchala/tracking.pdf},
       year = {2011},
  }
  

• V. Bárány, Ł. Kaiser, and A. Rabinovich. Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Chains. J. Symb. Logic, vol. 76(2), pp. 603-619, 2011.                                 
  Abstract   BibTeX

  We investigate the extension of monadic second-order logic of order with cardinality quantifiers “there exists uncountably many sets such that ...'' and “there exists continuum many sets such that ...''. We prove that over the class of countable linear orders the two quantifiers are equivalent and can be effectively and uniformly eliminated. Weaker or partial elimination results are obtained for certain wider classes of chains. In particular, we show that over the class of ordinals the uncountability quantifier can be effectively and uniformly eliminated. Our argument makes use of Shelah's composition method and Ramsey-like theorem for dense linear orders.

  @article{BKRJSL,
       author = {Vince B{\'a}r{\'a}ny and {\L}ukasz Kaiser and Alexander Rabinovich},
       journal = {J. Symb. Logic},
       volume = {76},
       number = {2},
       year = {2011},
       pages = {603-619},
       title = {{Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Chains}},
       url = {http://logic.rwth-aachen.de/~kaiser/msoc_chains.pdf},
  }
  

• D. Fischer and Ł. Kaiser. Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems. In Proceedings of the 38th International Colloquium on Automata, Languages and Programming, ICALP 2011 (2), vol. 6756 of Lecture Notes in Computer Science, pp. 404–415. Springer, 2011.                                 
  Abstract   BibTeX

  In this work, we consider the model-checking problem for a quantitative extension of the modal mu-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions, which arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and additionally allow to measure interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative mu-calculus, can be model-checked with arbitrary precision on initialised linear hybrid systems. To this end, we develop new techniques for the discretisation of continuous state spaces based on a special class of strategies in model-checking games and show decidability of a class of counter-reset games that may be of independent interest.

  @inproceedings{FK11,
       author = {Diana Fischer and {\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 38th International Colloquium on Automata, Languages and Programming, ICALP~2011 (2)}},
       pages = {404--415},
       publisher = {Springer},
       series = {{Lecture Notes in Computer Science}},
       title = {{Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems}},
       url = {http://www.liafa.jussieu.fr/~kaiser/pub/linear_hybrid_qmu.pdf},
       volume = {6756},
       year = {2011},
  }
  

2010

• D. Berwanger and Ł. Kaiser. Information Tracking in Games on Graphs. Journal of Logic, Language and Information, 2010.                                 
  Abstract   BibTeX

  When seeking to coordinate in a game with imperfect information, it is often relevant for a player to know what other players know. Keeping track of the information acquired in a play of infinite duration may, however, lead to infinite hierarchies of higher-order knowledge. We present a construction that makes explicit which higher-order knowledge is relevant in a game and allows us to describe a class of games that admit coordinated winning strategies with finite memory.

  @article{BK10,
       author = {Dietmar Berwanger and {\L}ukasz Kaiser},
       journal = {Journal of Logic, Language and Information},
       note = {Special Issue on Temporal Logics of Agency},
       title = {{Information Tracking in Games on Graphs}},
       url = {http://logic.rwth-aachen.de/~kaiser/track.pdf},
       year = {2010},
  }
  

• V. Bárány, Ł. Kaiser, and A. Rabinovich. Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Trees. Fundamenta Informaticae, vol. 100, pp. 1–18, 2010.                                 
  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.

  @article{BKR10,
       author = {Vince B{\'a}r{\'a}ny and {\L}ukasz Kaiser and Alexander Rabinovich},
       journal = {Fundamenta Informaticae},
       pages = {1--18},
       title = {{Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Trees}},
       url = {http://logic.rwth-aachen.de/~kaiser/msoc_trees_fi.pdf},
       volume = {100},
       year = {2010},
  }
  

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative mu-Calculus. Theory Comput. Syst., vol. 47(3), pp. 696–719, 2010.                                 
  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{FGK10,
       author = {Diana Fischer and Erich Gr{\"a}del and {\L}ukasz Kaiser},
       journal = {Theory Comput. Syst.},
       number = {3},
       pages = {696--719},
       title = {{Model Checking Games for the Quantitative mu-Calculus}},
       url = {http://logic.rwth-aachen.de/~kaiser/quantitative_games_journal.pdf},
       volume = {47},
       year = {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},
  }
  

• M. Holtmann, Ł. Kaiser, and W. Thomas. Degrees of Lookahead in Regular Infinite Games. In Proceedings of the 13th International Conference on Foundations of Software Science and Computation Structures, FOSSACS '10, vol. 6014 of LNCS, pp. 252–266. Springer, 2010.                                 
  Abstract   BibTeX

  We study variants of regular infinite games where the strict alternation of moves between the two players is subject to modifications. The second player may postpone a move for a finite number of steps, or, in other words, exploit in his strategy some lookahead on the moves of the opponent. This captures situations in distributed systems, e.g. when buffers are present in communication or when signal transmission between components is deferred. We distinguish strategies with different degrees of lookahead, among them being the continuous and the bounded lookahead strategies. In the first case the lookahead is of finite possibly unbounded size, whereas in the second case it is of bounded size. We show that for regular infinite games the solvability by continuous strategies is decidable, and that a continuous strategy can always be reduced to one of bounded lookahead. Moreover, this lookahead is at most doubly exponential in the size of the parity automaton recognizing the winning condition. We also show that the result fails for non-regular games where the winning condition is given by a context-free omega-language.

  @inproceedings{HKT10,
       author = {Michael Holtmann and {\L}ukasz Kaiser and Wolfgang Thomas},
       booktitle = {{Proceedings of the 13th International Conference on Foundations of Software Science and Computation Structures, FOSSACS~'10}},
       pages = {252--266},
       publisher = {Springer},
       series = {{LNCS}},
       title = {{Degrees of Lookahead in Regular Infinite Games}},
       url = {http://logic.rwth-aachen.de/~kaiser/continuous_finite_delay.pdf},
       volume = {6014},
       year = {2010},
  }
  

• Ł. Kaiser and Ł. Stafiniak. Playing Structure Rewriting Games. In Proceedings of AGI '10. Atlantis Press, 2010.                                 
  Abstract   BibTeX

  Achieving goals in a complex environment in which many players interact is a general task demanded from an AI agent. When goals of the players are given explicitly, such setting can be described as a multi-player game with complete information. We introduce a general model of such games in which states are represented by relational structures (hypergraphs), possibly with real-valued labels, and actions \%are given by structure rewriting rules. For this model, we develop an algorithm which computes rational strategies for the players. Our algorithm can be parametrized by a probabilistic evaluation function and we devise a general procedure for learning such evaluations. First tests on a few classical examples substantiate the chosen game model and our algorithm.

  @inproceedings{KS10,
       author = {{\L}ukasz Kaiser and {\L}ukasz Stafiniak},
       booktitle = {{Proceedings of AGI~'10}},
       publisher = {Atlantis Press},
       title = {{Playing Structure Rewriting Games}},
       url = {http://logic.rwth-aachen.de/~kaiser/playing_structure_rewriting_games.pdf},
       year = {2010},
  }
  

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{\'a}r{\'a}ny and {\L}ukasz Kaiser and Alexander Rabinovich},
       booktitle = {{Proceedings of the 18th EACSL Annual Conference on Computer Science Logic, CSL~'09}},
       editor = {Erich Gr{\"a}del and Reinhard Kahle},
       pages = {117--132},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Cardinality quantifiers in MLO over trees}},
       url = {http://logic.rwth-aachen.de/~kaiser/msoc_trees.pdf},
       volume = {5771},
       year = {2009},
  }
  

• 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{\"a}del and {\L}ukasz Kaiser and Roman Rabinovich},
       booktitle = {{Proceedings of the 17th International Symposium on Fundamentals of Computation Theory, FCT~'09}},
       pages = {169--181},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Directed Graphs of Entanglement Two}},
       url = {http://logic.rwth-aachen.de/~kaiser/entanglement2.pdf},
       volume = {5699},
       year = {2009},
  }
  

• Ł. 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 = {{\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science, MFCS~'09}},
       pages = {415--427},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Synthesis for Structure Rewriting Systems}},
       url = {http://logic.rwth-aachen.de/~kaiser/graph_games_short.pdf},
       volume = {5734},
       year = {2009},
  }
  

2008

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative μ-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{\"a}del and {\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS~2008}},
       editor = {Susanne Albers and Pascal Weil},
       pages = {301--312},
       title = {{Model Checking Games for the Quantitative $\mu$-Calculus}},
       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 = {{\L}ukasz Kaiser},
       school = {RWTH Aachen},
       title = {{Logic and Games on Automatic Structures}},
       type = {Ph.D. Thesis},
       url = {http://www.logic.rwth-aachen.de/~kaiser/diss.pdf},
       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 = {{\L}ukasz Kaiser and Sasha Rubin and Vince B{\'a}r{\'a}ny},
       booktitle = {{Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS~2008}},
       editor = {Susanne Albers and Pascal Weil},
       pages = {385--396},
       title = {{Cardinality and counting quantifiers on omega-automatic structures}},
       url = {http://www.logic.rwth-aachen.de/~kaiser/cardinality_automatic.pdf},
       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, pp. 89–116. 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{\"a}del and {\L}ukasz Kaiser},
       booktitle = {{Interactive Logic}},
       editor = {Johan van Benthem and Benedikt L{\"o}we and Dov Gabbay},
       pages = {89--116},
       publisher = {Amsterdam University Press},
       series = {{Texts in Logic and Games}},
       title = {{What kind of memory is needed to win infinitary Muller games?}},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/memory_kinds.pdf},
       volume = {1},
       year = {2007},
  }
  

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 = {{\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006}},
       editor = {Zoltan Esik},
       pages = {411--425},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Game Quantification on Automatic Structures and Hierarchical Model Checking Games}},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/game_quantifier_logic.pdf},
       volume = {4207},
       year = {2006},
  }
  

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, pp. 470–489. 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 = {{\L}ukasz Kaiser},
       booktitle = {{FOSSACS 2005, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures}},
       editor = {Vladimiro Sassone},
       pages = {470--489},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Confluence of Right Ground Term Rewriting Systems is Decidable}},
       url = {http://www.logic.rwth-aachen.de/pub/kaiser/rgtrs.pdf},
       volume = {3441},
       year = {2005},
  }
  

2004

• Ł. Kaiser. Network Design with Selfish Agents. GI Dagstuhl Seminar Report, 2004.                                 
  Abstract   BibTeX

  We study the price of stability and price of anarchy in network design games under various constraints and mechanisms.

  @misc{KaiND04,
       author = {{\L}ukasz Kaiser},
       howpublished = {{GI} {D}agstuhl {S}eminar {R}eport},
       title = {{Network Design with Selfish Agents}},
       url = {http://www.logic.rwth-aachen.de/~kaiser/network_design_report.pdf},
       year = {2004},
  }