Journal of the ACM Bibliography

Abstract

In the concurrent language CCS, two programs are considered the same if they are bisimilar. Several years and many researchers have demonstrated that the theory of bisimulation is mathematically appealing and useful in practice. However, bisimulation makes too many distinctions between programs. We consider the problem of adding operations to CCS to make bisimulation fully abstract. We define the class of GSOS operations, generalizing the style and technical advantages of CCS operations. We characterize GSOS congruency in as a bisimulation-like relation called ready simulation. Bisimulation is strictly finer than ready simulation, and hence not a congruence for any GSOS language. Copyright 1995 by ACM, Inc.

The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.

Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory -- semantics; D.3.3 [Programming Languages]: Language Constructs and Features -- concurrent programming structures; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages -- algebraic approaches to semantics; operational semantics; I.6.2 [Simulation and Modeling]: Simulation Languages

General Terms: Languages, Theory, Verification

Additional Key Words and Phrases: Bisimulation, structural operational semantics, process algebra, CCS

Selected papers that cite this one

• Luca Aceto, Bard Bloom, and Frits Vaandrager. Turning SOS rules into equations. Information and Computation, 111(1):1-52, 15 May 1994.

• Luca Aceto, Wan Fokkink, and Anna Ingólfsdóttir. A menagerie of non-finitely based process semantics over BPA* -- from ready simulation to completed traces. Mathematical Structures in Computer Science, 8(3):193-230, June 1998.

• Luca Aceto and Anna Ingólfsdóttir. CPO models for compact GSOS languages. Information and Computation, 129(2):107-141, 15 September 1996.

• Bard Bloom and Robert Paige. Transformational design and implementation of a new efficient solution to the ready simulation problem. Science of Computer Programming, 24(3):189-220, June 1995.

• Roland Bol and Jan Friso Groote. The meaning of negative premises in transition system specifications. Journal of the ACM, 43(5):863-914, September 1996.

• Pedro R. D'Argenio and Chris Verhoef. A general conservative extension theorem in process algebras with inequalities. Theoretical Computer Science, 177(2):351-380, 15 May 1997.

• Tim Fernando. Bisimulations and predicate logic. The Journal of Symbolic Logic, 59(3):924-944, September 1994.

• Gianluigi Ferrari, Ugo Montanari, and Miranda Mowbray. Structured transition systems with parametric observations: observational congruences and minimal realizations. Mathematical Structures in Computer Science, 7(3):241-282, June 1997.

• Gian-Luigi Ferrari, Ugo Montanari, and Paola Quaglia. A pi-calculus with explicit substitutions. Theoretical Computer Science, 168(1):53-103, 10 November 1996.

• Wan Fokkink and Rob van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Information and Computation, 126(1):1-10, 10 April 1996.

• Wan Fokkink and Chris Verhoef. A conservative look at operational semantics with variable binding. Information and Computation, 146(1):24-54, 10 October 1998.

• Rob J. van Glabbeek and W. Peter Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, May 1996.

• Trevor Jim and Albert R. Meyer. Full abstraction and the context lemma. SIAM Journal on Computing, 25(3):663-696, June 1996.

• David Sands. From SOS rules to proof principles: An operational metatheory for functional languages. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 428-441, Paris, France, 15-17 January 1997.

• Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447-479, October 1998.

• Daniele Turi and Gordon Plotkin. Towards a mathematical operational semantics. In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science, pages 280-291, Warsaw, Poland, 29 June-2 July 1997. IEEE Computer Society Press.

Selected references

• Samson Abramsky. A domain equation for bisimulation. Information and Computation, 92(2):161-218, June 1991.

• J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Control, 60(1-3):109-137, January/February/March 1984.

• Bard Bloom. Can LCF be topped? Flat lattice models of typed lambda calculus (preliminary report). In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 282-295, Edinburgh, Scotland, 5-8 July 1988. IEEE Computer Society.

• S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560-599, July 1984.

• Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, January 1985.

• Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, September 1991.

• Albert R. Meyer. Semantical paradigms: Notes for an invited lecture, with two appendices by Stavros S. Cosmadakis. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 236-253, Edinburgh, Scotland, 5-8 July 1988. IEEE Computer Society.

• Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Information and Computation, 100(1):1-40, September 1992.

• Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, II. Information and Computation, 100(1):41-77, September 1992.

• Irek Ulidowski. Equivalences on observable processes. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 148-159, Santa Cruz, California, 22-25 June 1992. IEEE Computer Society Press.

Shortcuts: