Skip to main content

A Canonical Contraction for Safe Petri Nets

  • Chapter
  • First Online:
Transactions on Petri Nets and Other Models of Concurrency IX

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 8910))

Abstract

Under maximal semantics, the occurrence of an event \(a\) in a concurrent run of an occurrence net may imply the occurrence of other events, not causally related to \(a\), in the same run. In recent works, we have formalized this phenomenon as the reveals relation, and used it to obtain a contraction of sets of events called facets in the context of occurrence nets. Here, we extend this idea to propose a canonical contraction of general safe Petri nets into pieces of partial-order behaviour which can be seen as “macro-transitions” since all their events must occur together in maximal semantics. On occurrence nets, our construction coincides with the facets abstraction.Our contraction preserves the maximal semantics in the sense that the maximal processes of the contracted net are in bijection with those of the original net.

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

Access this chapter

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 EPUB and 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

Notes

  1. 1.

    Notice that \((B, E, F, {^{\bullet }{E'}} \setminus {{E'}^{\bullet }})\) is not an occurrence net in general: it satisfies items 3, 4 and 5 of Definition 2, but items 1 and 2 may not hold.

  2. 2.

    The depth of an event \(e\) is the size of the longest path from an initial condition to \(e\).

  3. 3.

    By “\(\phi \) starts by \(t\)”, we mean that there exists an event in \(\phi \) which is mapped to \(t\) and consumes only initial conditions of \(\phi \).

References

  1. Balaguer, S., Chatain, T., Haar, S.: Building tight occurrence nets from reveals relations. In: Proceedings of the 11th International Conference on Application of Concurrency to System Design, pp. 44–53. IEEE Computer Society Press (2011)

    Google Scholar 

  2. Balaguer, S., Chatain, T., Haar, S.: Building occurrence nets from reveals relations. Fundam. Inform. 123(3), 245–272 (2013)

    MATH  MathSciNet  Google Scholar 

  3. Berthelot, G.: Checking properties of nets using transformation. In: Rozenberg, G. (ed.) APN 1985. LNCS, vol. 222, pp. 19–40. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  4. Best, E., Randell, B.: A formal model of atomicity in asynchronous systems. Acta Inform. 16(1), 93–124 (1981)

    Article  MATH  Google Scholar 

  5. Desel, J., Merceron, A.: Vicinity respecting homomorphisms for abstracting system requirements. In: Proceedings of International Workshop on Abstractions for Petri Nets and Other Models of Concurrency (APNOC) (2009)

    Google Scholar 

  6. Haar, S.: Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Trans. Autom. Control 55(10), 2310–2320 (2010)

    Article  MathSciNet  Google Scholar 

  7. Haar, S., Kern, C., Schwoon, S.: Computing the reveals relation in occurrence nets. In: Proceedings of GandALF’11. Electronic Proceedings in Theoretical Computer Science, vol. 54, pp. 31–44 (2011)

    Google Scholar 

  8. Kumar, R., Takai, S.: Decentralized prognosis of failures in discrete event systems. IEEE Trans. Autom. Control 55(1), 48–59 (2010)

    Article  MathSciNet  Google Scholar 

  9. Madalinski, A., Khomenko, V.: Diagnosability verification with parallel LTL-X model checking based on Petri net unfoldings. In: Control and Fault-Tolerant Systems (SysTol’2010), pp. 398–403. IEEE Computing Society Press (2010)

    Google Scholar 

  10. Madalinski, A., Khomenko, V.: Predictability verification with parallel LTL-X model checking based on Petri net unfoldings. In: Proceedings of the 8th IFAC Symposium on Fault Detection, Diagnosis and Safety of Technical Processes (SAFEPROCESS’2012), pp. 1232–1237 (2012)

    Google Scholar 

  11. Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part I. Theoret. Comput. Sci. 13, 85–108 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  12. Zielonka, W.: Notes on finite asynchronous automata. RAIRO Theoret. Inform. Appl. 21, 99–135 (1987)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Thomas Chatain .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Chatain, T., Haar, S. (2014). A Canonical Contraction for Safe Petri Nets. In: Koutny, M., Haddad, S., Yakovlev, A. (eds) Transactions on Petri Nets and Other Models of Concurrency IX. Lecture Notes in Computer Science(), vol 8910. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45730-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-45730-6_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-45729-0

  • Online ISBN: 978-3-662-45730-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics