Skip to main content
SpringerLink
Log in

Petri net models for algebraic theories of concurrency

extended abstract

  • Conference paper
  • First Online:
PARLE Parallel Architectures and Languages Europe (PARLE 1987)

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

Abstract

In this paper we discuss the issue of interleaving semantics versus True concurrency in an algebraic setting. We present various equivalence notions on Petri nets which can be used in the construction of algebraic models:

  1. (a)

    the occurrence net equivalence of Nielsen, Plotkin & Winskel;

  2. (b)

    bisimulation equivalence, which leads to a model which is isomorphic to the graph model of Baeten, Bergstra & Klop;

  3. (c)

    the concurrent bisimulation equivalence, which is also described by Nielsen & Thiagarajan, and Goltz;

  4. (d)

    partial order equivalences which are inspired by work of Pratt, and Boudol & Castellani.

A central role in the paper will be played by the notion of real-time consistency. We show that, besides occurrence net equivalence, none of the equivalences mentioned above (including the partial order equivalences!) is real-time consistent. Therefore we introduce the notion of ST-bisimulation equivalence, which is real-time consistent. Moreover a complete proof system will be presented for those finite ST-bisimulation processes in which no action can occur concurrently with itself.

Note: Partial support received from the European Communities under ESPRIT project no. 432, An Integrated Formal Approach to Industrial Software Development (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. Aalbersberg, IJ.J. & G. Rozenberg, Theory of traces, Technical Report No. 86-16, Institute of Applied Mathematics and Computer Science, University of Leiden, 1986.

    Google Scholar 

  2. Baeten, J.C.M. & J.A. Bergstra, Global renaming operators in concrete process algebra, CWI Report CS-R8521, Amsterdam, 1985.

    Google Scholar 

  3. Baeten, J.C.M., J.A. Bergstra & J.W. Klop, On the consistency of Koomen's fair abstraction rule, CWI Report CS-R8511, Amsterdam, 1985, to appear in Theor. Comp. Sci.

    Google Scholar 

  4. Baeten, J.C.M., J.A. Bergstra & J.W. Klop, An operational semantics for process algebra, CWI Report CS-R8522, Amsterdam, 1985, to appear in: Proc. Banach semester, Warschau 1985, North-Holland.

    Google Scholar 

  5. Bergstra, J.A. & J.W. Klop, Process algebra for synchronous communication, Information & Control 60 (1/3), 1984, pp. 109–137.

    Google Scholar 

  6. Bergstra, J.A. & J.W. Klop, Process Algebra: Specification and Verification in Bisimulation Semantics, In: Proc. CWI Symposium Math. & Comp. Sci. (M. Hazewinkel, J.K. Lenstra & L.G.L.T. Meertens, eds.), North Holland, 1986, pp. 61–94.

    Google Scholar 

  7. Bergstra, J.A. & J.W. Klop, Algebra of Communicating processes with abstraction, Theor. Comp. Sci. 37(1), 1985, pp. 77–121.

    Article  Google Scholar 

  8. Boudol, G. & I. Castellani, On the semantics of concurrency: partial orders and transition systems, Rapports de Recherche No 550, INRIA, Centre Sophia Antipolis, 1986.

    Google Scholar 

  9. Carlier, J., Chretienne & C. Girault, Modelling scheduling problems with timed Petri nets, In: Advances in Petri Nets 1984 (G. Rozenberg, ed.), Springer LNCS 188, 1985, pp. 62–82.

    Google Scholar 

  10. van Glabbeek, R.J. & F.W. Vaandrager, Petri net models for algebraic theories of concurrency, to appear as: CWI Report CS-R87.., Amsterdam, 1987.

    Google Scholar 

  11. Goltz, U., Building Structured Petri Nets, Arbeitspapiere der GMD 223, Sankt Augustin, 1986.

    Google Scholar 

  12. Goltz, U. & A. Mycroft, On the relationship of CCS and Petri nets, In: Proc. ICALP 84 (J. Paredaens, ed.), Springer LNCS 172, 1984, pp. 196–208.

    Google Scholar 

  13. Hospers, J., An Introduction to Philosophical Analysis, second edition, Prentice-Hall, Inc., Englewood Cliffs, N.J., 1967.

    Google Scholar 

  14. Mazurkiewicz, A., Concurrent program schemes and their interpretations, Report DAIMI PB-78, Computer Science Department, Aarhus University, Aarhus, 1978.

    Google Scholar 

  15. Mazurkiewicz, A., Semantics of concurrent systems: a modular fixed-point trace approach, In: Advances in Petri Nets 1984 (G. Rozenberg, ed.), Springer LNCS 188, 1985, pp. 353–375.

    Google Scholar 

  16. Milner, R., A calculus for Communicating Systems, Springer LNCS 92, 1980.

    Google Scholar 

  17. Nielsen, M., G.D. Plotkin & G. Winskel, Petri nets, event structures and domains, part I. Theor. Comp. Sci., 13(1). 1981, pp. 85–108.

    Article  Google Scholar 

  18. Nielsen, M. & P.S. Thiagarajan, Degrees of Non-Determinism and Concurrency: A Petri Net View, In: Proc. of the 5th Conf. on Found. of Softw. Techn. and Theor. Comp. Sci. (M. Joseph & R. Shyamasundar, eds.), Springer LNCS 181, 1984, pp. 89–118.

    Google Scholar 

  19. Park, D.M.R., Concurrency and automata on infinite sequences, Proc. 5th GI Conference (P. Deussen, ed.), Springer LNCS 104, 1981, pp. 167–183.

    Google Scholar 

  20. Petri, C.A., Kommunikation mit Automaten, Schriften des Institutes für Instrumentelle Mathematik, Bonn, 1962.

    Google Scholar 

  21. Pomello, L., Some equivalence notions for concurrent systems. An overview. In: Advances in Petri Nets 1985 (G. Rozenberg, ed.), Springer LNCS 222, 1986, pp. 381–400.

    Google Scholar 

  22. Pratt, V.R., On the Composition of Processes, Proc. of the 9th POPL, 1982, pp. 213–223.

    Google Scholar 

  23. Pratt, V.R., Modelling Concurrency with Partial Orders, International Journal of Parallel Programming, Vol. 15, No. 1, 1986, pp. 33–71.

    Article  Google Scholar 

  24. Reed, G.M. & A.W. Roscoe, A Timed Model for Communicating Sequential Processes, In: Proc. ICALP 86 (L. Kott, ed.), Springer LNCS 226, 1986, pp. 314–323.

    Google Scholar 

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

    Google Scholar 

  26. Rozenberg, G. & P.S. Thiagarajan, Petri nets: basic notions, structure, behaviour. In: Current Trends in Concurrency, Overviews and Tutorials (J.W. de Bakker, W.P. de Roever, G. Rozenberg, eds.), Springer LNCS 224, 1986, pp. 585–668.

    Google Scholar 

  27. Winskel, G., Event structure semantics for CCS and related languages, In: Proc. 9th ICALP (M. Nielsen & E.M. Schmidt, eds.), Springer LNCS 140, 1982, pp. 561–576.

    Google Scholar 

  28. Winskel, G., A new definition of morphism on Petri net, In: Proc. STACS 84 (M. Fontet, K. Mehlhorn, eds.), Springer LNCS 166, 1984, pp. 140–150.

    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

    Rob van Glabbeek & Frits Vaandrager

Authors
  1. Rob van Glabbeek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frits Vaandrager
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker A. J. Nijman P. C. Treleaven

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Glabbeek, R., Vaandrager, F. (1987). Petri net models for algebraic theories of concurrency. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds) PARLE Parallel Architectures and Languages Europe. PARLE 1987. Lecture Notes in Computer Science, vol 259. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-17945-3_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-17945-3_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-17945-0

  • Online ISBN: 978-3-540-47181-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation