Skip to main content
SpringerLink
Log in

A Concurrent and Compositional Petri Net Semantics of Preemption

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2000)

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

Included in the following conference series:

Abstract

The aim of this paper is the introduction of preemption in a compositional model, called M-nets, which is based on Petri nets and hence provided with a concurrent semantics. We propose a way to model preemptible systems by extending the M-net model with priorities and the M-net algebra with a preemption operator. We show that these extensions can be seen as a high-level version of the well studied model of priority systems, and so, can be reduced to Petri nets (without priori- ties) which retain as much as possible of the original concurrency. As a consequence, Petri nets appear as a model powerful enough to deal with preemption in a compositional way and with a concurrent semantics.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Berry. The Foundations of Esterel. Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling and M. Tofte, editors, MIT Press, 1998.

    Google Scholar 

  2. E. Best, R. Devillers, and J. Esparza. General refinement and recursion operators for the Petri box calculus. LNCS 665:130–140, 1993.

    Google Scholar 

  3. E. Best, R. Devillers, and J. G. Hall. The box calculus: a new causal algebra with multi-label communication. LNCS 609:21–69, 1992.

    Google Scholar 

  4. E. Best, W. Fraczak, R. Hopkins, H. Klaudel, and E. Pelz. M-nets: An algebra of high-level Petri nets, with an application to the semantics of concurrent programming languages. Acta Informatica, 35, 1998.

    Google Scholar 

  5. E. Best and R. P. Hopkins. B(PN)2 — A basic Petri net programming notation. PARLE’93, LNCS 694:379–390, 1993.

    Google Scholar 

  6. E. Best and M. Koutny. Petri net semantics of priority systems. Theoretical Computer Science, 96(1):175–215, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  7. E. Best and H. Wimmel. Reducing k-safe Petri nets to pomset-equivalent 1-safe Petri nets. ICATPN’2000, to appear.

    Google Scholar 

  8. R. Devillers, H. Klaudel, and R.-C Riemann. General refinement for high-level Petri nets. FST&TCS’97, LNCS 1346:297–311, 1997.

    Google Scholar 

  9. H. J. Genrich, K. Lautenbach, and P.S. Thiagarajan. Elements of General Net Theory. In W. Brauer, editor, Net Theory and Applications, Proceedings of the Advanced Course on General Net Theory of Processes and Systems, LNCS 84:21–163, 1980.

    Google Scholar 

  10. R. Devillers, H. Klaudel, and R.-C. Riemann. General parameterised refinement and recursion for the M-net calculus. Theoretical Computer Science, to appear.

    Google Scholar 

  11. J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23(2-3):151–195, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  12. H. Fleishhack and B. Grahlmann. A Petri net semantics for B(PN)2 with procedures. PDSE’97, Boston, 1997. IEEE Computer Society.

    Google Scholar 

  13. B. Grahlmann and E. Best. PEP-more than a Petri net tool. LNCS1055, 1996.

    Google Scholar 

  14. N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer Academic Publishers, 1993.

    Google Scholar 

  15. H. Klaudel. Compositional high-level Petri net semantics of a parallel programming language with procedures. Science of Computer Programming, to appear.

    Google Scholar 

  16. H. Klaudel. Parametrized M-expression semantics of parallel procedures. DAP-SYS’00, to appear.

    Google Scholar 

  17. H. Klaudel and F. Pommereau. Asynchronous links in the PBC and M-nets. ASIAN’99, LNCS 1742:190–200, 1999.

    Google Scholar 

  18. H. Klaudel and R.-C. Riemann. High level expressions with their SOS semantics. CONCUR’97, LNCS 1243:288–301, 1997.

    Google Scholar 

  19. H. Klaudel and R.-C. Riemann. Refinement-based semantics od parallel procedures. PDPTA’99, volume 4. CSREA Press, 1999.

    Google Scholar 

  20. J. Lilius and E. Pelz. An M-net semantics of B(PN)2 with procedures. ISCIS, volume 1, 1996.

    Google Scholar 

  21. R. Milner. A calculus of communicating systems. LNCS 92, 1980.

    MATH  Google Scholar 

  22. T. Vesper and M. Weber. Automatishes verteiltes rüchksetzen. In K. Spies and B. Schätz, editors, Proceedings of the workshop “Formale Beschreibungstechniken für verteilte Systeme”, number 9 in GI/ITG Fachgespräch, Munich, 1999.

    Google Scholar 

  23. M. Kishinevsky, J. Cortadella, A. Kondratyev, L. Lavagno, A. Taubin and A. Ya-kovlev. Coupling asynchrony and interrupts: place chart nets and their synthesis. ICATPN’97, LNCS1248:328–347, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LACL, Université Paris XII, 61, avenue du Général de Gaulle, 94010, Créteil, France

    Hanna Klaudel & Franck Pommereau

Authors
  1. Hanna Klaudel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Franck Pommereau
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Sekr.FR 5-13 bzw.5-6, TU Berlin, Franklinstr.28-29, 10587, Berlin, Germany

    Wolfgang Grieskamp  & Thomas Santen  & 

  2. School of Computing and Mathematics, University of Teesside, Middlesbrough, TS1 3BA, UK

    Bill Stoddart

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klaudel, H., Pommereau, F. (2000). A Concurrent and Compositional Petri Net Semantics of Preemption. In: Grieskamp, W., Santen, T., Stoddart, B. (eds) Integrated Formal Methods. IFM 2000. Lecture Notes in Computer Science, vol 1945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40911-4_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-40911-4_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41196-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation