Abstract
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.
supported by EPSRC GR/K68547
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andersen, H. (1994). Model checking and boolean graphs. Theoretical Comp. Science, 126, 3–30.
Bernholtz, O., Vardi, M. and Wolper, P. (1994). An automata-theoretic approach to branching-time model checking. Lecture Notes in Computer Science, 818, 142–155.
Emerson, E., Jutla, C, and Sistla, A. (1993). On model checking for fragments of Μ-calculus. Lecture Notes in Computer Science, 697, 385–396.
Long, D., Browne, A., Clarke, E., Jha, S., and Marrero, W. (1994) An improved algorithm for the evaluation of fixpoint expressions. Lecture Notes in Computer Science, 818, 338–350.
Mader, A. (1996) Verification of Modal Properties Using Boolean Equation Systems. Doctoral dissertation, Institut für Informatik, Technische Universität München.
Milner, R. (1989) Communication and Concurrency Prentice Hall
Moller, F. and Stevens, P. (1996). The Edinburgh Concurrency Workbench user manual. http://www.dcs.ed.ac.uk/home/cwb.
Stirling, C. (1995). Local model checking games. Lecture Notes in Computer Science, 962, 1–11.
Stirling, C. (1996). Modal and temporal logics for processes. Lecture Notes in Computer Science, 1043, 149–237.
Stirling, C. and Walker, D. (1991) Local model checking in the modal mu-calculus. Theoretical Computer Science, 89, 161–177.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stevens, P., Stirling, C. (1998). Practical model-checking using games. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054166
Download citation
DOI: https://doi.org/10.1007/BFb0054166
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive