Practical model-checking using games

Perdita Stevens, Colin Stirling

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication4th 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
EditorsBernhard Steffen
PublisherSpringer-Verlag GmbH
Number of pages17
ISBN (Electronic)978-3-540-69753-4
ISBN (Print)978-3-540-64356-2
Publication statusPublished - 1998

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'Practical model-checking using games'. Together they form a unique fingerprint.

Cite this