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},
  }
  

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},
  }
  

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},
  }
  

2008

• D. Berwanger, K. Chatterjee, L. Doyen, T. A. Henzinger, and S. Raje. Strategy Construction for Parity Games with Imperfect Information. In Proceedings of the 19th International Conference on Concurrency Theory, CONCUR 2008, vol. 5201 of LNCS, pp. 325–339. Springer, 2008.                                 
  Abstract   BibTeX

  We consider imperfect-information parity games in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games, i.e., to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent perfect-information game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies. In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. We have implemented this algorithm as a prototype. To our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.

  @inproceedings{BerwangerCDHR08,
       author = {Dietmar Berwanger and Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger and Sangram Raje},
       booktitle = {{Proceedings of the 19th International Conference on Concurrency Theory, CONCUR~2008}},
       pages = {325--339},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Strategy Construction for Parity Games with Imperfect Information}},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/concur08.pdf},
       volume = {5201},
       year = {2008},
  }
  

2007

• D. Berwanger, E. Grädel, and G. Lenzi. The variable hierarchy of the μ-calculus is strict. Theory of Computing Systems, vol. 40, pp. 437–466, 2007.                                 
  Abstract   BibTeX

  Most of the logics commonly used in verification, such as LTL, CTL, CTL*, and PDL can be embedded into the two-variable fragment of the mu-calculus. It is also known that properties occurring at arbitrarily high levels of the alternation hierarchy can be formalised using only two variables. This raises the question whether the number of fixedpoint variables in mu-formulae can be bounded in general.

  We answer this question negatively, and prove that the variable-hierarchy of the mu-calculus is semantically strict. For any k, we provide examples of formulae with k variables that are not equivalent to any formula with fewer variables. In particular, this implies that Parikh's Game Logic is less expressive than the mu-calculus, thus resolving an open issue raised by Parikh in 1983.

  @article{BGL07,
       author = {Dietmar Berwanger and Erich Gr{\"a}del and Giacomo Lenzi},
       journal = {Theory of Computing Systems},
       pages = {437--466},
       title = {{The variable hierarchy of the $\mu$-calculus is strict}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGrLe-tocs07.pdf},
       volume = {40},
       year = {2007},
  }
  

• D. Berwanger. Admissibility in infinite games. In Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2007 (W. Thomas and P. Weil, Eds.), vol. 4393 of LNCS, pp. 188–199. Springer, 2007.             
  BibTeX

  @inproceedings{Berwanger07,
       author = {Dietmar Berwanger},
       booktitle = {{Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2007}},
       editor = {Wolfgang Thomas and Pascal Weil},
       pages = {188--199},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Admissibility in infinite games}},
       url = {http://www.logic.rwth-aachen.de/~dwb/admissibility.pdf},
       volume = {4393},
       year = {2007},
  }
  

2006

• D. Berwanger, A. Dawar, P. Hunter, and S. Kreutzer. DAG-width and parity games. In Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006, vol. 3884 of LNCS, pp. 524–536. Springer, 2006.             
  BibTeX

  @inproceedings{BDHK06,
       author = {Dietmar Berwanger and Anuj Dawar and Paul Hunter and Stephan Kreutzer},
       booktitle = {{Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006}},
       pages = {524--536},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{DAG-width and parity games}},
       url = {http://www.logic.rwth-aachen.de/~dwb/pub/dagwidth.pdf},
       volume = {3884},
       year = {2006},
  }
  

• D. Berwanger and D. Janin. Automata on Directed Graphs: Vertex versus Edge Marking. In Proceedings of the 3rd International Conference on Graph Transformation, ICGT 2006, vol. 4178 of LNCS, pp. 46–60. Springer, 2006.             
  BibTeX

  @inproceedings{BerwangerJan06,
       author = {Dietmar Berwanger and David Janin},
       booktitle = {{Proceedings of the 3rd International Conference on Graph Transformation, ICGT 2006}},
       pages = {46--60},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Automata on Directed Graphs: Vertex versus Edge Marking}},
       url = {http://www.logic.rwth-aachen.de/~dwb/pub/acc.pdf},
       volume = {4178},
       year = {2006},
  }
  

2005

• D. Berwanger. Games and Logical Expressiveness. PhD thesis, RWTH Aachen, 2005.                                 
  Abstract   BibTeX

  We investigat the inner structure of process logics, in particular of the mu-calculus $L\_\mu$, from the viewpoint of games over graphs. First, we show that Parikh's Game Logic, a two-variable sublogic of the mu-calculus, is expressive enough to capture parity games and, hence, to reach arbitrarily high levels of the $L\_\mu$ alternation hierarchy. Further, we devise a game that captures relevant issues of descriptive and computational complexity of the mu-calculus. As a first application, we show that, for the model-checking problem of $L\_\mu$, our game naturally leads to instances that can be solved in polynomial time. On the basis of this game, we also derive a parameter that captures the number of variables required to specify the behaviour of a given transition system in the mu-calculus. As a consequence, it follows that the expressive power of the mu-calculus strictly increases with the number of variables used in formulae. Already a particular case of this result, that three variables can express more than two, allows us to separate the expressive power of Parikh's Game Logic and the mu-calculus, a question that was open since 1983.

  @phdthesis{BerwangerThesis,
       author = {Dietmar Berwanger},
       school = {RWTH Aachen},
       task = {2,7},
       title = {{Games and Logical Expressiveness}},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/express.pdf},
       year = {2005},
  }
  

