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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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)
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
Biere, A.: μcke – efficient μ-calculus model checking. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 468–471. Springer, Heidelberg (1997)
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)
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)
Bryant, R.E.: Symbolic manipulation of Boolean functions using a graphical representation. In: ACM/IEEE Design Automation Conference, pp. 688–694 (1985)
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)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal μ-calculus. Theoretical Computer Science 663, 410–422 (1992)
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)
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)
Edelkamp, S.: Symbolic exploration in two-player games: Preliminary results. In: AIPS-Workshop on Model Checking, pp. 40–48 (2002)
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)
Edelkamp, S., Kissmann, P.: Symbolic exploration for general game playing in PDDL. In: ICAPS-Workshop on Planning in Games (2007)
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)
Emerson, E.A., Jutla, C.S.: Tree automata μ-calculus and determinacy. In: Foundations of Computer Science, pp. 368–377 (1991)
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)
Genesereth, M.R.: Knowledge interchange format. In: Second International Conference on Principles of Knowledge Representation and Reasoning, pp. 238–249 (1991)
Helmert, M.: A planning heuristic based on causal graph analysis. In: International Conference on Automated Planning and Scheduling, pp. 161–170 (2004)
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)
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)
Jurdzinski, M.: Deciding the winner in parity games is UP∩co-UP. Information Processing Letters 68(3), 119–124 (1998)
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)
Jurdzinski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: SODA, pp. 117–123 (2006)
Kautz, H., Selman, B.: Pushing the envelope: Planning propositional logic, and stochastic search. In: European Conference on Artificial Intelligence, pp. 1194–1201 (1996)
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)
Madhusudan, P., Nam, W., Alur, R.: Symbolic computational techniques for solving games. Electronic Notes in Theoretical Computer Science 89(4) (2004)
McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65, 129–284 (1993)
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)
Schewe, S.: Solving parity games in big steps. In: CAV, pp. 449–460 (2007)
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)
Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. STTT 5(2-3), 185–204 (2004)
Seidl, H.: Fast and simple nested fixpoints. Information Processing Letters 59(6), 119–124 (1996)
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)
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)
Stirling, C.: Local model checking games. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)
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)
van de Pol, J., Weber, M.: A multi-core solver for parity games. In: PDMC 2008 (to appear, 2008)
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)
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)
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)
Yoo, H.: Fehlerdiagnose beim Model-Checking durch animierte Strategiesynthese. PhD thesis, Universität Dortmund (2007)
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)
Zielonka, W.: Infinite games on finite coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200, 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)