Skip to main content
SpringerLink
Log in

A compositional partial order semantics for Petri net components

  • Regular Papers
  • Conference paper
  • First Online:
Application and Theory of Petri Nets 1997 (ICATPN 1997)

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

Included in the following conference series:

Abstract

In this paper we introduce the concept of a Petri net component and show how systems can be composed from components. A component communicates with its environment via distinguished input and output places, which formalizes communication by message passing. Then, we present a compositional semantics for components. The semantics is an extension of processes for place/transition systems (partial order semantics). We show that the semantics is fully abstract with respect to the behaviour of closed components (essentially, processes of place/transition systems). A main feature of the compositional semantics is that composition of components corresponds to conjunction. This feature makes the compositional semantics applicable in combination with a temporal logic, which then allows to reason about systems in a compositional way. This is demonstrated by help of a simple temporal logic.

Supported by the DFG (SFB 342, TP YE1)

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. Martín Abadi and Leslie Lamport. Composing specifications. In J.W. de Bakker and W.-P. de Roever, editors, Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness, LNCS 430. Springer-Verlag, 1990.

    Google Scholar 

  2. Martín Abadi and Leslie Lamport. Conjoining specifications. Research Report 118, Digital Equipment Corporation, System Research Center, December 1993.

    Google Scholar 

  3. Howard Barringer, Ruurd Kuiper, and Amir Pnueli. Now you may compose temporal logic specifications. In 16th annual ACM Symposium on Theory of Computing, pages 51–63. ACM, April 1984.

    Google Scholar 

  4. Bernd Baumgarten. On internal and external characterizations of PT-net building block behaviour. In G. Rozenberg, editor, Advances in Petri Nets 1988, LNCS 340, pages 44–61. Springer-Verlag, 1988.

    Google Scholar 

  5. E. Best, R. Devillers, and F.G. Hall. The box calculus: A new causal algebra with multi-label communication. In G. Rozenberg, editor, Advances in Petri nets 1992, LNCS 609, pages 21–69. Springer-Verlag, 1992.

    Google Scholar 

  6. Eike Best and César Fernández. Nonsequential Processes, EATCS Monographs on Theoretical Computer Science 13. Springer-Verlag, 1988.

    Google Scholar 

  7. K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.

    Google Scholar 

  8. Søren Christensen and Niels D. Hansen. Coloured Petri nets extended with channels for synchronous communication. In R. Valette, editor, Application and Theory of Petri Nets 1994, LNCS 815, pages 159–178. Springer-Verlag, 1994.

    Google Scholar 

  9. U. Goltz and W. Reisig. The non-sequential behaviour of Petri nets. Information and Control, 57:125–147, 1983.

    Article  Google Scholar 

  10. Dominik Gomm, Ekkart Kindler, Barbara Paech, and Rolf Walter. Compositional liveness properties of EN-systems. In M. Ajmone Marsan, editor, Applications and Theory of Petri Nets 1993, 14th International Conference, LNCS 619, pages 262–281, Chicago, Illinois, USA, June 1993. Springer-Verlag.

    Google Scholar 

  11. Cliff. B. Jones. Specification and design of (parallel) programs. In R.E.A. Mason, editor, Information Processing, pages 321–332. IFIP, Elsevier Science Publishers B.V. (North Holland), 1983.

    Google Scholar 

  12. Ekkart Kindler. Modularer Entwurf verteilter Systeme mit Petrinetzen, Edition Versal 1. Bertz Verlag, December 1995. Dissertation, Technische Universität München.

    Google Scholar 

  13. Ekkart Kindler and Wolfgang Reisig. Algebraic system nets for modelling distributed algorithms. Petri Net Newsletter, 51:16–31, December 1996.

    Google Scholar 

  14. Ekkart Kindler, Wolfgang Reisig, Hagen Völzer, and Rolf Walter. Petri net based verification of distributed algorithms: An example. Informatik-Berichte 63, Humboldt-Universität zu Berlin, May 1996.

    Google Scholar 

  15. Ekkart Kindler and Rolf Walter, Message passing mutex. In J. Desel, editor, Structures in Concurrency Theory, Workshops in Computing, pages 205–219, Berlin, May 1995. Springer-Verlag.

    Google Scholar 

  16. Ekkart Kindler and Rolf Walter. Mutex needs fairness. Information Processing Letters, 1997. to appear.

    Google Scholar 

  17. Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer-Verlag, 1992.

    Google Scholar 

  18. Antoni Mazurkiewicz. Compositional semantics of pure place/transition systems. In G. Rozenberg, editor, Advances in Petri Nets 1988, LNCS 340, pages 307–330. Springer-Verlag, 1988.

    Google Scholar 

  19. Mogens Nielsen, Lutz Priese, and Vladimiro Sassone. Characterizing behavioural congruences for Petri nets. In I. Lee and S.A. Smolka, editors, CONCUR '95: Concurrency Theory, LNCS 962, pages 175–189. Springer-Verlag, August 1995.

    Google Scholar 

  20. Paritosh K. Pandya. Some comments on the assumption-commitment framework for compositional verification of distributed programs. In de Bakker, de Roever, and Rozenberg, editors, Stepwise Refinement of Distributed Systems, LNCS 430, pages 622–640. Springer-Verlag, 1990.

    Google Scholar 

  21. Amir Pnueli. In transition from global to modular temporal reasoning about programs. In K.R. Apt, editor, Logics and Models of Concurrent Systems, Series F: Computer and System Science 13, pages 123–144. Springer-Verlag, 1985.

    Google Scholar 

  22. Lutz Priese and Harro Wimmel. On some compositional Petri net semantics. Fachberichte Informatik 20/95, Universität Koblenz-Landau, 1995.

    Google Scholar 

  23. Wolfgang Reisig. Das Verhalten verteilter Systeme. GMD-Bericht 170. Oldenbourg Verlag. 1987.

    Google Scholar 

  24. Wolfgang Reisig. Elements of a temporal logic coping with concurrency. SFB-Bericht 342/23/92 A, Technische Universiät München, November 1992.

    Google Scholar 

  25. Wolfgang Reisig. Petri net models of distributed algorithms. In Jan van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, LNCS 1000, pages 441–454. Springer-Verlag, 1995.

    Google Scholar 

  26. C. Sibertin-Blanc. A client-server protocol for the composition of Petri nets. In M. Ajmone Marsan, editor, Application and Theory of Petri Nets 1993, 14 th International Conference, LNCS 691, pages 377–396. Springer-Verlag, June 1993.

    Google Scholar 

  27. C. Sibertin-Blanc. Cooperative nets. In R. Valette, editor, Application and Theory of Petri Nets, 15 th International Conference, LNCS 815, pages 471–490. Springer-Verlag, June 1994.

    Google Scholar 

  28. Younes Souissi and Gérard Memmi. Composition of nets via a communication medium. In G. Rozenberg, editor, Advances in Petri Nets 1990, LNCS 483, pages 457–470. Springer-Verlag, 1990.

    Google Scholar 

  29. Antti Valmari. Compositional analysis with place-bordered subnets. In R. Valette, editor, Application and Theory of Petri Nets, LNCS 815, pages 531–547. Springer-Verlag, 1994.

    Google Scholar 

  30. R. Walter, H. Völzer, T. Vesper, W. Reisig, E. Kindler, J. Freiheit, and J. Desel. Memorandum: Petrinetzmodelle zur Verifikation verteilter Algorithmen. Informatik-Bericht 67, Humboldt-Universität zu Berlin, July 1996.

    Google Scholar 

  31. Harro Wimmel and Lutz Priese. An application of compositional Petri net semantics. Fachberichte Informatik 14/96, Universität Koblenz-Landau, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Humboldt-Universität zu Berlin, D-10099, Berlin, Germany

    Ekkart Kindler

Authors
  1. Ekkart Kindler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Pierre Azéma Gianfranco Balbo

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kindler, E. (1997). A compositional partial order semantics for Petri net components. In: Azéma, P., Balbo, G. (eds) Application and Theory of Petri Nets 1997. ICATPN 1997. Lecture Notes in Computer Science, vol 1248. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63139-9_39

Download citation

  • DOI: https://doi.org/10.1007/3-540-63139-9_39

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation