Document

# Improved Set-Based Symbolic Algorithms for Parity Games

## File

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

## Cite As

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.
##### Keywords
• model checking
• graph games
• parity games
• symbolic computation
• progress measure

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. S. B. Akers. Binary decision diagrams. IEEE Trans. Comput., C-27(6):509-516, 1978.
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.
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.
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.
9. D. Bustan, O. Kupferman, and M. Y. Vardi. A measured collapse of the modal μ-calculus alternation hierarchy. In STACS, pages 522-533, 2004.
10. C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In STOC, 2017. To appear.
11. P. Cerný, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh. Quantitative synthesis for concurrent programs. In CAV, pages 243-259, 2011.
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.
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.
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.
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.
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.
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.
27. M. Huth, J. Huan-Pu Kuo, and N. Piterman. Concurrent small progress measures. In HVC, pages 130-144, 2011.
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.
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.
38. S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Inst., 1989.
39. S. Schewe. Solving Parity Games in Big Steps. JCSS, 84:243-262, 2017.
40. H. Seidl. Fast and simple nested fixpoints. IPL, 59(6):303-308, 1996.
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.
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.
X

Feedback for Dagstuhl Publishing