Skip to main content

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

  • 1407 Accesses

Abstract

The causal semantics of standard net classes like Elementary Net Systems and Place/Transition Nets, is typically expressed in terms of partially ordered sets of transition occurrences. In each such partial order, causally related occurrences are ordered while concurrent transition occurrences remain unordered. Partial order semantics can, in particular, support model checking by efficient verification techniques based on net unfoldings.

To enhance the modelling power of standard net classes, one can introduce different forms of ‘testing’ using, for example, inhibitor arcs. However, the causal semantics of such extended nets can often no longer be described solely in terms of partial orders. In this paper, we explain what modifications to the partial order semantics are needed in order to provide a satisfactory treatment for nets with activator, inhibitor and mutex arcs. On the technical side, the proposed solution is based on causal structures which enrich partial orders with additional order relations corresponding to other aspects of causality. With en-systems as our starting point, we discuss how their extensions can be treated using these richer notions of causality.

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 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. Best, E., Devillers, R.: Sequential and concurrent behaviour in Petri net theory. Theor. Comput. Sci. 55(1), 87–136 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  2. Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)

    Google Scholar 

  3. Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  4. Esparza, J., Heljanko, K.: Unfoldings: A Partial Order Approach to Model Checking. Monographs in Theoretical Computer Science. Springer (2008)

    Google Scholar 

  5. Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 87–106. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  6. Gaifman, H., Pratt, V.R.: Partial order models of concurrency and the computation of functions. In: LICS, pp. 72–85. IEEE Computer Society (1987)

    Google Scholar 

  7. Guo, G., Janicki, R.: Modelling concurrent behaviours by commutativity and weak causality relations. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 178–191. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Hoogers, P.W., Kleijn, H.C.M., Thiagarajan, P.S.: A trace semantics for Petri nets. Inf. Comput. 117(1), 98–114 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  9. Hoogers, P.W., Kleijn, H.C.M., Thiagarajan, P.S.: An event structure semantics for general Petri nets. Theor. Comput. Sci. 153(1&2), 129–170 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  10. Janicki, R.: Relational structures model of concurrency. Acta Inf. 45(4), 279–320 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  11. Janicki, R., Kleijn, J., Koutny, M.: Quotient monoids and concurrent behaviour. In: Martín-Vide, C. (ed.) Mathematics, Computing, Language, and Life: Frontiers in Mathematical Linguistics and Language Theory, vol. 2, pp. 313–386. World Scientific (2010)

    Google Scholar 

  12. Janicki, R., Koutny, M.: Invariants and paradigms of concurrency theory. In: Aarts, E.H.L., van Leeuwen, J., Rem, M. (eds.) PARLE 1991. LNCS, vol. 506, pp. 59–74. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  13. Janicki, R., Koutny, M.: Structure of concurrency. Theor. Comput. Sci. 112(1), 5–52 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  14. Janicki, R., Koutny, M.: Semantics of inhibitor nets. Inf. Comput. 123(1), 1–16 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  15. Janicki, R., Koutny, M.: Fundamentals of modelling concurrency using discrete relational structures. Acta Inf. 34(5), 367–388 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  16. Janicki, R., Le, D.T.M.: Modelling concurrency with comtraces and generalized comtraces. Inf. Comput. 209(11), 1355–1389 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  17. Juhás, G., Lorenz, R., Mauser, S.: Complete process semantics of Petri nets. Fundam. Inform. 87(3-4), 331–365 (2008)

    MATH  Google Scholar 

  18. Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. Acta Inf. 40(2), 95–118 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  19. Kleijn, H.C.M., Koutny, M.: Process semantics of general inhibitor nets. Inf. Comput. 190(1), 18–69 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  20. Kleijn, J., Koutny, M.: Processes of Petri nets with range testing. Fundam. Inform. 80(1-3), 199–219 (2007)

    MathSciNet  MATH  Google Scholar 

  21. Kleijn, J., Koutny, M.: The mutex paradigm of concurrency. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol. 6709, pp. 228–247. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  22. Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Tech. Rep. DAIMI PB 78, Aarhus University (1977)

    Google Scholar 

  23. McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–177. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  24. Montanari, U., Rossi, F.: Contextual nets. Acta Inf. 32(6), 545–596 (1995)

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  26. Reisig, W., Rozenberg, G. (eds.): Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996, Lecture Notes in Computer Science, vol. 1491. Springer (1998)

    MATH  Google Scholar 

  27. Rozenberg, G., Engelfriet, J.: Elementary net systems. In: Reisig, Rozenberg (eds.) [26], pp. 12–121

    Google Scholar 

  28. Szpilrajn, E.: Sur l’extension de l’ordre partiel. Fundam. Mathem. 16, 386–389 (1930)

    MATH  Google Scholar 

  29. Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kleijn, J., Koutny, M. (2013). Causality in Extensions of Petri Nets. In: Jensen, K., van der Aalst, W.M.P., Balbo, G., Koutny, M., Wolf, K. (eds) Transactions on Petri Nets and Other Models of Concurrency VII. Lecture Notes in Computer Science, vol 7480. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38143-0_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38143-0_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38142-3

  • Online ISBN: 978-3-642-38143-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics