Model-checking for adventure videogames

This paper describes a model-checking approach for adventure games focusing on 〈e-Adventure〉, a platform for the development of adaptive educational adventure videogames. In 〈e-Adventure〉, games are described using a domain-specific language oriented to game writers. By defining a translation from this language to suitable state-based models, it is possible to automatically extract a verification model for each 〈e-Adventure〉 game. In addition, temporal properties to be verified are described using an extensible assertion language, which can be tailored to each specific application scenario. When the framework determines that some of these properties do not hold, it generates an animation of a counterexample. This approach facilitates the collaboration of multidisciplinary teams of experts during the verification of the integrity of the game scripts, exchanging hours of manual verification for semi-automatic verification processes that also facilitate the diagnosis of the conditions that may potentially break the games.