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.
|Title of host publication||Tools and Algorithms for the Construction and Analysis of Systems|
|Subtitle of host publication||4th International Conference, TACAS'98 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98 Lisbon, Portugal, March 28 – April 4, 1998 Proceedings|
|Number of pages||17|
|Publication status||Published - 1998|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|