Advertisement

Process theory based on bisimulation semantics

  • J. A. Bergstra
  • J. W. Klop
Tutorials
Part of the Lecture Notes in Computer Science book series (LNCS, volume 354)

Abstract

In this paper a process is viewed as a labeled graph modulo bisimulation equivalence. Three topics are covered: (i) specification of processes using finite systems of equations over the syntax of process algebra; (ii) inference systems which are complete for proving the equivalence of regular (finite state) processes; (iii) variations of the bisimulation model.

Keywords

Proof System Recursion Equation Process Algebra Proof Rule Regular Process 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ACZEL, P. (87), Lecture Notes on Non-Well-Founded sets, CSLI, Lecture Notes Nr.9, 1987Google Scholar
  2. AMERICA, P. & RUTTEN, J.J.M.M. (88), Solving reflexive domain equations in a category of complete metric spaces, in: Proc. of the Third Workshop on Mathematical Foundations of Programming Language Semantics (M. Main, A. Melton, M. Mislove, D. Schmidt, eds.), Springer LNCS 298, 1988, p.254–288. Also to appear in the Journal of Computer and System Sciences.Google Scholar
  3. BAETEN, J.C.M. & BERGSTRA, J.A. (88), Global renaming operators in concrete process algebra, Information and Computation, Vol.78, Nr.3 (1988), 205–245.CrossRefGoogle Scholar
  4. BAETEN, J.C.M., BERGSTRA, J.A. & KLOP, J.W. (86), Syntax and defining equations for an interrupt mechanism in process algebra, Fund. Inf. IX (2), p.127–168, 1986.Google Scholar
  5. BAETEN, J.C.M., BERGSTRA, J.A. & KLOP, J.W. (87) On the consistency of Koomen's Fair Abstraction Rule, TCS 51 (1987), 129–176.CrossRefGoogle Scholar
  6. BAETEN, J.C.M., BERGSTRA, J.A. & KLOP, J.W. (87a), Decidability of bisimulation equivalence for processes generating context-free languages, in: Proc. PARLE, Vol.II (Parallel Languages), (eds. J.W. de Bakker, A.J. Nijman, P.C. Treleaven), Eindhoven 1987, Springer LNCS 259, p.94–113, 1987.Google Scholar
  7. BAETEN, J.C.M., BERGSTRA, J.A. & KLOP, J.W. (87b), Conditional axioms and α/β calculus in process algebra, in: Proc. IFIP Conf. on Formal Description of Programming Concepts—III, Ebberup 1986, (M. Wirsing, ed.) North-Holland, Amsterdam 1987, p.53–75.Google Scholar
  8. BAETEN, J.C.M. & VAN GLABBEEK, R.J. (87), Another look at abstraction in process algebra, in: Proc. 14th ICALP 87, Karlsruhe (Th. Ottman, ed.), Springer LNCS 267, p.84–94, 1987.Google Scholar
  9. DE BAKKER, J.W., BERGSTRA, J.A., KLOP, J.W. & MEYER, J.-J.CH. (84), Linear time and branching time semantics for recursion with merge. Theoretical Computer Science 34 (1984), p.135–156.CrossRefGoogle Scholar
  10. DE BAKKER, J.W. & ZUCKER, J.I. (82a), Denotational semantics of concurrency, Proc. 14th ACM Symp. Theory of Comp., p. 153–158, 1982.Google Scholar
  11. DE BAKKER, J.W. & ZUCKER, J.I. (82b), Processes and the denotational semantics of concurrency, Information and Control 54 (1/2), p. 70–120, 1982.CrossRefGoogle Scholar
  12. BERGSTRA, J.A. & KLOP, J.W. (84a), Process algebra for synchronous communication, Information & Control 60 (1/3), p. 109–137, 1984.Google Scholar
  13. BERGSTRA, J.A. & KLOP, J.W. (84b), The algebra of recurively defined processes and the algebra of regular processes, in: Proc. 11th ICALP (ed. J. Paredaens), Antwerpen 1984, Springer LNCS 172, p.82–95, 1984.Google Scholar
  14. BERGSTRA, J.A. & KLOP, J.W. (85), Algebra of communicating processes with abstraction, TCS 37 (1), p. 77–121, 1985.CrossRefGoogle Scholar
  15. BERGSTRA, J.A. & KLOP, J.W. (86a), Verification of an alternating bit protocol by means of process algebra, in: Math. Methods of Spec. and Synthesis of Software Systems '85 (eds. W. Bibel and K.P. Jantke), Math. Research 31, Akademie-Verlag Berlin, p.9–23. 1986.Google Scholar
  16. BERGSTRA, J.A. & KLOP, J.W. (86b), Algebra of communicating processes, in: CWI Monographs I, Proceedings of the CWI Symposium Mathematics and Computer Science (eds. J.W. de Bakker, M. Hazewinkel & J.K. Lenstra) North-Holland, Amsterdam, 1986, p.89–138.Google Scholar
  17. BERGSTRA, J.A. & KLOP, J.W. (86c), Process algebra: specification and verification in bisimulation semantics, in: CWI Monograph 4, Proceedings of the CWI Symposium Mathematics and Computer Science II (eds. M. Hazewinkel, J.K. Lenstra & L.G.L.T. Meertens), North-Holland, Amsterdam 1986, p.61–94.Google Scholar
  18. BERGSTRA, J.A. & KLOP, J.W. (87), A convergence theorem in process algebra, CWI Report CS-R8733, Centre for Mathematics and Computer Science, Amsterdam, 1987.Google Scholar
  19. BERGSTRA, J.A. & KLOP, J.W. (88), A complete inference system for regular processes with silent moves, in: Proc. of Logic Colloquium, Hull '86, (eds. F.R. Drake and J.K. Truss), North-Holland 1988.Google Scholar
  20. BERGSTRA, J.A., KLOP, J.W. & OLDEROG, E.-R. (86), Failure semantics with fair abstraction, CWI Report CS-R8609, Amsterdam 1986.Google Scholar
  21. BERGSTRA, J.A., KLOP, J.W. & OLDEROG, E.-R. (87), Failures without chaos: a new process semantics for fair abstraction, in: Proceedings IFIP Conference on Formal Description of Programming Concepts—III, Gl. Avernaes (Ebberup) 1986 (ed. M. Wirsing), North-Holland, Amsterdam, p.77–103, 1987.Google Scholar
  22. BERGSTRA, J.A., KLOP, J.W. & OLDEROG, E.-R. (88), Readies and failures in the algebra of communicating processes, CWI Report CS-R8523, Amsterdam 1985. To appear in SIAM J. of Computing, 1988.Google Scholar
  23. BERGSTRA, J.A. & TIURYN, J. (87), Process algebra semantics for queues, Fund. Inf. X, p.213–224, 1987.Google Scholar
  24. BERGSTRA, J.A. & TUCKER, J.V. (84), Top down design and the algebra of communicating processes, Sci. of Comp. Progr. 5 (2), p. 171–199, 1984.CrossRefGoogle Scholar
  25. BROOKES, S.D. (83), On the relationship of CCS and CSP Proc. 10th ICALP (ed. J. Díaz), Barcelona 1983, Springer LNCS 154, 83–96.Google Scholar
  26. BROOKES, S.D., HOARE, C.A.R. & ROSCOE, A.W. (84), A theory of Communicating Sequential Processes, JACM Vol.31, No.3 (1984) 560–599.CrossRefGoogle Scholar
  27. DE NICOLA, R. & HENNESSY, M. (83), Testing equivalences for processes, TCS 34, p.83–133.Google Scholar
  28. VAN GLABBEEK, R.J. (87), Bounded nondeterminism and the approximation principle in process algebra. In: Proc. of the 4th Annual Symposium on Theoretical Aspects of Computer Science (eds. F.J. Brandenburg, G. Vidal-Naquet and M. Wirsing), Passau (W. Germany) 1987, Springer LNCS 247, 336–347.Google Scholar
  29. VAN GLABBEEK, R.J. & VAANDRAGER, F.W. (88), Modular specifications in process algebra—with curious queues, Centre for Mathematics and Computer Science, Report CS-R8821, Amsterdam 1988; extended abstract to appear in: Proc. of the METEOR Workshop on Algebraic Methods: Theory, Tools and Applications, Springer LNCS.Google Scholar
  30. GOLSON, W.G. & ROUNDS, W.C. (83), Connections between two theories of concurrency: metric spaces and synchronization trees. Information and Control 57 (1983), 102–124.CrossRefGoogle Scholar
  31. HENNESSY, M. (88), Algebraic theory of processes, The MIT Press, 1988.Google Scholar
  32. HENNESSY, M. & MILNER, R. (85), Algebraic laws for nondeterminism and nondeterminism and concurrency, JACM 32, 137–161.Google Scholar
  33. HESSELINK, W. (88), Deadlock and fairness in morphisms of transition systems, Theor. Comp. Sci. 59 (1988) 235–257.CrossRefGoogle Scholar
  34. HOARE, C.A.R. (78), Communicating sequential processes, Comm. ACM 21, p. 666–677, 1978.CrossRefGoogle Scholar
  35. HOARE, C.A.R. (84), Notes on communicating sequential processes, International Summer School in Marktoberdorf: Control Flow and Data Flow, Munich 1984.Google Scholar
  36. HOARE, C.A.R. (85), Communicating sequential processes, Prentice Hall 1985.Google Scholar
  37. KOYMANS, C.P.J. & MULDER, J.C. (86), A modular approach to protocol verification using process algebra, Logic Group Preprint Series Nr.6, Dept. of Philosophy, State University of Utrecht, 1986; to appear in: Applications of Process Algebra, (J.C.M. Baeten, ed.), CWI Monograph, North-Holland, 1988.Google Scholar
  38. KOYMANS, C.P.J. & VRANCKEN, J.L.M. (85), Extending process algebra with the empty process ɛ, Logic Group Preprint Series Nr.1, Dept. of Philosophy, State University of Utrecht, 1985.Google Scholar
  39. KOSSEN, L. & WEIJLAND, W.P. (87), Correctness proofs for systolic algorithms: palindromes and sorting, Report FVI 87-04, Computer Science Department, University of Amsterdam, 1987.Google Scholar
  40. KRANAKIS, E. (86), Approximating the projective model, in: Proc. Conf. on Math. Logic & its Applications, Druzhba (Bulgaria), 1986 (Pergamon Press).Google Scholar
  41. KRANAKIS, E. (87), Fixed point equations with parameters in the projective model, Information and Computation, Vol.75, No.3, 1987.Google Scholar
  42. MAUW, S. (87), A constructive version of the Approximation Induction Principle, Report FVI 87-09, Computer Science Department, University of Amsterdam, 1987.Google Scholar
  43. MILNER, R. (80), A calculus of communicating systems, Springer LNCS 92, 1980.Google Scholar
  44. MILNER, R. (84a), Lectures on a Calculus for Communicating Systems, Working Material for the Summer School Control Flow and Data Flow, Munich, July 1984.Google Scholar
  45. MILNER, R. (84b), A complete inference system for a class of regular behaviours, Journal of Computer and System Sciences, Vol.28, Nr.3, 439–466, 1984.CrossRefGoogle Scholar
  46. MILNER, R. (85), Lectures on a calculus for communicating systems, in: Seminar on Concurrency, Springer LNCS 197 (1985), 197–220.Google Scholar
  47. MILNER, R. (88), A complete axiomatisation for observational congruence of finite-state behaviours, Preprint, Univ. of Edinburgh 1985; to appear in Information and Computation 1988.Google Scholar
  48. MOLLER, F. (88), Non-finite axiomatisability in Process Algebras, preprint, Univ. of Edinburgh, 1988Google Scholar
  49. MULDER, J.C. (88), On the Amoeba protocol, CWI Report CS-R8827, Centre for Mathematics and Computer Science, Amsterdam 1988.Google Scholar
  50. PARK, D.M.R. (81), Concurrency and automata on infinite sequences. Proc. 5th GI Conference, Springer LNCS 104, 1981.Google Scholar
  51. PHILLIPS, I.C.C. (87), Refusal testing, TCS 50 (2), 1987.Google Scholar
  52. VAANDRAGER, F.W. (86), Verification of two communication protocols by means of process algebra, CWI Report CS-R8608, Centre for Mathematics and Computer Science, Amsterdam 1986.Google Scholar
  53. VRANCKEN, J.L.M. (86), The Algebra of Communicating Processes with empty process, Report FVI 86-01, Computer Science Department, University of Amsterdam, 1986.Google Scholar
  54. WEIJLAND, W.P. (87), A systolic algorithm for matrix-vector multiplication, Report FVI 87-08, Computer Science Department, University of Amsterdam, 1987; also in: Proc. SION Conf. CSN 87, p.143–160, CWI, Amsterdam 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • J. A. Bergstra
    • 1
    • 2
  • J. W. Klop
    • 3
    • 4
  1. 1.Department of Computer ScienceUniversity of AmsterdamAmsterdam
  2. 2.Department of PhilosophyState University of UtrechtUtrecht
  3. 3.Centre for Mathematics and Computer ScienceAmsterdam
  4. 4.Department of Mathematics and Computer ScienceFree UniversityAmsterdam

Personalised recommendations