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.
Keywords for this software
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Saitoh, Akira; Rahimi, Robabeh; Nakahara, Mikio: Yet another framework for quantum simultaneous noncooperative bimatrix games (2009)
- SaiToh, Akira; Rahimi, Robabeh; Nakahara, Mikio: Quantum metagame extensions of noncooperative bimatrix games (2009)
- Bajohr, Markus; Margaria, Tiziana: MaTRICS: a service-based management tool for remote intelligent configuration of systems (2006) ioport
- Müller-Olm, Markus; Yoo, Haiseung: MetaGame: an animation tool for model-checking games (2004)
- Takahashi, Wataru (ed.): Nonlinear analysis and convex analysis. Proceedings of a symposium held at the Research Institute for Mathematical Sciences, Kyoto University, Kyoto, Japan, August 28--30, 2001 (2002)
- Wang, Shou Yang; Li, Zhong Fei: Paréto equilibria in multicriteria metagames (1995)
- Selbirak, Tadeusz: Some concepts of non-myopic equilibria in games with finite strategy sets and their properties (1994)
- Baye, Michael R.; Kovenock, Dan; de Vries, Casper G.: It takes two to tango: equilibria in a model of sales (1992)
- Gmytrasiewicz, Piotr J.; Durfee, Edmund H.; Wehe, David K.: A decision-theoretic approach to coordinating multiagent interactions (1991)