Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Model Checking and Artificial Intelligence

MoChArt 2008: Model Checking and Artificial Intelligence pp 15–33Cite as

Solving μ-Calculus Parity Games by Symbolic Planning

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5348))

Abstract

This paper applies symbolic planning to solve parity games equivalent to μ-calculus model checking problems. Compared to explicit algorithms, state sets are compacted during the analysis. Given that \(\mbox{\it diam}(G)\) is the diameter of the parity game graph G with node set V, for the alternation-free model checking problem with at most one fixpoint operator, the algorithm computes at most \(O(\mbox{\it diam}(G))\) partitioned images. For d alternating fixpoint operators, \(O(d \cdot \mbox{\it diam}(G) \cdot (\frac{|V|+(d-1)}{d-1})^{d-1})\) partitioned images are required in the worst case.

Practical models and properties stem from data-flow analysis, with problems transformed to parity game graphs, which are then compiled to a general game playing planner input.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bakera, M., Margaria, T., Renner, C.D., Steffen, B.: Game-based model checking for reliable autonomy in space. Journal of the American Institute of Aeronautics and Astronautics (AIAA) (to appear)

    Google Scholar 

  2. Bakera, M., Margaria, T., Renner, C.D., Steffen, B.: Verification, diagnosis and adaptation: Tool supported enhancement of the model-driven verification process. In: Revue des Nouvelles Technologies de Information (RNTI-SM-1), pp. 85–98 (to appear) ISBN 2854288148

    Google Scholar 

  3. Biere, A.: μcke – efficient μ-calculus model checking. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 468–471. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  4. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. Tools and Algorithms for the Construction and Analysis of Systems (1999)

    Google Scholar 

  5. Björklund, H., Sandberg, S., Vorobyov, S.G.: A discrete subexponential algorithm for parity games. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 663–674. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Bryant, R.E.: Symbolic manipulation of Boolean functions using a graphical representation. In: ACM/IEEE Design Automation Conference, pp. 688–694 (1985)

    Google Scholar 

  7. Bustan, D., Kupferman, O., Vardi, M.Y.: A measured collapse of the modal μ-calculus alternation hierarchy. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol. 2996, pp. 522–533. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  9. Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal μ-calculus. Theoretical Computer Science 663, 410–422 (1992)

    Google Scholar 

  10. Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design 2(2), 121–147 (1993)

    Article  MATH  Google Scholar 

  11. de Alfaro, L., Faella, M.: An accelerated algorithm for 3-color parity games with an application to timed games. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 108–120. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Edelkamp, S.: Symbolic exploration in two-player games: Preliminary results. In: AIPS-Workshop on Model Checking, pp. 40–48 (2002)

    Google Scholar 

  13. Edelkamp, S., Helmert, M.: Exhibiting knowledge in planning problems to minimize state encoding length. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 135–147. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  14. Edelkamp, S., Kissmann, P.: Symbolic exploration for general game playing in PDDL. In: ICAPS-Workshop on Planning in Games (2007)

    Google Scholar 

  15. Edelkamp, S., Kissmann, P.: Symbolic classification of general two-player games. In: Dengel, A.R., Berns, K., Breuel, T.M., Bomarius, F., Roth-Berghofer, T.R. (eds.) KI 2008. LNCS, vol. 5243, pp. 185–192. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Emerson, E.A., Jutla, C.S.: Tree automata μ-calculus and determinacy. In: Foundations of Computer Science, pp. 368–377 (1991)

    Google Scholar 

  17. Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Symposium on Logic in Computer Science, pp. 267–278 (1986)

    Google Scholar 

  18. Genesereth, M.R.: Knowledge interchange format. In: Second International Conference on Principles of Knowledge Representation and Reasoning, pp. 238–249 (1991)

    Google Scholar 

  19. Helmert, M.: A planning heuristic based on causal graph analysis. In: International Conference on Automated Planning and Scheduling, pp. 161–170 (2004)

    Google Scholar 

  20. Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  21. Jørges, S., Kubczak, C., Pageau, F., Margaria, T.: Model driven design of reliable robot control programs using the jabc. In: 4th IEEE International Workshop on Engineering of Autonomic and Autonomous Systems (EASe), March 2007, pp. 137–148 (2007)

    Google Scholar 

  22. Jurdzinski, M.: Deciding the winner in parity games is UP∩co-UP. Information Processing Letters 68(3), 119–124 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  23. Jurdzinski, 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)

    Chapter  Google Scholar 

  24. Jurdzinski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: SODA, pp. 117–123 (2006)

    Google Scholar 

  25. Kautz, H., Selman, B.: Pushing the envelope: Planning propositional logic, and stochastic search. In: European Conference on Artificial Intelligence, pp. 1194–1201 (1996)

    Google Scholar 

  26. Love, N.C., Hinrichs, T.L., Genesereth, M.R.: General game playing: Game description language specification. Technical Report LG-2006-01, Stanford Logic Group (April 2006)

    Google Scholar 

  27. Madhusudan, P., Nam, W., Alur, R.: Symbolic computational techniques for solving games. Electronic Notes in Theoretical Computer Science 89(4) (2004)

    Google Scholar 

  28. McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65, 129–284 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  29. Schaeffer, J., Björnsson, Y., Burch, N., Kishimoto, A., Müller, M., Lake, R., Lu, P., Sutphen, S.: Solving checkers. In: International Joint Conference on Artificial Intelligence, pp. 292–297 (2005)

    Google Scholar 

  30. Schewe, S.: Solving parity games in big steps. In: CAV, pp. 449–460 (2007)

    Google Scholar 

  31. Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: Conference Record of POPL 1998: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, Janary 19–21, 1998, pp. 38–48 (1998)

    Google Scholar 

  32. Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. STTT 5(2-3), 185–204 (2004)

    Article  Google Scholar 

  33. Seidl, H.: Fast and simple nested fixpoints. Information Processing Letters 59(6), 119–124 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  34. Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–365. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  35. Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  36. Stirling, C.: Local model checking games. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  37. Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  38. van de Pol, J., Weber, M.: A multi-core solver for parity games. In: PDMC 2008 (to appear, 2008)

    Google Scholar 

  39. Vöge, J., Jurdzinski, M.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  40. Vöge, J., Ulbrand, S., Matz, O., Buhrke, N.: The automata theory package omega. In: Wood, D., Yu, S. (eds.) WIA 1997. LNCS, vol. 1436, pp. 228–231. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  41. Wallmeier, N., Hütten, P., Thomas, W.: Symbolic synthesis of finite-state controllers for request-response specifications. In: H. Ibarra, O., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 11–22. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  42. Yoo, H.: Fehlerdiagnose beim Model-Checking durch animierte Strategiesynthese. PhD thesis, Universität Dortmund (2007)

    Google Scholar 

  43. Yoo, H., Müller-Olm, M.: MetaGame: An animation tool for model-checking games. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 163–167. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  44. Zielonka, W.: Infinite games on finite coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200, 135–183 (1998)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Dortmund University of Technology, Germany

    Marco Bakera, Stefan Edelkamp, Peter Kissmann & Clemens D. Renner

Authors
  1. Marco Bakera
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Edelkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Kissmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Clemens D. Renner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Bar Ilan University, 52900, Ramat Gan, Israel

    Doron A. Peled

  2. Department of Computer Science, University of Liverpool, L69 3BX, Liverpool, UK

    Michael J. Wooldridge

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bakera, M., Edelkamp, S., Kissmann, P., Renner, C.D. (2009). Solving μ-Calculus Parity Games by Symbolic Planning. In: Peled, D.A., Wooldridge, M.J. (eds) Model Checking and Artificial Intelligence. MoChArt 2008. Lecture Notes in Computer Science(), vol 5348. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00431-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-00431-5_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-00430-8

  • Online ISBN: 978-3-642-00431-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation