Practical model-checking using games

Abstract

We describe how model-checking games can be the foundationfor efficient local model-checking of the modal mu-calculus on transitionsystems. Game-based algorithms generate winning strategies for acertain game, which can then be used interactively to help the user understandwhy the property is or is not true of the model. This kind of feedback has advantages over traditional techniques such as error traces.We give a proof technique for verifying such algorithms, and apply it toone which we have implemented in the Edinburgh Concurrency Workbench.We discuss its usability and performance.