Abstract
Failing model checking runs should be accompanied by appropriate error diagnosis information that allows the user to identify the cause of the problem. For branching time logics error diagnosis information can be given by a winning strategy in a graph game derived from the model checking instance. However, winning strategies as such are hard to grasp. In this paper we describe the MetaGame tool that computes and animates winning strategies for modal μ-calculus model checking games on finite graphs. MetaGame allows the user to play model checking games in a GUI interface thus making winning strategies more accessible.
Chapter PDF
Similar content being viewed by others
References
Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal mu-calculus. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 410–422. Springer, Heidelberg (1993)
Metaframe homepage, http://ls5-www.cs.uni-dortmund.de/projects/METAFrame/
Spin homepage, http://spinroot.com/spin/whatispin.html
Stirling, C.: Local model checking games. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)
Stirling, C., Stevens, P.: Practical model-checking using games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 85–101. Springer, Heidelberg (1998)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller-Olm, M., Yoo, H. (2004). MetaGame: An Animation Tool for Model-Checking Games. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive