Practical model-checking using games

We describe how model-checking games can be the foundation for efficient local model-checking of the modal mu-calculus on transition systems. Game-based algorithms generate winning strategies for a certain game, which can then be used interactively to help the user understand why 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 to one which we have implemented in the Edinburgh Concurrency Workbench. We discuss its usability and performance.