2007

• D. Berwanger, E. Grädel, and G. Lenzi. The variable hierarchy of the $\mu$-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ädel and Giacomo Lenzi},
       title = {The variable hierarchy of the $\mu$-calculus is strict},
       journal = {Theory of Computing Systems},
       volume = {40},
       pages = {437–466},
       year = {2007},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGrLe-tocs07.pdf},
  }
  

• 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-Verlag, 2007.             
  BibTeX

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

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-Verlag, 2006.             
  BibTeX

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

• 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. 4179 of LNCS, pp. 46–60. Springer-Verlag, 2006.             
  BibTeX

  @inproceedings{BerwangerJan06,
       author = {Dietmar Berwanger and David Janin},
       title = {Automata on Directed Graphs: Vertex versus Edge Marking},
       booktitle = {Proceedings of the 3rd International Conference on Graph Transformation, ICGT 2006},
       url = {http://www.logic.rwth-aachen.de/~dwb/pub/acc.pdf},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {4179},
       pages = {46–60},
       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},
       title = {Games and Logical Expressiveness},
       school = {RWTH Aachen},
       year = {2005},
       task = {2,7},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/express.pdf},
  }
  

• 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-Verlag, 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ädel},
       title = {Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games},
       pages = {209–223},
       booktitle = {Proceedings of LPAR 2004, Montevideo, Uruguay},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {3452},
       year = {2005},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/BG_lpar04.pdf},
       task = {2},
  }
  

• D. Berwanger and G. Lenzi. The variable hierarchy of the $\mu$-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-Verlag, 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},
       title = {The variable hierarchy of the $\mu$-calculus is strict},
       booktitle = {STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science},
       publisher = {Springer-Verlag},
       series = {LNCS},
       volume = {3404},
       year = {2005},
       pages = {97–109},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/hierarchy.ps},
       task = {7},
  }
  

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ädel},
       title = {Fixed-Point Logics and Solitaire Games},
       journal = {Theory of Computing Systems},
       publisher = {Springer-Verlag},
       year = {2004},
       volume = {37},
       pages = {675–694},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGr_tocs.pdf},
       task = {2,7},
  }
  

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

• 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-Verlag, 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ädel and Sthephan Kreutzer},
       title = {Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games.},
       booktitle = {Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning},
       year = {2003},
       series = {LNCS},
       volume = {2850},
       pages = {226–240},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar03.ps},
       task = {7},
  }
  

2002

• D. Berwanger and A. Blumensath. Automata for Guarded Fixed Point Logics. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), LNCS, pp. 343-355. Springer Verlag, 2002.             
  BibTeX

  @incollection{BerwangerBl02,
       author = {Dietmar Berwanger and Achim Blumensath},
       title = {Automata for Guarded Fixed Point Logics},
       booktitle = {Automata, Logics, and Infinite Games},
       pages = {343-355},
       publisher = {Springer Verlag},
       year = {2002},
       editor = {E. Grädel and W. Thomas and T. Wilke},
       number = {2500},
       series = {LNCS},
       chapter = {19},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/guarded.ps},
  }
  

• D. Berwanger and A. Blumensath. The Monadic Theory of Tree-like Structures. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), LNCS, pp. 285-301. Springer Verlag, 2002.             
  BibTeX

  @incollection{BlumensathBe02,
       author = {Dietmar Berwanger and Achim Blumensath},
       title = {The Monadic Theory of Tree-like Structures},
       booktitle = {Automata, Logics, and Infinite Games},
       pages = {285-301},
       publisher = {Springer Verlag},
       year = {2002},
       editor = {E. Grädel and W. Thomas and T. Wilke},
       number = {2500},
       series = {LNCS},
       chapter = {16},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/muchnik.ps},
  }
  

• D. Berwanger and E. Grädel. Fixed point formulae and solitaire games. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.                                 
  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 , a fragment of least fixed point logic, whose model checking 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 efficiently computed. The model checking problem for is Pspace-complete in general and Ptime-complete for formulae of bounded width. On finite structures (but not on infinite ones), is equivalent to transitive closure logic.

  @inproceedings{BerwangerGra02,
       author = {Dietmar Berwanger and Erich Grädel},
       title = {Fixed point formulae and solitaire games},
       booktitle = {Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002},
       year = {2002},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/ciad02.ps},
       task = {7},
  }
  

• D. Berwanger, E. Grädel, and G. Lenzi. On the variable hierarchy of the modal mu-calculus. In Computer Science Logic, CSL 2002 (J. Bradfield, Ed.), vol. 2471 of LNCS, pp. 352–366. Springer-Verlag, 2002.                                 
  Abstract   BibTeX

  Most of the logics commonly used in verification, such as CTL, LTL, CTL*, PDL, etc. can in fact be embedded into the two-variable fragment of the mu-calculus. It is also known that the two-variable fragment can express properties that occur at arbitrarily high levels of the alternation hierarchy. However, it is an open problem whether the variable hierarchy is strict. Here we study this problem with a game-based approach and establish the strictness of the hierarchy for the case of existential (i.e., Box-free) formulae. It is known that these characterize precisely the L_\mu-definable properties that are closed under extensions. We also relate the strictness of the variable hierarchy to the question whether the finite variable fragments satisfy the existential preservation theorem.

  @inproceedings{BerwangerGraLen02,
       author = {Dietmar Berwanger and Erich Grädel and Giacomo Lenzi},
       title = {On the variable hierarchy of the modal mu-calculus},
       booktitle = {Computer Science Logic, CSL 2002},
       editor = {Julian Bradfield},
       year = {2002},
       series = {LNCS},
       volume = {2471},
       pages = {352–366},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/csl02.ps},
  }
  

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-Verlag, 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 = {D. Berwanger and E. Grädel},
       title = {Games and Model Checking for Guarded Logics},
       booktitle = {Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, LPAR 2001, Havana},
       editor = {R. Nieuwenhuis and A. Voronkov},
       year = {2001},
       series = {LNCS},
       volume = {2250},
       publisher = {Springer-Verlag},
       copyright = {(c) Springer-Verlag},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar.ps},
  }
  

• 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,
       author = {D. Berwanger},
       title = {Game Logic is Strong Enough for Parity Games},
       booktitle = {Proceedings of the ESSLLI 2001 Workshop on Logic and Games},
       editor = {M. Pauly and G. Sandu},
       year = {2001},
       address = {Helsinki},
       note = {Conference version of \citeBer03},
       url = {http://www.logic.rwth-aachen.de/pub/dwb/helsinki.ps},
  }
  

2000

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

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