Publications

2014

• F. Canavoi, E. Grädel, and R. Rabinovich. The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs. Theoretical Computer Science, vol. 560, Part 3(0), pp. 235 - 250, 2014.                                 
  Abstract   BibTeX

  Abstract The problem whether winning regions and winning strategies for parity games can be computed in polynomial time is a major open problem in the field of infinite games, which is relevant for many applications in logic and formal verification. For some time the discrete strategy improvement algorithm due to Jurdziński and Vöge had been considered to be a candidate for solving parity games in polynomial time. However, it has recently been proved by Oliver Friedmann that this algorithm requires super-polynomially many iteration steps, for all popular local improvements rules, including switch-all (also with Fearnley's snare memorisation), switch-best, random-facet, random-edge, switch-half, least-recently-considered, and Zadeh's Pivoting rule. We analyse the examples provided by Friedmann in terms of complexity measures for directed graphs such as treewidth, DAG-width, Kelly-width, entanglement, directed pathwidth, and cliquewidth. It is known that for every class of parity games on which one of these parameters is bounded, the winning regions can be efficiently computed. It turns out that with respect to almost all of these measures, the complexity of Friedmann's counterexamples is bounded, and indeed in most cases by very small numbers. This analysis strengthens in some sense Friedmann's results and shows that the discrete strategy improvement algorithm is even more limited than one might have thought. Not only does it require super-polynomial running time in the general case, where the problem of polynomial-time solvability is open, it even has super-polynomial time lower bounds on natural classes of parity games on which efficient algorithms are known.

  @article{CanavoiGraRab14,
       title = {The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs},
       journal = {Theoretical Computer Science},
       volume = {560, Part 3},
       number = {0},
       pages = {235 - 250},
       year = {2014},
       note = {Games, Automata, Logic and Formal Verification},
       issn = {0304-3975},
       doi = {http://dx.doi.org/10.1016/j.tcs.2013.12.021},
       url = {http://logic.rwth-aachen.de/pub/graedel/CanavoiGraRab14.pdf},
       author = {Felix Canavoi and Erich Gr{\"a}del and Roman Rabinovich},
       keywords = {Parity games},
       keywords = {Graph complexity measures},
       keywords = {Treewidth},
  }
  

2013

• R. Rabinovich. Graph Complexity Measures and Monotonicity. PhD thesis, RWTH Aachen University, 2013.             
  BibTeX

  @phdthesis{RPHD13,
       author = {Roman Rabinovich},
       school = {{RWTH} Aachen University},
       title = {Graph Complexity Measures and Monotonicity},
       url = {http://www.logic.rwth-aachen.de/~rabinovich/diss_19.04.2013.pdf},
       year = {2013},
  }
  

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

• E. Grädel, F. Canavoi, and R. Rabinovich. The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs. In Proceedings of the Third International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2012 (M. Faella and A. Murano, Eds.), Electronic Proceedings in Theoretical Computer Science, 2012.                                 
  Abstract   BibTeX

  For some time the discrete strategy improvement algorithm due to Jurdziński and V\"oge had been considered as a candidate for solving parity games in polynomial time. However, it has recently been proved by Oliver Friedmann that the strategy improvement algorithm requires super-polynomially many iteration steps, for all popular local improvements rules, including switch-all (also with Fearnley's snare memorisation), switch-best, random-facet, random-edge, switch-half, least-recently-considered, and Zadeh's Pivoting rule. We analyse the examples provided by Friedmann in terms of complexity measures for directed graphs such as treewidth, DAG-width, Kelly-width, entanglement, directed pathwidth, and cliquewidth. It is known that for every class of parity games on which one of these parameters is bounded, the winning regions can be efficiently computed. It turns out that with respect to almost all of these measures, the complexity of Friedmann's counterexamples is bounded, and indeed in most cases by very small numbers. This analysis strengthens in some sense Friedmann's results and shows that the discrete strategy improvement algorithm is even more limited than one might have thought. Not only does it require super-polynomial running time in the general case, where the problem of polynomial-time solvability is open, it even has super-polynomial lower time bounds on natural classes of parity games on which efficient algorithms are known.

  @inproceedings{CGR12,
       author = {Erich Gr{\"a}del and Felix Canavoi and Roman Rabinovich},
       title = {The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs},
       url = {http://www.logic.rwth-aachen.de/~rabinovich/simple_counterexamples.pdf},
       year = {2012},
       booktitle = {Proceedings of the Third International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2012},
       editor = {Marco Faella and Aniello Murano},
       series = {Electronic Proceedings in Theoretical Computer Science},
       note = {To appear},
  }
  

• D. Neider, R. Rabinovich, and M. Zimmermann. Down the Borel Hierarchy: Solving Muller Games via Safety Games. In Proceedings of the Third International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2012 (M. Faella and A. Murano, Eds.), Electronic Proceedings in Theoretical Computer Science, 2012.                                 
  Abstract   BibTeX

  We transform a Muller game with n vertices into a safety game with n!^3 vertices whose solution allows to determine the winning regoins of the Muller game and to compute a finite-state winning strategy for one player. This yields a novel antichain-based memory structure and a natural notion of permissive strategies for Muller games. Moreover, we generalize our construction by presenting a new type of game reduction from infinite games to safety games and show its applicability to several other winning conditions.

  @inproceedings{NRZ12,
       author = {Daniel Neider and Roman Rabinovich and Martin Zimmermann},
       title = {Down the Borel Hierarchy: Solving Muller Games via Safety Games},
       url = {http://www.logic.rwth-aachen.de/~rabinovich/downthehierarchy.pdf},
       year = {2012},
       booktitle = {Proceedings of the Third International Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2012},
       editor = {Marco Faella and Aniello Murano},
       series = {Electronic Proceedings in Theoretical Computer Science},
       note = {To appear},
  }
  

2011

• D. Neider, R. Rabinovich, and M. Zimmermann. Solving Muller Games via Safety Games. Technical Report. RWTH Aachen University, 2011.                                 
  Abstract   BibTeX

  We show how to transform a Muller game with n vertices into a safety game with (n!)^3 vertices whose solution allows to determine the winning reions of the Muller game and a winning strategy for one player.

  @techreport{NRZ11,
       author = {Daniel Neider and Roman Rabinovich and Martin Zimmermann},
       institution = {RWTH Aachen University},
       key = {Infinite Games, Muller Games, Safety Games, Antichains, Scores},
       month = {july},
       number = {AIB-2011-14},
       title = {{Solving Muller Games via Safety Games}},
       url = {http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2011/2011-14.pdf},
       year = {2011},
  }
  

• B. Puchala and R. Rabinovich. Graph Searching, Parity Games and Imperfect Information. arXiv:1110.5575v1 [cs.GT], 2011.                                 
  Abstract   BibTeX

  We investigate the interrelation between graph searching games and games with imperfect information. As key consequence we obtain that parity games with bounded imperfect information can be solved in PTIME on graphs of bounded DAG-width which generalizes several results for parity games on graphs of bounded complexity. We use a new concept of graph searching where several cops try to catch multiple robbers instead of just a single robber. The main technical result is that the number of cops needed to catch r robbers monotonously is at most r times the DAG-width of the graph. We also explore aspects of this new concept as a refinement of directed path-width which accentuates its connection to the concept of imperfect information.

  @misc{PR11,
       author = {Bernd Puchala and Roman Rabinovich},
       howpublished = {arXiv:1110.5575v1 [cs.GT]},
       title = {{Graph Searching, Parity Games and Imperfect Information}},
       url = {http://logic.rwth-aachen.de/~puchala/multiple-Robbers.pdf},
       year = {2011},
  }
  

2010

• B. Puchala and R. Rabinovich. Parity Games with Partial Information Played on Graphs of Bounded Complexity. In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science 2010, MFCS '10, vol. 6281 of LNCS, pp. 604–615. Springer, 2010.                                 
  Abstract   BibTeX

  We address the strategy problem for parity games with partial information and observable colors, played on finite graphs of bounded graph complexity. We consider several measures for the complexity of graphs and analyze in which cases, bounding the measure decreases the complexity of the strategy problem on the corresponding classes of graphs. We prove or disprove that the usual powerset construction for eliminating partial information preserves boundedness of the graph complexity. For the case where the partial information is unbounded we prove that the construction does not preserve boundedness of any measure we consider. We also prove that the strategy problem is EXPTIME-hard on graphs with directed path-width at most 2 and PSPACE-complete on acyclic graphs. For games with bounded partial information we obtain that the powerset construction, while neither preserving boundedness of entanglement nor of (undirected) tree-width, does preserve boundedness of directed path-width. Furthermore, if tree-width is bounded then DAG-width of the resulting graph is bounded. Therefore, parity games with bounded partial information, played on graphs with bounded directed path-width or tree-width can be solved in polynomial time.

  @inproceedings{PR10,
       author = {Bernd Puchala and Roman Rabinovich},
       booktitle = {Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science 2010, MFCS~'10},
       pages = {604--615},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Parity Games with Partial Information Played on Graphs of Bounded Complexity}},
       url = {http://logic.rwth-aachen.de/~puchala/bounded_partial.pdf},
       volume = {6281},
       year = {2010},
  }
  

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

2008

• R. Rabinovich. Complexity Measures of Directed Graphs. Diploma thesis, RWTH-Aachen, 2008.             
  BibTeX

  @misc{Rabinovich08,
       author = {Roman Rabinovich},
       howpublished = {Diploma thesis, RWTH-Aachen},
       title = {{Complexity Measures of Directed Graphs}},
       url = {http://logic.rwth-aachen.de/~rabinovich/diplomarbeit.pdf},
       year = {2008},
  }