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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Best, E., Devillers, R.: Sequential and concurrent behaviour in Petri net theory. Theor. Comput. Sci. 55(1), 87–136 (1987)
Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)
Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991)
Esparza, J., Heljanko, K.: Unfoldings: A Partial Order Approach to Model Checking. Monographs in Theoretical Computer Science. Springer (2008)
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)
Gaifman, H., Pratt, V.R.: Partial order models of concurrency and the computation of functions. In: LICS, pp. 72–85. IEEE Computer Society (1987)
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)
Hoogers, P.W., Kleijn, H.C.M., Thiagarajan, P.S.: A trace semantics for Petri nets. Inf. Comput. 117(1), 98–114 (1995)
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)
Janicki, R.: Relational structures model of concurrency. Acta Inf. 45(4), 279–320 (2008)
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)
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)
Janicki, R., Koutny, M.: Structure of concurrency. Theor. Comput. Sci. 112(1), 5–52 (1993)
Janicki, R., Koutny, M.: Semantics of inhibitor nets. Inf. Comput. 123(1), 1–16 (1995)
Janicki, R., Koutny, M.: Fundamentals of modelling concurrency using discrete relational structures. Acta Inf. 34(5), 367–388 (1997)
Janicki, R., Le, D.T.M.: Modelling concurrency with comtraces and generalized comtraces. Inf. Comput. 209(11), 1355–1389 (2011)
Juhás, G., Lorenz, R., Mauser, S.: Complete process semantics of Petri nets. Fundam. Inform. 87(3-4), 331–365 (2008)
Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. Acta Inf. 40(2), 95–118 (2003)
Kleijn, H.C.M., Koutny, M.: Process semantics of general inhibitor nets. Inf. Comput. 190(1), 18–69 (2004)
Kleijn, J., Koutny, M.: Processes of Petri nets with range testing. Fundam. Inform. 80(1-3), 199–219 (2007)
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)
Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Tech. Rep. DAIMI PB 78, Aarhus University (1977)
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)
Montanari, U., Rossi, F.: Contextual nets. Acta Inf. 32(6), 545–596 (1995)
Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part I. Theor. Comput. Sci. 13, 85–108 (1981)
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)
Rozenberg, G., Engelfriet, J.: Elementary net systems. In: Reisig, Rozenberg (eds.) [26], pp. 12–121
Szpilrajn, E.: Sur l’extension de l’ordre partiel. Fundam. Mathem. 16, 386–389 (1930)
Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)