Nothing Special   »   [go: up one dir, main page]

Skip to main content

Process theory based on bisimulation semantics

  • Tutorials
  • Conference paper
  • First Online:
Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency (REX 1988)

Part of the book series: Lecture Notes in Computer Science ((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.

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • ACZEL, P. (87), Lecture Notes on Non-Well-Founded sets, CSLI, Lecture Notes Nr.9, 1987

    Google Scholar 

  • 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 

  • 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.

    Article  Google Scholar 

  • 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 

  • 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.

    Article  Google Scholar 

  • 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 

  • 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 

  • 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 

  • 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.

    Article  Google Scholar 

  • 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 

  • 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.

    Article  Google Scholar 

  • BERGSTRA, J.A. & KLOP, J.W. (84a), Process algebra for synchronous communication, Information & Control 60 (1/3), p. 109–137, 1984.

    Google Scholar 

  • 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 

  • BERGSTRA, J.A. & KLOP, J.W. (85), Algebra of communicating processes with abstraction, TCS 37 (1), p. 77–121, 1985.

    Article  Google Scholar 

  • 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 

  • 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 

  • 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 

  • 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 

  • 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 

  • BERGSTRA, J.A., KLOP, J.W. & OLDEROG, E.-R. (86), Failure semantics with fair abstraction, CWI Report CS-R8609, Amsterdam 1986.

    Google Scholar 

  • 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 

  • 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 

  • BERGSTRA, J.A. & TIURYN, J. (87), Process algebra semantics for queues, Fund. Inf. X, p.213–224, 1987.

    Google Scholar 

  • 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.

    Article  Google Scholar 

  • 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 

  • 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.

    Article  Google Scholar 

  • DE NICOLA, R. & HENNESSY, M. (83), Testing equivalences for processes, TCS 34, p.83–133.

    Google Scholar 

  • 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 

  • 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 

  • 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.

    Article  Google Scholar 

  • HENNESSY, M. (88), Algebraic theory of processes, The MIT Press, 1988.

    Google Scholar 

  • HENNESSY, M. & MILNER, R. (85), Algebraic laws for nondeterminism and nondeterminism and concurrency, JACM 32, 137–161.

    Google Scholar 

  • HESSELINK, W. (88), Deadlock and fairness in morphisms of transition systems, Theor. Comp. Sci. 59 (1988) 235–257.

    Article  Google Scholar 

  • HOARE, C.A.R. (78), Communicating sequential processes, Comm. ACM 21, p. 666–677, 1978.

    Article  Google Scholar 

  • HOARE, C.A.R. (84), Notes on communicating sequential processes, International Summer School in Marktoberdorf: Control Flow and Data Flow, Munich 1984.

    Google Scholar 

  • HOARE, C.A.R. (85), Communicating sequential processes, Prentice Hall 1985.

    Google Scholar 

  • 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 

  • 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 

  • 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 

  • KRANAKIS, E. (86), Approximating the projective model, in: Proc. Conf. on Math. Logic & its Applications, Druzhba (Bulgaria), 1986 (Pergamon Press).

    Google Scholar 

  • KRANAKIS, E. (87), Fixed point equations with parameters in the projective model, Information and Computation, Vol.75, No.3, 1987.

    Google Scholar 

  • MAUW, S. (87), A constructive version of the Approximation Induction Principle, Report FVI 87-09, Computer Science Department, University of Amsterdam, 1987.

    Google Scholar 

  • MILNER, R. (80), A calculus of communicating systems, Springer LNCS 92, 1980.

    Google Scholar 

  • 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 

  • 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.

    Article  Google Scholar 

  • MILNER, R. (85), Lectures on a calculus for communicating systems, in: Seminar on Concurrency, Springer LNCS 197 (1985), 197–220.

    Google Scholar 

  • 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 

  • MOLLER, F. (88), Non-finite axiomatisability in Process Algebras, preprint, Univ. of Edinburgh, 1988

    Google Scholar 

  • MULDER, J.C. (88), On the Amoeba protocol, CWI Report CS-R8827, Centre for Mathematics and Computer Science, Amsterdam 1988.

    Google Scholar 

  • PARK, D.M.R. (81), Concurrency and automata on infinite sequences. Proc. 5th GI Conference, Springer LNCS 104, 1981.

    Google Scholar 

  • PHILLIPS, I.C.C. (87), Refusal testing, TCS 50 (2), 1987.

    Google Scholar 

  • 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 

  • 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 

  • 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 

Download references

Author information

Authors and Affiliations

Authors

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Rights and permissions

Reprints 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

Publish with us

Policies and ethics