We introduce the notion of a T-path within Petri nets, and propose to adopt the model of directed hypergraphs in order to determine properties of nets: in particular, we study the relationships between T-paths and firable sequences of transitions. Let us consider a Petri net P = < P, T, A, M-0 > and the set of places with a positive marking in M-0, i.e., P-0 = {p vertical bar M-0(p) > 0}. If we regard the net as a directed graph, the existence of a simple path from any place in P-0 to a transition t is, of course, a necessary condition for the potential firability of t. This is sufficient only if the net is a state machine, where vertical bar(center dot)t vertical bar = vertical bar t(center dot)vertical bar = 1 for all t epsilon T. In this paper we show that the existence of a T-path from any subset of P-0 to a transition t is a more restrictive condition and is, again, a necessary condition for the potential firability of t. But, in this case: (a) if P is a conflict-free Petri net, this is also a sufficient condition, (b) if P is a general Petri net, t is potentially firable by increasing the number of tokens in P-0. For conflict-free nets (CFPN) we consider the following problems: (a) determining the set of firable transitions, (b) determining the set of covetable places, (c) determining the set of live transitions, (d) deciding the boundedness of the net. For all these problems we provide algorithms requiring linear space and time, i.e., O(vertical bar p vertical bar + vertical bar T vertical bar + vertical bar A vertical bar), for a net P = < P, T, A. M-0 >. Previous results for this class of networks are given by Howell et al. (1987) [20], providing algorithms for solving problems in conflict-free nets in O(vertical bar p vertical bar x vertical bar T vertical bar ) time and space. Given a Petri net and a marking M, the well-known coverability problem consists in finding a reachable marking M` such that M` >= M; this problem is known to be EXPSPACE hard (Rackoff (1978) [33]). For general Petri nets we provide a partial answer to this problem. M is coverable by augmentation if it is coverable from an augmented marking m`(0); of the initial marking M-0: M`(0) >= M-0 and, for all p epsilon P, M`(0)(p) = 0 if M-0(p) = 0. We solve this problem in linear time. The algorithms for computing T-paths are incremental: it is possible to modify the network (adding new places, transitions, arcs, tokens), and update the set of potentially firable transitions and coverable places without recomputing them from scratch. This feature is meaningful when used during the interactive design of a system. (c) 2010 Elsevier B.V. All rights reserved.

Linear time analysis of properties of conflict-free and general Petri nets / Paola, Alimonti; Feuerstein, Esteban; Laura, Luigi; Nanni, Umberto. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - STAMPA. - 412:4-5(2011), pp. 320-338. [10.1016/j.tcs.2010.09.030]

Linear time analysis of properties of conflict-free and general Petri nets

LAURA, Luigi;NANNI, Umberto
2011

Abstract

We introduce the notion of a T-path within Petri nets, and propose to adopt the model of directed hypergraphs in order to determine properties of nets: in particular, we study the relationships between T-paths and firable sequences of transitions. Let us consider a Petri net P = < P, T, A, M-0 > and the set of places with a positive marking in M-0, i.e., P-0 = {p vertical bar M-0(p) > 0}. If we regard the net as a directed graph, the existence of a simple path from any place in P-0 to a transition t is, of course, a necessary condition for the potential firability of t. This is sufficient only if the net is a state machine, where vertical bar(center dot)t vertical bar = vertical bar t(center dot)vertical bar = 1 for all t epsilon T. In this paper we show that the existence of a T-path from any subset of P-0 to a transition t is a more restrictive condition and is, again, a necessary condition for the potential firability of t. But, in this case: (a) if P is a conflict-free Petri net, this is also a sufficient condition, (b) if P is a general Petri net, t is potentially firable by increasing the number of tokens in P-0. For conflict-free nets (CFPN) we consider the following problems: (a) determining the set of firable transitions, (b) determining the set of covetable places, (c) determining the set of live transitions, (d) deciding the boundedness of the net. For all these problems we provide algorithms requiring linear space and time, i.e., O(vertical bar p vertical bar + vertical bar T vertical bar + vertical bar A vertical bar), for a net P = < P, T, A. M-0 >. Previous results for this class of networks are given by Howell et al. (1987) [20], providing algorithms for solving problems in conflict-free nets in O(vertical bar p vertical bar x vertical bar T vertical bar ) time and space. Given a Petri net and a marking M, the well-known coverability problem consists in finding a reachable marking M` such that M` >= M; this problem is known to be EXPSPACE hard (Rackoff (1978) [33]). For general Petri nets we provide a partial answer to this problem. M is coverable by augmentation if it is coverable from an augmented marking m`(0); of the initial marking M-0: M`(0) >= M-0 and, for all p epsilon P, M`(0)(p) = 0 if M-0(p) = 0. We solve this problem in linear time. The algorithms for computing T-paths are incremental: it is possible to modify the network (adding new places, transitions, arcs, tokens), and update the set of potentially firable transitions and coverable places without recomputing them from scratch. This feature is meaningful when used during the interactive design of a system. (c) 2010 Elsevier B.V. All rights reserved.
2011
boundedness; conflict-free petri nets; coverability; directed hypergraphs; incremental algorithms; liveness; marked graphs; petri nets
01 Pubblicazione su rivista::01a Articolo in rivista
Linear time analysis of properties of conflict-free and general Petri nets / Paola, Alimonti; Feuerstein, Esteban; Laura, Luigi; Nanni, Umberto. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - STAMPA. - 412:4-5(2011), pp. 320-338. [10.1016/j.tcs.2010.09.030]
File allegati a questo prodotto
File Dimensione Formato  
VE_2011_11573-230643.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 403.64 kB
Formato Adobe PDF
403.64 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/230643
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 8
social impact