• D. Berwanger and E. Grädel. Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games. In Proceedings of LPAR 2004, Montevideo, Uruguay, vol. 3452 of LNCS, pp. 209–223. Springer, 2005.                                 
  Abstract   BibTeX

  We propose a new parameter for the complexity of finite directed graphs which measures to what extent the cycles of the graph are intertwined. This measure, called entanglement, is defined by way of a game that is similar in spirit to the robber and cops 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.

  As we will show, entanglement is intimately related to the descriptive complexity of the modal $\mu$-calculus. Particular, if we view the syntax of a formula as a tree with back edges leading from fixed-point variables to their definition, the block width of this syntax graph is bounded by the number of distinct variables used in the formula. On the one hand, the entanglement of a finite transition system provides an upper bound for the number of fixed point variables needed to describe it up to bisimulation.

  In addition to this, we prove 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 winning strategies.

  @inproceedings{BerwangerGraLPAR04,
       author = {Dietmar Berwanger and Erich Gr{\"a}del},
       booktitle = {{Proceedings of LPAR 2004, Montevideo, Uruguay}},
       pages = {209--223},
       publisher = {{Springer}},
       series = {{LNCS}},
       task = {2},
       title = {{Entanglement -- {A} Measure for the Complexity of Directed Graphs with Applications to Logic and Games}},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/BG_lpar04.pdf},
       volume = {3452},
       year = {2005},
  }
  

• D. Berwanger and G. Lenzi. The variable hierarchy of the μ-calculus is strict. In STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science, vol. 3404 of LNCS, pp. 97–109. Springer, 2005.                                 
  Abstract   BibTeX

  The modal $\mu$-calculus $\Lmu$ attains high expressive power by extending basic modal logic with monadic variables and binding them to extremal fixed points of definable operators. The number of variables occurring in a formula provides a relevant measure of its conceptual complexity. In a previous paper with Erich Grädel we have shown, for the existential fragment of $\Lmu$, that this conceptual complexity is also reflected in an increase of semantic complexity, by providing examples of existential formulae with $k$ variables that are not equivalent to any existential formula with fewer than $k$ variables.

  In this paper, we prove an existential preservation theorem for the family of $\Lmu$-formulae over at most $k$ variables that define simulation closures of finite strongly connected structures. Since hard formulae for the level $k$ of the existential hierarchy belong to this family, it follows that the bounded variable fragments of the full modal $\mu$-calculus form a hierarchy of strictly increasing expressive power.

  @inproceedings{BerwangerLen05,
       author = {Dietmar Berwanger and Giacomo Lenzi},
       booktitle = {{STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science}},
       pages = {97--109},
       publisher = {{Springer}},
       series = {{LNCS}},
       task = {7},
       title = {{The variable hierarchy of the $\mu$-calculus is strict}},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/hierarchy.ps},
       volume = {3404},
       year = {2005},
  }
  

2004

