Abstract
We introduce an integrated tool for implementing and playing various diagnostic games. The tool uses a semantics hierarchy introduced in [6] to improve code sharing among various diagnostic games and reduce the cost of introducing a new game. PlayGame synthesizes the winning strategy using the evidence that is an abstract and uniform encoding of the proof computed by a checker, and hence instead of relying on any particular checker the tool works on a variety of checkers that can be extended to produce such evidence. PlayGame implements a μ-calculus game and a full range of equivalence/preorder games on the Concurrency Workbench-New Century (CWB-NC).
Chapter PDF
Similar content being viewed by others
References
The Edinburgh Concurrency Workbench. The University of Edinburgh (1999)
Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Leucker, M., Noll, T.: Truth/SLC — A parallel verification platform for concurrent systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 255. Springer, Heidelberg (2001)
Stevens, P., Stirling, C.: Practical model-checking using games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 85. Springer, Heidelberg (1998)
Stirling, C.: Games and modal mu-calculus. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, Springer, Heidelberg (1996)
Tan, L.: An abstract schema for equivalence games. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, p. 65. Springer, Heidelberg (2002)
Tan, L.: Evidence-based Verification. PhD thesis, State University of New York at Stony Brook (May 2002)
Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 455. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tan, L. (2004). PlayGame: A Platform for Diagnostic Games. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_44
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive