Abstract
The coupled simulation equivalence is slightly larger than observation equivalence. Where observation equivalence is based on weak bisimulations, coupled simulation equivalence is based on pairs of simulations which coincide at stable states. We establish the corresponding congruence and provide a complete axiomatization by adding a new Τ-law, Τ.(Τ. P + Q) = Τ. P + Q, to the axiomatization of observation congruence. We further indicate how the definition of the equivalence can be extended to divergent transition systems.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Cleaveland, J. Parrow, and B. Steffen. A semantics-based verification tool for finitestate systems. In E. Brinksma, G. Scollo, and C. A. Vissers, editors, Protocol Specification, Testing, and Verification, IX, pages 287–302. North-Holland, 1989.
M. Hennessy. Algebraic Theory of Processes. The MIT Press, 1988.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1980.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
J. Parrow and P. Sjödin. Multiway synchronization verified with coupled simulation. In W. R. Cleaveland, editor, Proceedings of CONCUR '92, volume 630 of Lecture Notes in Computer Science, pages 518–533. Springer-Verlag, 1992.
J. Parrow and P. Sjödin. The complete axiomatization of cs-congruence. Research report, Swedish Institute of Computer Science, 1994. In preparation.
R. J. van Glaabeek. De semantiek van eidige, sequentiËle processes met interne acties. Syllabus processemantieken, deel 2. Handwritten manuscript, in Dutch, 1988.
R. J. van Glaabeek. The linear time — branching time spectrum II. In E. Best, editor, Proceedings of CONCUR '93, volume 715 of Lecture Notes in Computer Science, pages 66–80. Springer-Verlag, 1993.
R. J. van Glabbeek. Comparative Concurrency Semantics and Refinement of Actions. PhD thesis, Free University of Amsterdam, The Netherlands, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Parrow, J., Sjödin, P. (1994). The complete axiomatization of Cs-congruence. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds) STACS 94. STACS 1994. Lecture Notes in Computer Science, vol 775. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57785-8_171
Download citation
DOI: https://doi.org/10.1007/3-540-57785-8_171
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57785-0
Online ISBN: 978-3-540-48332-8
eBook Packages: Springer Book Archive