MetaGame: An Animation Tool for Model-Checking Games

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.

• Type: Conference
• Year: 2004
• Where: TACAS
• Authors: Markus Müller-Olm, Haiseung Yoo
• Keywords: Algorithms, Error Diagnosis Information, Model Checking, Model Checking Games, TACAS 2004