Skip to main content
SpringerLink
Log in

Improving Parity Game Solvers with Justifications

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

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

Abstract

Parity games are infinite two-player games played on node-weighted directed graphs. Formal verification problems such as verifying and synthesizing automata, bounded model checking of LTL, CTL*, propositional \(\mu \)-calculus, ... reduce to problems over parity games. The core problem of parity game solving is deciding the winner of some (or all) nodes in a parity game. In this paper, we improve several parity game solvers by using a justification graph. Experimental evaluation shows our algorithms improve upon the state-of-the-art.

R. Lapauw—Supported by a IWT research grant.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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.

    To make \( strategy _\alpha \) deterministic, choose can return, e.g., the smallest element.

  2. 2.

    Choosing \(v_9\) as winning move for \(v_6\) never resets node \(v_6\), avoiding the difficulties of Example 1.

  3. 3.

    The benchmarks can be reproduced in the VMCAI 2020 virtual machine (https://doi.org/10.5281/zenodo.3533104) with the artifact at https://doi.org/10.5281/zenodo.3510292.

References

  1. Benerecetti, M., Dell’Erba, D., Mogavero, F.: Improving priority promotion for parity games. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 117–133. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49052-6_8

    Chapter  Google Scholar 

  2. Benerecetti, M., Dell’Erba, D., Mogavero, F.: Solving parity games via priority promotion. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 270–290. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_15. ISBN 978-3-319-41539-0

    Chapter  Google Scholar 

  3. Bruse, F., Falk, M., Lange, M.: The fixpoint-iteration algorithm for parity games. In: Peron, A., Piazza, C. (eds.) Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014. EPTCS, Verona, Italy, 10–12 September 2014, vol. 161, pp. 116–130 (2014)

    Article  MathSciNet  Google Scholar 

  4. Calude, C.S., et al.: Deciding parity games in quasipolynomial time. In: Hatami, H., McKenzie, P., King, V. (eds.) Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, 19–23 June 2017, pp. 252–263. ACM (2017). ISBN 978-1-4503-4528-6

    Google Scholar 

  5. Cranen, S., et al.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199–213. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_15. ISBN 978-3-642-36742-7

    Chapter  Google Scholar 

  6. Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: Proceedings of the Symposium on Logic in Computer Science (LICS 1986), Cambridge, Massachusetts, USA, 16–18 June 1986. IEEE Computer Society, pp. 267–278 (1986). ISBN 0-8186-0720-3

    Google Scholar 

  7. Fearnley, J., et al.: An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In: Erdogmus, H., Havelund, K. (eds.) Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, 10–14 July 2017, pp. 112–121. ACM (2017). ISBN 978-1-4503-5077-8

    Google Scholar 

  8. 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). https://doi.org/10.1007/978-3-642-04761-9_15. ISBN 978-3-642-04760-2

    Chapter  Google Scholar 

  9. Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers. University of Munich (2009)

    Google Scholar 

  10. Grädel, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36387-4. ISSN 3-540-00388-5

    Book  MATH  Google Scholar 

  11. Hou, P., De Cat, B., Denecker, M.: FO(FD): extending classical logic with rule-based fixpoint definitions. TPLP 10(4–6), 581–596 (2010)

    MathSciNet  MATH  Google Scholar 

  12. 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). https://doi.org/10.1007/3-540-46541-3_24. ISBN 3-540-67141-1

    Chapter  Google Scholar 

  13. Kant, G., van de Pol, J.: Efficient instantiation of parameterised Boolean equation systems to parity games. In: Wijs, A., Bosnacki, D., Edelkamp, S. (eds.) Proceedings First Work-Shop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2012. EPTCS, Tallinn, Estonia, 1st April 2012, vol. 99, pp. 50–65 (2012)

    Article  Google Scholar 

  14. Keiren, J.J.A.: Benchmarks for parity games. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 127–142. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24644-4_9. ISBN 978-3-319-24643-7

    Chapter  Google Scholar 

  15. Long, D.E., Browne, A., Clarke, E.M., Jha, S., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 338–350. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58179-0_66. ISBN 3-540-58179-6

    Chapter  Google Scholar 

  16. 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). https://doi.org/10.1007/978-3-540-87531-4_27. ISBN 978-3-540-87530-7

    Chapter  Google Scholar 

  17. Seidl, H.: Fast and simple nested fixpoints. Inf. Process. Lett. 59(6), 303–308 (1996)

    Article  MathSciNet  Google Scholar 

  18. Dijk, T.: Attracting tangles to solve parity games. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 198–215. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_14. ISBN 978-3-319-96141-5

    Chapter  Google Scholar 

  19. Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 291–308. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_16. ISBN 978-3-319-89959-6

    Chapter  Google Scholar 

  20. Walukiewicz, I.: Monadic second-order logic on tree-like structures. Theor. Comput. Sci. 275(1–2), 311–346 (2002)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, KU Leuven, 3001, Leuven, Belgium

    Ruben Lapauw, Maurice Bruynooghe & Marc Denecker

Authors
  1. Ruben Lapauw
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maurice Bruynooghe
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marc Denecker
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ruben Lapauw .

Editor information

Editors and Affiliations

  1. Ludwig-Maximilians-Universität München, Munich, Germany

    Dirk Beyer

  2. Max Planck Institute for Software Systems, Kaiserslautern, Rheinland-Pfalz, Germany

    Damien Zufferey

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lapauw, R., Bruynooghe, M., Denecker, M. (2020). Improving Parity Game Solvers with Justifications. In: Beyer, D., Zufferey, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2020. Lecture Notes in Computer Science(), vol 11990. Springer, Cham. https://doi.org/10.1007/978-3-030-39322-9_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-39322-9_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-39321-2

  • Online ISBN: 978-3-030-39322-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation