Advertisement

ACPτ a universal axiom system for process specification

  • J. A. Bergstra
  • J. W. Klop
Part IV An Algebraic Approach To Concurrency
Part of the Lecture Notes in Computer Science book series (LNCS, volume 394)

Abstract

Starting with Basic Process Algebra (BPA), an axiom system for alternative composition (+) and sequential composition (·) of processes, we give a presentation in several intermediate stages leading to ACPτ, Algebra of Communicating Processes with abstraction. At each successive stage an example is given showing that the specification power is increased. Also some graph models for the respective axiom systems are informally presented. We conclude with the Finite Specification Theorem for ACPτ, stating that each finitely branching, effectively presented process (as an element of the graph model) can be specified in ACPτ by means of a finite system of guarded recursion equations.

Key Words & Phrases

communicating processes process algebra bisimulation semantics graph models recursive specifications 

1985 Mathematical Subject Classification

68Q10 68Q55 68Q45 68N15 

1982 CR Categories

F.1.2 F.3.2 F.4.3 D.3.3 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    J.C.M. Baeten, J.A. Bergstra, J.W. Klop (1987). On the consistency of Koomen's Fair Abstraction Rule. TCS 51 (1/2), 129–176.CrossRefGoogle Scholar
  2. 2.
    J.C.M. Baeten, J.A. Bergstra, J.W. Klop (1987). Decidability of bisimulation equivalence for processes generating context-free languages. J.W. de Bakker, A.J. Nijman, P.C. Treleaven (eds.). Proceedings of the PARLE Conference, Eindhoven 1987, Vol. II, Springer LNCS 259, 94–113.Google Scholar
  3. 3.
    J.C.M. Baeten, R.J. van Glabbeek (1987). Abstraction and Empty Process in Process Algebra, CWI Report CS-R8721, Centre for Mathematics and Computer Science, Amsterdam.Google Scholar
  4. 4.
    J.A. Bergstra, J.W. Klop (1984). The algebra of recursively defined processes and the algebra of regular processes. J. Paredaens (ed.). Proc. 11th ICALP, Antwerpen 1984, Springer LNCS 172, 82–95.Google Scholar
  5. 5.
    J.A. Bergstra, J.W. Klop (1986). Algebra of communicating processes. J.W. de Bakker, M. Hazewinkel, J.K. Lenstra (eds.). CWI Monograph I, Proceedings of the CWI Symposium Mathematics and Computer Science, North-Holland, Amsterdam, 89–138.Google Scholar
  6. 6.
    J.A. Bergstra, J.W. Klop (1986). Process algebra: specification and verification in bisimulation semantics. M. Hazewinkel, J.K. Lenstra, L.G.L.T. Meertens (eds.). CWI Monograph 4, Proceedings of the CWI Symposium Mathematics and Computer Science II, North-Holland, Amsterdam, 61–94.Google Scholar
  7. 7.
    J.A. Bergstra, J.W. Klop, E.-R. Olderog (1987). Failures without chaos: a new process semantics for fair abstraction. M. Wirsing (ed.). Proceedings IFIP Conference on Formal Description of Programming Concepts, Gl. Avernaes 1986, North-Holland, Amsterdam, 77–103.Google Scholar
  8. 8.
    R.J. van Glabbeek, F.W. Vaandrager (1987). Petri net models for algebraic theories of concurrency. J.W. de Bakker, A.J. Nijman, P.C. Treleaven (eds.). Proc. PARLE Conference, Eindhoven 1987, Vol. II, Springer LNCS 259, 224–242.Google Scholar
  9. 9.
    C.P.J. Koymans, J.C. Mulder (1986). A Modular Approach to Protocol Verification using Process Algebra, Logic Group Preprint Series Nr.6, Dept. of Philosophy, State University of Utrecht.Google Scholar
  10. 10.
    L. Kossen, W.P. Weijland (1987). Correctness Proofs for Systolic Algorithms: Palindromes and Sorting, Report FVI 87-04, Computer Science Department, University of Amsterdam.Google Scholar
  11. 11.
    S. Mauw (1987). A Constructive Version of the Approximation Induction Principle, Report FVI 87-09, Computer Science Department, University of Amsterdam.Google Scholar
  12. 12.
    R. Milner (1980). A Calculus of Communicating Systems, Springer LNCS 92.Google Scholar
  13. 13.
    D. Park (1981). Concurrency and automata on infinite sequences. Proc. 5th GI Conference, Springer LNCS 104.Google Scholar
  14. 14.
    F.W. Vaandrager (1986). Verification of Two Communication Protocols by Means of Process Algebra, CWI Report CS-R8608, Centre for Mathematics and Computer Science, Amsterdam.Google Scholar
  15. 15.
    W.P. Weijland (1987). A Systolic Algorithm for Matrix-Vector Multiplication, Report FVI 87-08, Computer Science Department, University of Amsterdam.Google Scholar
  16. 16.
    J.L.M. Vrancken (1986). The Algebra of Communicating Processes with Empty Process, Report FVI 86-01, Computer Science Department, University of Amsterdam.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