Bisimulation can't be traced

ABSTRACT

Bisimulation is the primitive notion of equivalence between concurrent processes in Milner's Calculus of Communicating Systems (CCS); there is a nontrivial game-like protocol for distinguishing nonbisimular processes. In contrast, process distinguishability in Hoare's theory of Communicating Sequential Processes (CSP) is determined solely on the basis of traces of visible actions. We examine what additional operations are needed to explain bisimulation similarly—specifically in the case of finitely branching processes without silent moves. We formulate a general notion of Structured Operational Semantics for processes with Guarded recursion (GSOS), and demonstrate that bisimulation does not agree with trace congruence with respect to any set of GSOS-definable contexts. In justifying the generality and significance of GSOS's, we work out some of the basic proof theoretic facts which justify the SOS discipline.

REFERENCES

• 1: S. Abramsky, Observation equivalence as a testing equivalence, Theoretical Computer Science, v.53 n.2-3, p.225-241, Aug. 1987 [doi>10.1016/0304-3975(87)90065-X]
• 2: D. Austry and G. Boudol. Alg~bre de processus et synehronisation. Theoretical Campnter Sci., 30:91-131, 1984.
• 3: J. C. M. Baeten , R. J. van Glabbeek, Another look at abstraction in process algebra, 14th International Colloquium on Automata, languages and programming, p.84-94, July 1987, Karlsruhe, Germany
• 4: J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Control, 60:109-137, 1984.
• 5: J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Sci., 37:77-121, 1985.
• 6: Stephen D. Brookes, On the Relationship of CCS and CSP, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.83-96, July 18-22, 1983
• 7: S. D. Brookes , C. A. R. Hoare , A. W. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM (JACM), v.31 n.3, p.560-599, July 1984 [doi>10.1145/828.833]
• 8: L. Castellano, G. D. Michelis, and L. Pomello. Concurrency vs interleaving" an instructive example. Bull. Enrop. Ass. Theoretical Computer Set., (31):12-15, 1987.
• 9: R. de Sirnone. Higher-level synchronising devices in MIEJE-SCCS. Theoretical Computer Sci., 37:245-267, 1985.
• 10: R. DeNicola and M. C. Hennessy. Testing equivalences for processes. Theoretical Computer Sci., 34:83-133, 1984.
• 11: M. Fischer and R. Ladner. Propositional dynamic logic of regular programs. J. Computer and System Set., 18:194-211, 1979.
• 12: Susanne Graf , Joseph Sifakis, Frm Synchronization Tree Logic to Acceptance Model Logic, Proceedings of the Conference on Logic of Programs, p.128-142, June 17-19, 1985
• 13: S Graf , J Sifakis, A modal characterization of observational congruence on finite terms of CCS, Information and Control, v.68 n.1-3, p.125-145, Jan/Feb/March 1986 [doi>10.1016/S0019-9958(86)80031-6]
• 14: S. Graf , J. Sifakis, Readiness semantics for regular processes with silent actions, 14th International Colloquium on Automata, languages and programming, p.115-125, July 1987, Karlsruhe, Germany
• 15: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 16: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 17: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 18: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 19: R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Sci., 25:267-310, 1983.
• 20: Robin Milner, Lectures on a Calculus for Communicating Systems, Seminar on Concurrency, Carnegie-Mellon University, p.197-220, July 09-11, 1984
• 21: E R Olderog , C A R Hoare, Specification-oriented semantics for communicating processes, Acta Informatica, v.23 n.1, p.9-66, April 1986 [doi>10.1007/BF00268075]
• 22: I Phillips, Refusal testing, International Colloquium on Automata, Languages and Programming on Automata, languages and programming, p.304-313, September 1986, Rennes, France
• 23: G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN- 19, Aarhus Univ., Computer Science Dept., Denmark, 1981.
• 24: Amir Pnueli, Linear and Branching Structures in the Semantics and Logics of Reactive Systems, Proceedings of the 12th Colloquium on Automata, Languages and Programming, p.15-32, July 15-19, 1985
• 25: R. S. Streett. PDL of looping and converse is elementarily decidable. Information and Control, 54.'121-141, 1982. Cambridge, Massachusetts, October 18, 1987

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Trees

General Terms:
Algorithms, Languages, Theory