Structured operational semantics and bisimulation as a congruence. (English) Zbl 0752.68053

Summary: We are interested in general properties of classes of transition system specifications in Plotkin style. The discussion takes place in a setting of labelled transition systems. The states of the transition systems are terms generated by a single sorted signature and the transitions between states are defined by conditional rules over the syntax. It is argued that in this setting it is natural to require that strong bisimulation equivalence be a congruence on the states of the transition systems. A general format, called the \(tyft/tyxt\) format, is presented for the rules in a transition system specification, such that bisimulation is always a congruence when all the rules fit this format. With a series of examples it is demonstrated that the \(tyft/tyxt\) format cannot be generalized in any obvious way. Another series of examples illustrates the usefulness of our congruence theorem. Briefly we touch upon the issue of modularity of transition system specifications. It is argued that certain pathological \(tyft/tyxt\) rules (the ones which are not pure) can be disqualified because they behave badly with respect to modularization. Next we address the issue of full abstraction. We characterize the completed trace congruence induced by the operators in pure \(tyft/tyxt\) format as 2- nested simulation equivalence. The pure \(tyft/tyxt\) format includes the format given by de Simone [Theoret. Comput. Sci. 37, 245-267 (1985)] but is incomparable to the GSOS format of Bloom, Istrail, and Meyer [in “Conference record of the 15th Annual Symposium on Principles of Programming Languages, San Diego, California, 1988”, pp. 229-239). However, it turns out that 2-nested simulation equivalence strictly refines the completed trace congruence induced by the GSOS format.


68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI Link


[1] Abramsky, S., Observation equivalence as a testing equivalence, Theoret. comput. sci., 53, 225-241, (1987) · Zbl 0626.68016
[2] America, P.; de Bakker, J.W.; Kok, J.N.; Rutten, J.J.M.M., Operational semantics of a parallel object-oriented language, (), 194-208
[3] Baeten, J.C.M.; Bergstra, J.A., Global renaming operators in concrete process algebra, Inform. and comput., 78, 205-245, (1988) · Zbl 0651.68031
[4] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., Syntax and defining equations for an interrupt mechanism in process algebra, Fund. inform., 9, No. 2, 127-168, (1986) · Zbl 0617.68027
[5] Baeten, J.C.M.; van Glabbeek, R.J., Merge and termination in process algebra, (), 153-172 · Zbl 0636.68024
[6] de Bakker, J.W.; Kok, J.N., Uniform abstraction, atomicity and contractions in the comparative semantics of concurrent prolog, (), 347-355
[7] Bergstra, J.A.; Klop, J.W.; Bergstra, J.A.; Klop, J.W., A complete inference system for regular processes with silent moves, (), 21, Amsterdam · Zbl 0647.68033
[8] Bergstra, J.A.; Klop, J.W.; Olderog, E.-R., Readies and failures in the algebra of communicating processes, SIAM J. comput., 17, No. 6, 1134-1177, (1988) · Zbl 0677.68089
[9] {\scBloom, B}. (November 1988), personal communication.
[10] Bloom, B.; Istrail, S.; Meyer, A.R., Bisimulation can’t be traced: preliminary report, (), 229-239, Full version appeared as
[11] Boudol, G., Notes on algebraic calculi of processes, (), 261-303 · Zbl 0578.68025
[12] Cleaveland, R.; Hennessy, M., Priorities in process algebra, (), 193-202
[13] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. comput. sci., 34, 83-133, (1984) · Zbl 0985.68518
[14] van Glabbeek, R.J., Bounded nondeterminism and the approximation induction principle in process algebra, (), 336-347 · Zbl 0612.68025
[15] {\scvan Glabbeek, R. J.} (November 1988), personal communication.
[16] van Glabbeek, R.J.; Vaandrager, F.W., Petri net models for algebraic theories of concurrency, (), 224-242, Lecture Notes in Computer Science, Vol. 259
[17] Groote, J.F., (), extended abstract
[18] in “Proceedings, CONCUR 90, Amsterdam” (J. C. M. Baeten and J. W. Klop, Eds.), pp. 332-341, Lecture Notes in Computer Science, Vol. 458, Springer-Verlag, Berlin/New York.
[19] Hennessy, M., ()
[20] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. assoc. comput. Mach., 32, 1, 137-161, (1985) · Zbl 0629.68021
[21] Keller, R.M., Formal verification of parallel programs, Comm. ACM, 19, 7, 371-384, (1976) · Zbl 0329.68016
[22] Klop, J.W., Term rewriting systems: A tutorial, Bull. European assoc. theoret. comput. sci., 32, 143-182, (1987) · Zbl 0666.68025
[23] Larsen, K.G.; Skou, A., Bisimulation through probabilistic testing, (), 344-352 · Zbl 0756.68035
[24] Milner, R., (), Lecture Notes in Computer Science
[25] Milner, R., Modal characterization of observable machine behaviour, (), 25-34
[26] Milner, R., Calculi for synchrony and asynchrony, Theoret. comput. sci., 25, 267-310, (1983) · Zbl 0512.68026
[27] Milner, R., ()
[28] Olderog, E.-R.; Hoare, C.A.R., Specification-oriented semantics for communicating processes, Acta informat., 23, 9-66, (1986) · Zbl 0569.68019
[29] Park, D.M.R., Concurrency and automata on infinite sequences, (), 167-183
[30] Plotkin, G.D., (), Technical Report DAIMI FN-19
[31] Plotkin, G.D., An operational semantics for CSP, (), 199-225 · Zbl 0512.68012
[32] Pnueli, A., Linear and branching structures in the semantics and logics of reactive systems, (), 15-32
[33] de Simone, R., Calculabilité et expressivité dans l’algèbre de processus parallèles meije, ()
[34] de Simone, R., Higher-level synchronising devices in meije-SCCS, Theoret. comput. sci., 37, 245-267, (1985) · Zbl 0598.68027
[35] Unix, ()
[36] Vrancken, J.L.M., (), Report FVI 86-01
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.