• D. Berwanger and E. Grädel. Fixed-Point Logics and Solitaire Games. Theory of Computing Systems, vol. 37, pp. 675–694, 2004.                                 
  Abstract   BibTeX

  The model checking games associated with fixed-point logics are parity games, and it is currently not known whether the strategy problem for parity games can be solved in polynomial time. We study $\SolLFP$, a fragment of least fixed-point logic, whose evaluation games are nested soltaire games. This means that on each strongly connected component of the game, only one player can make non-trivial moves. Winning sets of nested solitaire games can be computed efficiently.

  The model checking problem for $\SolLFP$ is \sc Pspace-complete in general and \sc Ptime-complete for formulae of bounded width. On finite structures (but not on infinite ones), $\SolLFP$ is equivalent to transitive closure logic.

  We also consider the solitaire fragment of guarded fixed-point logics. Due to the restricted quantification pattern of these logics, the associated games are small and therefore admit more efficient model checking algorithms.

  @article{BerwangerGra04,
       author = {Dietmar Berwanger and Erich Gr{\"a}del},
       journal = {Theory of Computing Systems},
       pages = {675--694},
       publisher = {{Springer}},
       task = {2,7},
       title = {{Fixed-Point Logics and Solitaire Games}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGr_tocs.pdf},
       volume = {37},
       year = {2004},
  }
  

2003

• D. Berwanger. Game Logic is Strong Enough for Parity Games. Studia Logica, vol. 75(2), pp. 205–219, 2003.                                 
  Abstract   BibTeX

  We investigate the expressive power of Parikh's Game Logic interpreted in Kripke structures, and show that the syntactical alternation hierarchy of this logic is strict. This is done by encoding the winning condition for parity games of rank $n$. It follows that Game Logic is not captured by any finite level of the modal $\mu$-calculus alternation hierarchy. Moreover, we can conclude that model checking for the $\mu$-calculus is efficiently solvable iff this is possible for Game Logic.

  @article{Ber03,
       author = {Dietmar Berwanger},
       journal = {Studia Logica},
       note = {Special issue on Game Logic and Game Algebra edited by M. Pauly and R. Parikh},
       number = {2},
       pages = {205--219},
       publisher = {Kluwer},
       title = {{Game Logic is Strong Enough for Parity Games}},
       url = {http://journals.kluweronline.com/article.asp?PIPS=5253758},
       volume = {75},
       year = {2003},
  }
  

• D. Berwanger, E. Grädel, and S. Kreutzer. Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games. In Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning, vol. 2850 of LNCS, pp. 226–240. Springer, 2003.                                 
  Abstract   BibTeX

  We study determinacy, definability and complexity issues of path games on finite and infinite graphs.

  Compared to the usual format of infinite games on graphs (such as Gale-Stewart games) we consider here a different variant where the players select, in each move, a path of arbitrary finite length, rather than just an edge. The outcome of a play is an infinite path, the winning condition hence is a set of infinite paths, possibly given by a formula from S1S, LTL, or first-order logic. Such games have a long tradition in descriptive set theory (in the form of Banach-Mazur games) and have recently been shown to have interesting application for planning in nondeterministic domains.

  It turns out that path games behave quite differently than classical graph games. For instance, path games with Muller conditions always admit positional winning strategies which are computable in polynomial time.

  With any logic on infinite paths (defining a winning condition) we can associate a logic on graphs, defining the winning regions of the associated path games. We explore the relationships between these logics. For instance, the winning regions of path games with an S1S-winning condition are definable in the modal mu-calculus. Further, if the winning condition is first-order (on paths), then the winning regions are definable in monadic path logic, or, for a large class of games, even in first-order logic. As a consequence, winning regions of LTL path games are definable in CTL*

  @inproceedings{BGK03,
       author = {Dietmar Berwanger and Erich Gr{\"a}del and Sthephan Kreutzer},
       booktitle = {{Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning}},
       pages = {226--240},
       publisher = {{Springer}},
       series = {{LNCS}},
       task = {7},
       title = {{Once Upon a Time in the West. {D}eterminacy, Complexity and Definability of Path Games.}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar03.ps},
       volume = {2850},
       year = {2003},
  }
  

2001

• D. Berwanger and E. Grädel. Games and Model Checking for Guarded Logics. In Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, LPAR 2001, Havana (R. Nieuwenhuis and A. Voronkov, Eds.), vol. 2250 of LNCS. Springer, 2001.                                 
  Abstract   BibTeX

  We investigate the model checking problems for guarded first-order and fixed point logics by reducing them to parity games. This approach is known to provide good results for the modal $\mu$-calculus and is very closely related to automata-based methods. To obtain good results also for guarded logics, optimized constructions of games have to be provided.

  Further, we study the structure of parity games, isolate èasy' cases that admit efficient algorithmic solutions, and determine their relationship to specific fragments of guarded fixed point logics.

  @inproceedings{BeGr01,
       author = {Dietmar Berwanger and Erich Gr{\"a}del},
       booktitle = {{Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, {LPAR} 2001, Havana}},
       editor = {R. Nieuwenhuis and A. Voronkov},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Games and Model Checking for Guarded Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar.ps},
       volume = {2250},
       year = {2001},
  }
  

• D. Berwanger. Game Logic is Strong Enough for Parity Games. In Proceedings of the ESSLLI 2001 Workshop on Logic and Games (M. Pauly and G. Sandu, Eds.), Helsinki, 2001.                                 
  Abstract   BibTeX

  This paper is concerned with the expressive power of Parikh's Game Logic interpreted in Kripke structures. We show that the syntactical alternation hierarchy of this logic is strict, by expressing the winning condition for parity games with $n$ priorities. Moreover, it follows that Game Logic is not captured by any finite level of the $\mu$-calculus alternation hierarchy. We can further conclude that model checking for the $\mu$-calculus is efficiently solvable iff this is possible for Game Logic.

  @inproceedings{Ber01,
       address = {Helsinki},
       author = {Dietmar Berwanger},
       booktitle = {{Proceedings of the ESSLLI 2001 Workshop on Logic and Games}},
       editor = {M. Pauly and G. Sandu},
       note = {Conference version of \cite{Ber03}},
       title = {{Game Logic is Strong Enough for Parity Games}},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/helsinki.ps},
       year = {2001},
  }
  

2000

• D. Berwanger. Games and Model Checking for Guarded Logics. Diploma thesis, RWTH-Aachen, 2000.             
  BibTeX

  @misc{Ber00,
       author = {Dietmar Berwanger},
       howpublished = {{Diploma thesis, RWTH-Aachen}},
       title = {{Games and Model Checking for Guarded Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/ber00.ps.gz},
       year = {2000},
  }