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.
Note: Research partially supported by ESPRIT project 432, Meteor.
Chapter 1 of this paper is a modified version of ‘Process algebra: specification and verification in bisimulation semantics’, from CWI Monograph 4, Proc. of the CWI Symposium Mathematics and Computer Science II (eds. Hazewinkel, Lenstra, Meertens), North-Holland, Amsterdam 1986. Permission of the editors to include the present Chapter 1 here is gratefully acknowledged.
Preview
Unable to display preview. Download preview PDF.
References
ACZEL, P. (87), Lecture Notes on Non-Well-Founded sets, CSLI, Lecture Notes Nr.9, 1987
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.
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.
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.
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.
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.
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.
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.
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.
DE BAKKER, J.W. & ZUCKER, J.I. (82a), Denotational semantics of concurrency, Proc. 14th ACM Symp. Theory of Comp., p. 153–158, 1982.
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.
BERGSTRA, J.A. & KLOP, J.W. (84a), Process algebra for synchronous communication, Information & Control 60 (1/3), p. 109–137, 1984.
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.
BERGSTRA, J.A. & KLOP, J.W. (85), Algebra of communicating processes with abstraction, TCS 37 (1), p. 77–121, 1985.
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.
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.
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.
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.
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.
BERGSTRA, J.A., KLOP, J.W. & OLDEROG, E.-R. (86), Failure semantics with fair abstraction, CWI Report CS-R8609, Amsterdam 1986.
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.
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.
BERGSTRA, J.A. & TIURYN, J. (87), Process algebra semantics for queues, Fund. Inf. X, p.213–224, 1987.
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.
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.
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.
DE NICOLA, R. & HENNESSY, M. (83), Testing equivalences for processes, TCS 34, p.83–133.
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.
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.
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.
HENNESSY, M. (88), Algebraic theory of processes, The MIT Press, 1988.
HENNESSY, M. & MILNER, R. (85), Algebraic laws for nondeterminism and nondeterminism and concurrency, JACM 32, 137–161.
HESSELINK, W. (88), Deadlock and fairness in morphisms of transition systems, Theor. Comp. Sci. 59 (1988) 235–257.
HOARE, C.A.R. (78), Communicating sequential processes, Comm. ACM 21, p. 666–677, 1978.
HOARE, C.A.R. (84), Notes on communicating sequential processes, International Summer School in Marktoberdorf: Control Flow and Data Flow, Munich 1984.
HOARE, C.A.R. (85), Communicating sequential processes, Prentice Hall 1985.
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.
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.
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.
KRANAKIS, E. (86), Approximating the projective model, in: Proc. Conf. on Math. Logic & its Applications, Druzhba (Bulgaria), 1986 (Pergamon Press).
KRANAKIS, E. (87), Fixed point equations with parameters in the projective model, Information and Computation, Vol.75, No.3, 1987.
MAUW, S. (87), A constructive version of the Approximation Induction Principle, Report FVI 87-09, Computer Science Department, University of Amsterdam, 1987.
MILNER, R. (80), A calculus of communicating systems, Springer LNCS 92, 1980.
MILNER, R. (84a), Lectures on a Calculus for Communicating Systems, Working Material for the Summer School Control Flow and Data Flow, Munich, July 1984.
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.
MILNER, R. (85), Lectures on a calculus for communicating systems, in: Seminar on Concurrency, Springer LNCS 197 (1985), 197–220.
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.
MOLLER, F. (88), Non-finite axiomatisability in Process Algebras, preprint, Univ. of Edinburgh, 1988
MULDER, J.C. (88), On the Amoeba protocol, CWI Report CS-R8827, Centre for Mathematics and Computer Science, Amsterdam 1988.
PARK, D.M.R. (81), Concurrency and automata on infinite sequences. Proc. 5th GI Conference, Springer LNCS 104, 1981.
PHILLIPS, I.C.C. (87), Refusal testing, TCS 50 (2), 1987.
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.
VRANCKEN, J.L.M. (86), The Algebra of Communicating Processes with empty process, Report FVI 86-01, Computer Science Department, University of Amsterdam, 1986.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bergstra, J.A., Klop, J.W. (1989). Process theory based on bisimulation semantics. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. REX 1988. Lecture Notes in Computer Science, vol 354. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013021
Download citation
DOI: https://doi.org/10.1007/BFb0013021
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51080-2
Online ISBN: 978-3-540-46147-0
eBook Packages: Springer Book Archive