Abstract
In this paper the question is considered in which cases a transition system specification in Plotkin style has ‘good’ properties and deserves the predicate ‘structured’. 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. We argue that in this setting it is natural to require that strong bisimulation equivalence is a congruence on the states of the transition systems. A general format, called the tyft/tyxt format, is presented for the conditional rules in a transition system specification, such that bisimulation is always a congruence when all the rules fit into this format. With a series of examples it is demonstrated that the tyft/tyxt format cannot be generalized in any obvious way. Briefly we touch upon the issue of modularity of transition system specifications. We show that certain pathological tyft/tyxt rules (the ones which are not pure) can be disqualified because they behave badly with respect to modularisation. 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 [16, 17] but is incomparable to the GSOS format of Bloom, Istrail & Meyer [7]. However, it turns out that 2-nested simulation equivalence strictly refines the completed trace congruence induced by the GSOS format.
The research of the authors was supported by ESPRIT project no. 432, An Integrated Formal Approach to Industrial Software Development (METEOR), and by RACE project no. 1046, Specification and Programming Environment for Communication Software (SPECS). A full version of this paper appeared as [9]. There also the proofs can be found which have been omitted here.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky (1987): Observation equivalence as a testing equivalence. Theoretical Computer Science 53, pp. 225–241.
J.C.M. Baeten & R.J. van Glabbeek (1987): Merge and termination in process algebra. In: Proceedings 7th Conference on Foundations of Software Technology & Theoretical Computer Science, Pune, India (K.V. Nori, ed.), LNCS 287, Springer-Verlag, pp. 153–172.
J.C.M. Baeten & F.W. Vaandrager (1989): An algebra for process creation. Report CSR89.., Centrum voor Wiskunde en Informatica, Amsterdam, to appear.
J.W. de Bakker & J.N. Kok (1988): Uniform abstraction, atomicity and contractions in the comparative semantics of concurrent Prolog. In: Proceedings Fifth Generation Computer Systems 1988 (FGCS'88), Tokyo, Japan.
J.A. Bergstra & J.W. Klop (1988): A complete inference system for regular processes with silent moves. In: Proceedings Logic Colloquium 1986 (F.R. Drake & J.K. Truss, eds.), North Holland, Hull, pp. 21–81, also appeared as: Report CS-R8420, Centrum voor Wiskunde en Informatica, Amsterdam 1984.
B. Bloom (November 1988): Personal communication.
B. Bloom, S. Istrail & A.R. Meyer (1988): Bisimulation can't be traced: preliminary report. In: Conference Record of the 15th ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pp. 229–239.
R.J. van Glabbeek (1987): Bounded nondeterminism and the approximation induction principle in process algebra. In: Proceedings STACS 87 (F.J. Brandenburg, G. Vidal-Naquet & M. Wirsing, eds.), LNCS 247, Springer-Verlag, pp. 336–347.
J.F. Groote & F.W. Vaandrager (1988): Structured operational semantics and bisimulation as a congruence. Report CS-R8845, Centrum voor Wiskunde en Informatica, Amsterdam.
M. Hennessy & R. Milner (1985): Algebraic laws for nondeterminism and concurrency. JACM 32(1), pp. 137–161.
R. Milner (1980): A Calculus of Communicating Systems, LNCS 92, Springer-Verlag.
R. Milner (1983): Calculi for synchrony and asynchrony. Theoretical Computer Science 25, pp. 267–310.
D.M.R. Park (1981): Concurrency and automata on infinite sequences. In: Proceedings 5th GI Conference (P. Deussen, ed.), LNCS 104, Springer-Verlag, pp. 167–183.
G.D. Plotkin (1981): A Structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University.
G.D. Plotkin (1983): An operational semantics for CSP. In: Proceedings IFIP TC2 Working Conference on Formal Description of Programming Concepts — II, Garmish, 1982 (D. Bjørner, ed.), North-Holland, Amsterdam, pp. 199–225.
R. de Simone (1984): Calculabilité et expressivité dans l'algebra de processus parallèles Meije. Thèse de 3e cycle, Univ. Paris 7.
R. de Simone (1985): Higher-level synchronising devices inMeije-SCCS, Theoretical Computer Science 37, pp. 245–267.
J.L.M. Vrancken (1986): The algebra of communicating processes with empty process. Report FVI 86-01, Dept. of Computer Science, University of Amsterdam.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Groote, J.F., Vaandrager, F. (1989). Structured operational semantics and bisimulation as a congruence. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds) Automata, Languages and Programming. ICALP 1989. Lecture Notes in Computer Science, vol 372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035774
Download citation
DOI: https://doi.org/10.1007/BFb0035774
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51371-1
Online ISBN: 978-3-540-46201-9
eBook Packages: Springer Book Archive