Skip to main content
SpringerLink
Log in

Bounded nondeterminism and the approximation induction principle in process algebra

  • Contributed Papers
  • Conference paper
  • First Online:
Book cover STACS 87 (STACS 1987)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 247))

Included in the following conference series:

Abstract

This paper presents a new semantics of ACPτ, the Algebra of Communicating Processes with abstraction. This leads to a term model of ACPτ which is isomorphic to the model of process graphs modulo rooted τδ-bisimulation of Baeten, Bergstra & Klop

In this model, the Recursive Definition Principle (RDP), the Commutativity of Abstraction (CA) and Koomen's Fair Abstraction Rule (KFAR) are satisfied, but the Approximation Induction Principle (AIP) is not. The combination of these four principles is proven to be inconsistent, while any combination of three of them is not.

In [2] a restricted version of AIP is proved valid in the graph model. This paper proposes a simpler and less restrictive version of AIP, not containing guarded recursive specifications as a parameter, which is still valid. This infinitary rule is formulated with the help of a family B n of unary predicates, expressing bounded nondeterminism.

Extended abstract

Note: Sponsored in part by Esprit project no. 432, METEOR.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.C.M. Baeten, J.A. Bergstra & J.W. Klop, Conditional axioms and α/β calculus in process algebra, report CS-R8502, Centrum voor Wiskunde en Informatica, Amsterdam 1985, to appear in: Proc. IFIP Conference on Formal Description of Programming Concepts, Gl. Avernaes 1986, (M. Wirsing, ed.), North-Holland.

    Google Scholar 

  2. J.C.M. Baeten, J.A. Bergstra & J.W. Klop, On the consistency of Koomen's Fair Abstraction Rule, report CS-R8511, Centrum voor Wiskunde en Informatica, Amsterdam 1985, to appear in Theoretical Computer Science.

    Google Scholar 

  3. J.W. de Bakker & J.I. Zucker, Processes and the denotational semantics of concurrency, Information & Control 54 (1/2), pp. 70–120, 1982.

    Google Scholar 

  4. J.A. Bergstra & J.W. Klop, Algebra of communicating processes, Proc. of the CWI Symp. Math. & Comp. Sci., eds. J.W. de Bakker, M. Hazewinkel & J.K. Lenstra, Amsterdam 1986.

    Google Scholar 

  5. J.A. Bergstra & J.W. Klop, Algebra of communicating processes with abstraction, Theoretical Computer Science 37(1), pp. 77–121, 1985.

    Google Scholar 

  6. J.A. Bergstra, J.W. Klop & E.-R. Olderog, Failures without chaos: a new process semantics with fair abstraction, report CS-R8625, Centrum voor Wiskunde en Informatica, Amsterdam 1986, to appear in: Proc. IFIP Conference on Formal Description of Programming Concepts, Gl. Avernaes 1986, (M. Wirsing, ed.), North-Holland.

    Google Scholar 

  7. S.D. Brookes, C.A.R. Hoare & W. Roscoe, A theory of communicating sequential processes, Journal ACM 31(3), pp. 560–599, 1984.

    Google Scholar 

  8. R.J. van Glabbeek, Bounded nondeterminism and the approximation induction principle in process algebra, report CS-R8634, Centrum voor Wiskunde en Informatica, Amsterdam 1986.

    Google Scholar 

  9. G.J. Milne, CIRCAL and the representation of communication, concurrency, and time, Transactions on Programming Languages and Systems (ACM) 7(2), pp. 270–298, 1985.

    Google Scholar 

  10. R. Milner, A calculus for communicating systems, Springer LNCS 92, 1980.

    Google Scholar 

  11. R. Milner, Lectures on a calculus for communicating systems, Seminar on Concurrency, Springer LNCS 197, pp. 197–220, 1985.

    Google Scholar 

  12. D.M.R. Park, Concurrency and automata on infinite sequences, Proc. 5th GI Conference, Springer LNCS 104, 1981.

    Google Scholar 

  13. W. Reisig, Petri Nets, An Introduction, EATCS Monographs on Theoretical Computer Science, Springer-Verlag 1985.

    Google Scholar 

  14. M. Rem, Partially ordered computations, with applications to VLSI design, Proc. 4th Advanced Course on Foundations of Computer Science, part 2, (eds.) J.W. de Bakker & J. van Leeuwen, Tract 159, Mathematisch Centrum, Amsterdam 1983.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Mathematics and Computer Science, P.O. Box 4079, 1009 AB, Amsterdam, The Netherlands

    R. J. van Glabbeek

Authors
  1. R. J. van Glabbeek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Franz J. Brandenburg Guy Vidal-Naquet Martin Wirsing

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Glabbeek, R.J. (1987). Bounded nondeterminism and the approximation induction principle in process algebra. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds) STACS 87. STACS 1987. Lecture Notes in Computer Science, vol 247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0039617

Download citation

  • DOI: https://doi.org/10.1007/BFb0039617

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-17219-2

  • Online ISBN: 978-3-540-47419-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation