Document Open Access Logo

Improved Set-Based Symbolic Algorithms for Parity Games

Authors Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Veronika Loitzenbauer

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.18.pdf
  • Filesize: 0.67 MB
  • 21 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
Wolfgang Dvorák
Monika Henzinger
Veronika Loitzenbauer

Cite As Get BibTex

Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, and Veronika Loitzenbauer. Improved Set-Based Symbolic Algorithms for Parity Games. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 18:1-18:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.18

Abstract

Graph games with omega-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify omega-regular winning conditions. Graph games with parity conditions are equivalent to mu-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms  for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators.
We consider graph games with n vertices and parity conditions with c priorities (equivalently, a mu-calculus formula with c alternations of least and greatest fixed points). While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires O(n^c) symbolic operations and linear space; and (b) an improved algorithm that requires  O(n^{c/2+1}) symbolic operations but also O(n^{c/2+1}) space (i.e., exponential space).
In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires  O(n^{c/3+1}) symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations.

Subject Classification

Keywords
  • model checking
  • graph games
  • parity games
  • symbolic computation
  • progress measure

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. B. Akers. Binary decision diagrams. IEEE Trans. Comput., C-27(6):509-516, 1978. Google Scholar
  2. R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. JACM, 49:672-713, 2002. URL: http://dx.doi.org/10.1145/585265.585270.
  3. M. Benerecetti, D. Dell'Erba, and F. Mogavero. Solving parity games via priority promotion. In CAV, pages 270-290, 2016. URL: http://dx.doi.org/10.1007/978-3-319-41540-6_15.
  4. T. A. Beyene, S. Chaudhuri, C. Popeea, and A. Rybalchenko. A constraint-based approach to solving games on infinite graphs. In POPL, pages 221-234, 2014. Google Scholar
  5. H. Björklund, S. Sandberg, and S. Vorobyov. A discrete subexponential algorithms for parity games. In STACS, pages 663-674, 2003. URL: http://dx.doi.org/10.1007/3-540-36494-3_58.
  6. A. Browne, E. M. Clarke, S. Jha, D. E. Long, and W. R. Marrero. An improved algorithm for the evaluation of fixpoint expressions. TCS, 178(1-2):237-255, 1997. Google Scholar
  7. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., C-35(8):677-691, 1986. URL: http://dx.doi.org/10.1109/TC.1986.1676819.
  8. J. R. Büchi and L. H. Landweber. Solving sequential conditions by finite-state strategies. Trans. AMS, 138:295-311, 1969. Google Scholar
  9. D. Bustan, O. Kupferman, and M. Y. Vardi. A measured collapse of the modal μ-calculus alternation hierarchy. In STACS, pages 522-533, 2004. Google Scholar
  10. C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In STOC, 2017. To appear. Google Scholar
  11. P. Cerný, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh. Quantitative synthesis for concurrent programs. In CAV, pages 243-259, 2011. Google Scholar
  12. K. Chatterjee, W. Dvořák, M. Henzinger, and V. Loitzenbauer. Improved set-based symbolic algorithms for parity games. CoRR, abs/1706.04889, 2017. URL: https://arxiv.org/abs/1706.04889.
  13. K. Chatterjee, M. Henzinger, and V. Loitzenbauer. Improved Algorithms for One-Pair and k-Pair Streett Objectives. In LICS, pages 269-280, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.34.
  14. A. Church. Logic, arithmetic, and automata. In ICM, pages 23-35, 1962. Google Scholar
  15. L. de Alfaro and M. Faella. An accelerated algorithm for 3-color parity games with an application to timed games. In CAV, pages 108-120, 2007. Google Scholar
  16. L. de Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga. The element of surprise in timed games. In CONCUR, pages 142-156, 2003. Google Scholar
  17. L. de Alfaro and T. A. Henzinger. Interface theories for component-based design. In EMSOFT, pages 148-165. 2001. URL: http://dx.doi.org/10.1007/3-540-45449-7_11.
  18. L. de Alfaro, T. A. Henzinger, and R. Majumdar. Symbolic algorithms for infinite-state games. In CONCUR, pages 536-550, 2001. URL: http://dx.doi.org/10.1007/3-540-44685-0_36.
  19. E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy. In FOCS, pages 368-377, 1991. URL: http://dx.doi.org/10.1109/SFCS.1991.185392.
  20. E. A. Emerson and Ch.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In LICS, pages 267-278, 1986. Google Scholar
  21. J. Fearnley, S. Jain, S. Schewe, F. Stephan, and D. Wojtczak. An ordered approach to solving parity games in quasi polynomial time and quasi linear space. To be announced at SPIN, 2017. URL: http://arxiv.org/abs/1703.01296.
  22. O. Friedmann. An exponential lower bound for the parity game strategy improvement algorithm as we know it. In LICS, pages 145-156, 2009. URL: http://dx.doi.org/10.1109/LICS.2009.27.
  23. O. Friedmann and M. Lange. Solving parity games in practice. In ATVA, pages 182-196, 2009. Google Scholar
  24. H. Gimbert and R. Ibsen-Jensen. A short proof of correctness of the quasi-polynomial time algorithm for parity games, 2017. URL: https://arxiv.org/abs/1702.01953.
  25. T. A. Henzinger, O. Kupferman, and S. K. Rajamani. Fair simulation. Information and Computation, 173(1):64-81, 2002. URL: http://dx.doi.org/10.1006/inco.2001.3085.
  26. P. Hoffmann and M. Luttenberger. Solving parity games on the GPU. In ATVA, pages 455-459, 2013. Google Scholar
  27. M. Huth, J. Huan-Pu Kuo, and N. Piterman. Concurrent small progress measures. In HVC, pages 130-144, 2011. Google Scholar
  28. B. Jobstmann, A. Griesmayer, and R. Bloem. Program repair as a game. In CAV, pages 226-238, 2005. URL: http://dx.doi.org/10.1007/11513988_23.
  29. M. Jurdziński. Small Progress Measures for Solving Parity Games. In STACS, pages 290-301, 2000. URL: http://dx.doi.org/10.1007/3-540-46541-3_24.
  30. M. Jurdziński and R. Lazić. Succinct progress measures for solving parity games. To be announced at LICS, 2017. URL: https://arxiv.org/abs/1702.05051.
  31. M. Jurdziński, M. Paterson, and U. Zwick. A Deterministic Subexponential Algorithm for Solving Parity Games. SIAM J. Comput., 38(4):1519-1532, 2008. Google Scholar
  32. C. Y. Lee. Representation of switching circuits by binary-decision programs. Bell System Techn. J., 38(4):985-999, 1959. URL: http://dx.doi.org/10.1002/j.1538-7305.1959.tb01585.x.
  33. P. Madhusudan and P. S. Thiagarajan. Distributed controller synthesis for local specifications. In ICALP, pages 396-407, 2001. URL: http://dx.doi.org/10.1007/3-540-48224-5_33.
  34. R. McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149-184, 1993. URL: http://dx.doi.org/10.1016/0168-0072(93)90036-D.
  35. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, pages 179-190, 1989. URL: http://dx.doi.org/10.1145/75277.75293.
  36. P. J. Ramadge and W. Murray Wonham. Supervisory control of a class of discrete-event processes. SIAM J. Control Optim., 25(1):206-230, 1987. URL: http://dx.doi.org/10.1137/0325013.
  37. S. Safra. On the complexity of ω-automata. In FOCS, pages 319-327, 1988. Google Scholar
  38. S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Inst., 1989. Google Scholar
  39. S. Schewe. Solving Parity Games in Big Steps. JCSS, 84:243-262, 2017. Google Scholar
  40. H. Seidl. Fast and simple nested fixpoints. IPL, 59(6):303-308, 1996. Google Scholar
  41. F. Somenzi. CUDD: CU decision diagram package release 3.0.0, 2015. URL: http://vlsi.colorado.edu/~fabio/CUDD/.
  42. S. Vester. Winning cores in parity games. In LICS, pages 662-671, 2016. Google Scholar
  43. J. Vöge and M. Jurdziński. A discrete strategy improvement algorithm for solving parity games. In CAV, pages 202-215, 2000. URL: http://dx.doi.org/10.1007/10722167_18.
  44. W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact