Skip to main content
SpringerLink
Log in

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10145))

Abstract

2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that—in contrast to existing techniques—tackles both aspects with the best suited approach and works exclusively on the 2.5 player game itself. The resulting technique is powerful enough to handle games with several million states.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In classic strategy improvement algorithms, the restriction to implementing a change once is made to keep it easy to identify the improvements. Such changes will also lead to an improvement when applied repeatedly.

  2. 2.

    In the notation of [7, 9], \(\pi = \mathsf {Tr}_{\text {almost}}(\overline{\pi }_Q)\).

References

  1. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. JACM 49(5), 672–713 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  2. Andersson, D., Miltersen, P.B.: The complexity of solving stochastic games on graphs. In: Dong, Y., Du, D.-Z., Ibarra, O. (eds.) ISAAC 2009. LNCS, vol. 5878, pp. 112–121. Springer, Heidelberg (2009). doi:10.1007/978-3-642-10631-6_13

    Chapter  Google Scholar 

  3. Berwanger, D., Dawar, A., Hunter, P., Kreutzer, S.: DAG-width and parity games. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 524–536. Springer, Heidelberg (2006). doi:10.1007/11672142_43

    Chapter  Google Scholar 

  4. Björklund, H., Vorobyov, S.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. DAM 155(2), 210–229 (2007)

    MathSciNet  MATH  Google Scholar 

  5. Browne, A., Clarke, E.M., Jha, S., Long, D.E., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. TCS 178(1–2), 237–255 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  6. Chatterjee, K.: The complexity of stochastic müller games. Inf. Comput. 211, 29–48 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  7. Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of quantitative concurrent parity games. In: SODA, pp. 678–687. SIAM (2006)

    Google Scholar 

  8. Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Strategy improvement for concurrent reachability and turn-based stochastic safety games. J. Comput. Syst. Sci. 79(5), 640–657 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  9. Chatterjee, K., Henzinger, T.A.: Strategy improvement and randomized subexponential algorithms for stochastic parity games. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 512–523. Springer, Heidelberg (2006). doi:10.1007/11672142_42

    Chapter  Google Scholar 

  10. Chatterjee, K., Henzinger, T.A.: Strategy improvement for stochastic rabin and streett games. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 375–389. Springer, Heidelberg (2006). doi:10.1007/11817949_25

    Chapter  Google Scholar 

  11. Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A.: Gist: a solver for probabilistic games. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 665–669. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_57

    Chapter  Google Scholar 

  12. Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Quantitative stochastic parity games. In: SODA 2004, pp. 121–130 (2004)

    Google Scholar 

  13. Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: a model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185–191. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_13

    Chapter  Google Scholar 

  14. Condon, A.: On algorithms for simple stochastic games. Adv. Comput. Complex. Theory 13, 51–73 (1993)

    MathSciNet  MATH  Google Scholar 

  15. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  16. de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: LICS, pp. 279–290 (2001)

    Google Scholar 

  17. de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. In: Vitter, J.S., Spirakis, P.G., Yannakakis, M. (eds.) Proceedings on 33rd Annual ACM Symposium on Theory of Computing, 6–8 July 2001, Heraklion, Crete, Greece, pp. 675–683. ACM (2001)

    Google Scholar 

  18. de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  19. Emerson, E.A., Jutla, C.S.: Tree automata, \(\mu \)-calculus and determinacy. In: FOCS, pp. 368–377 (1991)

    Google Scholar 

  20. Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of \(\mu \)-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_32

    Chapter  Google Scholar 

  21. Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \(\mu \)-calculus. In: LICS, pp. 267–278 (1986)

    Google Scholar 

  22. Fearnley, J.: Non-oblivious strategy improvement. In: LPAR, pp. 212–230 (2010)

    Google Scholar 

  23. Friedmann, O.: An exponential lower bound for the parity game strategy improvement algorithm as we know it. In: LICS, pp. 145–156 (2009)

    Google Scholar 

  24. Friedmann, O., Hansen, T.D., Zwick, U.: A subexponential lower bound for the random facet algorithm for parity games. In: SODA, pp. 202–216 (2011)

    Google Scholar 

  25. 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). doi:10.1007/978-3-642-04761-9_15

    Chapter  Google Scholar 

  26. Gimbert, H., Horn, F.: Solving simple stochastic games with few random vertices. LMCS 5(2:9), 1–17 (2009)

    MathSciNet  MATH  Google Scholar 

  27. Hahn, E.M. Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: CONCUR. LIPIcs, vol. 42, pp. 354–367 (2015)

    Google Scholar 

  28. Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Heidelberg (2014). doi:10.1007/978-3-319-06410-9_22

    Chapter  Google Scholar 

  29. Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: Synthesising strategy improvement, recursive algorithms for solving 2.5 player parity games. arXiv:1607.01474

  30. Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: A simple algorithm for solving qualitative probabilistic parity games. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 291–311. Springer, Heidelberg (2016). doi:10.1007/978-3-319-41540-6_16

    Chapter  Google Scholar 

  31. 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). doi:10.1007/3-540-46541-3_24

    Chapter  Google Scholar 

  32. Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SIAM J. Comput. 38(4), 1519–1532 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  33. Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains. D. Van Nostrand Company, Princeton (1966)

    MATH  Google Scholar 

  34. Kozen, D.: Results on the propositional \(\mu \)-calculus. TCS 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  35. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  36. Ludwig, W.: A subexponential randomized algorithm for the simple stochastic game problem. Inf. Comput. 117(1), 151–155 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  37. McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  38. Obdržálek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80–92. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_7

    Chapter  Google Scholar 

  39. Piterman, N.: From nondeterministic Büchi, Streett automata to deterministic parity automata. J. Log. Methods Comput. Sci. 3(3:5), 1–21 (2007)

    MathSciNet  MATH  Google Scholar 

  40. Puri, A.: Theory of hybrid systems and discrete event systems. Ph.D. thesis, Computer Science Department, University of California, Berkeley (1995)

    Google Scholar 

  41. Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 369–384. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87531-4_27

    Chapter  Google Scholar 

  42. Schewe, S.: Solving parity games in big steps. J. Comput. Syst. Sci. 84, 243–262 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  43. Schewe, S., Finkbeiner, B.: Satisfiability and finite model property for the alternating-time \(\mu \)-calculus. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 591–605. Springer, Heidelberg (2006). doi:10.1007/11874683_39

    Chapter  Google Scholar 

  44. Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 127–142. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71410-1_10

    Chapter  Google Scholar 

  45. Schewe, S., Trivedi, A., Varghese, T.: Symmetric strategy improvement. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 388–400. Springer, Heidelberg (2015). doi:10.1007/978-3-662-47666-6_31

    Google Scholar 

  46. Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998). doi:10.1007/BFb0055090

    Chapter  Google Scholar 

  47. Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games (Extended abstract). In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000). doi:10.1007/10722167_18

    Chapter  Google Scholar 

  48. Wilke, T.: Alternating tree automata, parity games, and modal \(\mu \)-calculus. Bull. Soc. Math. Belg. 8(2), 359 (2001)

    MathSciNet  MATH  Google Scholar 

  49. Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200(1–2), 135–183 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  50. Zielonka, W.: Perfect-information stochastic parity games. In: Walukiewicz, I. (ed.) FoSSaCS 2004. LNCS, vol. 2987, pp. 499–513. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24727-2_35

    Chapter  Google Scholar 

Download references

Acknowledgement

This work is supported by the National Natural Science Foundation of China (Grants Nos. 61472473, 61532019, 61550110249, 61550110506), by the National 973 Program (No. 2014CB340701), the CDZ project CAP (GZ 1023), the CAS Fellowship for International Young Scientists, the CAS/SAFEA International Partnership Program for Creative Research Teams, and the EPSRC grant EP/M027287/1.

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Science, Institute of Software, CAS, Beijing, China

    Ernst Moritz Hahn, Andrea Turrini & Lijun Zhang

  2. University of Liverpool, Liverpool, UK

    Sven Schewe

Authors
  1. Ernst Moritz Hahn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sven Schewe
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrea Turrini
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lijun Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sven Schewe .

Editor information

Editors and Affiliations

  1. IRIF, Université Paris Diderot, Paris, France

    Ahmed Bouajjani

  2. VERIMAG, CNRS & Université Grenoble Alpes, Grenoble, France

    David Monniaux

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Hahn, E.M., Schewe, S., Turrini, A., Zhang, L. (2017). Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-52234-0_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-52233-3

  • Online ISBN: 978-3-319-52234-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation