Linear time analysis of properties of conflict-free and general Petri nets
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,M0〉 and the set...
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Artículo publishedVersion |
| Publicado: |
2011
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03043975_v412_n4-5_p320_Alimonti https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03043975_v412_n4-5_p320_Alimonti_oai |
| Aporte de: |
| id |
I28-R145-paper_03043975_v412_n4-5_p320_Alimonti_oai |
|---|---|
| record_format |
dspace |
| spelling |
I28-R145-paper_03043975_v412_n4-5_p320_Alimonti_oai2024-08-16 Alimonti, P. Feuerstein, E. Laura, L. Nanni, U. 2011 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,M0〉 and the set of places with a positive marking in M0, i.e., P0=p|M0(p)>0. If we regard the net as a directed graph, the existence of a simple path from any place in P0 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 |•t|=|t•|=1 for all t∈T. In this paper we show that the existence of a T-path from any subset of P0 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 P0. For conflict-free nets (CFPN) we consider the following problems: (a) determining the set of firable transitions, (b) determining the set of coverable 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(|P|+|T|+|A|), for a net P=〈P,T,A,M0〉. 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(|P|×|T|) 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 M0′ of the initial marking M0: M0′<M0 and, for all p∈P, M0′(p)=0 if M0(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. © 2010 Elsevier B.V. All rights reserved. application/pdf http://hdl.handle.net/20.500.12110/paper_03043975_v412_n4-5_p320_Alimonti info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar Theor Comput Sci 2011;412(4-5):320-338 Boundedness Conflict-free Petri nets Coverability Directed hypergraphs Incremental algorithms Liveness Marked graphs Petri nets Boundedness Conflict free Coverability Directed hypergraphs Incremental algorithm Liveness Marked graphs Algorithms Graph theory Petri nets Teaching Problem solving Linear time analysis of properties of conflict-free and general Petri nets info:eu-repo/semantics/article info:ar-repo/semantics/artículo info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03043975_v412_n4-5_p320_Alimonti_oai |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-145 |
| collection |
Repositorio Digital de la Universidad de Buenos Aires (UBA) |
| topic |
Boundedness Conflict-free Petri nets Coverability Directed hypergraphs Incremental algorithms Liveness Marked graphs Petri nets Boundedness Conflict free Coverability Directed hypergraphs Incremental algorithm Liveness Marked graphs Algorithms Graph theory Petri nets Teaching Problem solving |
| spellingShingle |
Boundedness Conflict-free Petri nets Coverability Directed hypergraphs Incremental algorithms Liveness Marked graphs Petri nets Boundedness Conflict free Coverability Directed hypergraphs Incremental algorithm Liveness Marked graphs Algorithms Graph theory Petri nets Teaching Problem solving Alimonti, P. Feuerstein, E. Laura, L. Nanni, U. Linear time analysis of properties of conflict-free and general Petri nets |
| topic_facet |
Boundedness Conflict-free Petri nets Coverability Directed hypergraphs Incremental algorithms Liveness Marked graphs Petri nets Boundedness Conflict free Coverability Directed hypergraphs Incremental algorithm Liveness Marked graphs Algorithms Graph theory Petri nets Teaching Problem solving |
| description |
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,M0〉 and the set of places with a positive marking in M0, i.e., P0=p|M0(p)>0. If we regard the net as a directed graph, the existence of a simple path from any place in P0 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 |•t|=|t•|=1 for all t∈T. In this paper we show that the existence of a T-path from any subset of P0 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 P0. For conflict-free nets (CFPN) we consider the following problems: (a) determining the set of firable transitions, (b) determining the set of coverable 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(|P|+|T|+|A|), for a net P=〈P,T,A,M0〉. 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(|P|×|T|) 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 M0′ of the initial marking M0: M0′<M0 and, for all p∈P, M0′(p)=0 if M0(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. © 2010 Elsevier B.V. All rights reserved. |
| format |
Artículo Artículo publishedVersion |
| author |
Alimonti, P. Feuerstein, E. Laura, L. Nanni, U. |
| author_facet |
Alimonti, P. Feuerstein, E. Laura, L. Nanni, U. |
| author_sort |
Alimonti, P. |
| title |
Linear time analysis of properties of conflict-free and general Petri nets |
| title_short |
Linear time analysis of properties of conflict-free and general Petri nets |
| title_full |
Linear time analysis of properties of conflict-free and general Petri nets |
| title_fullStr |
Linear time analysis of properties of conflict-free and general Petri nets |
| title_full_unstemmed |
Linear time analysis of properties of conflict-free and general Petri nets |
| title_sort |
linear time analysis of properties of conflict-free and general petri nets |
| publishDate |
2011 |
| url |
http://hdl.handle.net/20.500.12110/paper_03043975_v412_n4-5_p320_Alimonti https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=artiaex&d=paper_03043975_v412_n4-5_p320_Alimonti_oai |
| work_keys_str_mv |
AT alimontip lineartimeanalysisofpropertiesofconflictfreeandgeneralpetrinets AT feuersteine lineartimeanalysisofpropertiesofconflictfreeandgeneralpetrinets AT laural lineartimeanalysisofpropertiesofconflictfreeandgeneralpetrinets AT nanniu lineartimeanalysisofpropertiesofconflictfreeandgeneralpetrinets |
| _version_ |
1809357220176986112 |