Abstract
It is well understood that solving parity games is equivalent, up to polynomial time, to model checking of the modal mu-calculus. It is a long-standing open problem whether solving parity games (or model checking modal mu-calculus formulas) can be done in polynomial time. A recent approach to studying this problem has been the design of partial solvers, algorithms that run in polynomial time and that may only solve parts of a parity game. Although it was shown that such partial solvers can completely solve many practical benchmarks, the design of such partial solvers was somewhat ad hoc, limiting a deeper understanding of the potential of that approach. We here mean to provide such robust foundations for deeper analysis through a new form of game, alternating reachability under parity. We prove the determinacy of these games and use this determinacy to define, for each player, a monotone fixed point over an ordered domain of height linear in the size of the parity game such that all nodes in its greatest fixed point are won by said player in the parity game. We show, through theoretical and experimental work, that such greatest fixed points and their computation leads to partial solvers that run in polynomial time. These partial solvers are based on established principles of static analysis and are more effective than partial solvers studied in extant work.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Chatterjee, K.: Linear time algorithm for weak parity games. CoRR abs/0805.1391 (2008)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, January 1977, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Abstract interpretation: past, present and future. In: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, 14–18 July 2014, p. 2 (2014)
Dam, M.: CTL* and ECTL* as fragments of the modal mu-calculus. Theor. Comput. Sci. 126(1), 77–96 (1994)
Dawar, A., Grädel, E.: The descriptive complexity of parity games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 354–368. Springer, Heidelberg (2008)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411–420 (1999)
Emerson, E., Jutla, C.: Tree automata, \(\mu \)-calculus and determinacy. In: Proceedings 32nd IEEE Symposium on Foundations of Computer Science, pp. 368–377 (1991)
Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982)
Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of \(\rm \mu \)-calculus. In: Proceedings of 5th International Conference on Computer Aided Verification, CAV 1993, Elounda, 28 June - 1 July, 1993, pp. 385–396 (1993)
Filipiuk, P., Nielson, F., Nielson, H.R.: Layered fixed point logic. CoRR abs/1204.2768 (2012)
Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182–196. Springer, Heidelberg (2009)
Huth, M., Kuo, J.H.-P., Piterman, N.: Fatal attractors in parity games. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 34–49. Springer, Heidelberg (2013)
Huth, M., Kuo, J.H., Piterman, N.: Fatal attractors in parity games: building blocks for partial solvers. CoRR abs/1405.0386 (2014)
Huth, M., Ryan, M.D.: Logic in Computer Science - Modelling and Reasoning About Systems, 2nd edn. Cambridge University Press, New York (2004)
Jurdziński, M.: Deciding the winner in parity games is in UP\({}\cap {}\)co-UP. Inf. Process. Lett. 68, 119–124 (1998)
Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983). http://dx.doi.org/10.1016/0304-3975(82)90125-6
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)
Martin, D.A.: Borel determinacy. Ann. Math. 102(2), 363–371 (1975)
Mostowski, A.W.: Games with forbidden positions. Technical Report 78, University of Gdańsk (1991)
Nielson, F., Nielson, H.R.: Model checking is static analysis of modal logic. In: Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, 20–28 March, 2010. Proceedings, pp. 191–205 (2010)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis (2. corr. print). Springer, Heidelberg (2005)
Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: International Symposium on Programming, 5th Colloquium, Torino, Italy, 6–8 April, 1982, Proceedings, pp. 337–351 (1982)
Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351–380. Springer, Heidelberg (1998)
Steffen, B.: Data flow analysis as model checking. In: Theoretical Aspects of Computer Software, International Conference TACS 1991, Sendai, Japan, 24–27 September, 1991, Proceedings, pp. 346–365 (1991)
Stirling, C.: Lokal model checking games. In: CONCUR 1995: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21–24, 1995, Proceedings, pp. 1–11 (1995)
Zhang, F., Nielson, F., Nielson, H.R.: Model checking as static analysis: revisited. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 99–112. Springer, Heidelberg (2012)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1–2), 135–183 (1998)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Huth, M., Kuo, J.HP., Piterman, N. (2016). Static Analysis of Parity Games: Alternating Reachability Under Parity. In: Probst, C., Hankin, C., Hansen, R. (eds) Semantics, Logics, and Calculi. Lecture Notes in Computer Science(), vol 9560. Springer, Cham. https://doi.org/10.1007/978-3-319-27810-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-27810-0_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27809-4
Online ISBN: 978-3-319-27810-0
eBook Packages: Computer ScienceComputer Science (R0)