Abstract
Equivalence games have been shown as an efficient way to diagnose design systems. Nevertheless, like other diagnostic routines, equivalence games utilize the information already computed by equivalence checker during verification. Therefore, these diagnostic routines tightly gear to the data structure of checker being used, and their ability of migrating to a different checker is not always guaranteed. Moreover, different equivalence relations demand different game schemas, which makes it tedious to implement equivalence games. We solve the first problem by utilizing a generalized version of partition refinement tree (PRT) as an abstract of proof structures. With a little bookkeeping, a partition refinement-based checker is able to supply PRT as the evidence to support its result. The diagnostic routines built on PRTs are independent of equivalence checkers being used. PRTs may also be used to certify the equivalence-checking result.
To solve the second problem, we introduce a semantics hierarchy. Implementation following this hierarchy enjoys greater code sharing among different games. The prototype of this schema, including PRT-friendly algorithms and the architecture of semantics hierarchy, has been implemented on the Concurrency Workbench.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
R. Cleaveland and M. C. B. Hennessy. Testing equivalence as a bisimulation equivalence. Formal Aspects of Computing, 5:1–20, 1993.
R. Cleaveland and S. Sims. The NCSU concurrency workbench. In R. Alurand T. A. Henzinger, editors, Computer Aided Verification (CAV’ 96), volume 1102 of Lecture Notes in Computer Science, pages 394–397, New Brunswick, New Jersey, July 1996. Springer-Verlag.
J.-C. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Sicence of Computer Programming, 13:219–236, 1989/90.
M. C. B. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, January 1985.
P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. In Proceedings of the 2nd ACM Symposium on the Principles of Distributed Computing, Montreal, Canada, August 1983.
M. Main. Trace, failure and testing equivalences for communication, concurrency, and time. International Journal of Parallel Programming, 16(5):383–400, 1987.
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal of Computing, 16(6):973–989, December 1987.
C. Stirling. Modal logics for communicating systems. Theoretical Computer Science, 49:311–347, 1987.
C. Stirling. Games and modal μ-calculus. In Proceedings of the Third International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 1996.
L. Tan and R. Cleaveland. Simulation revisited. In The 7-th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 480–495. Springer-Verlag, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tan, L. (2002). An Abstract Schema for Equivalence-Checking Games. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_5
Download citation
DOI: https://doi.org/10.1007/3-540-47813-2_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43631-7
Online ISBN: 978-3-540-47813-3
eBook Packages: Springer Book Archive