Unfolding of Petri nets with semilinear reachability set

Semilinearity plays a key role not only in formal languages but also in the study of Petri nets. Although the reachability set of a Petri net may not be semilinear in general, there are a wide variety of subclasses of Petri nets which enjoy having semilinear reachability sets. In this paper, we develop sufficient conditions for Petri nets under which semilinearity is guaranteed. Our approach, based on the idea of path decomposition, can be used for consolidating several existing semilinearity results as well as for deriving new results all under the same framework.

Download Full-text

A class of Petri nets with a convex reachability set

[1993] Proceedings IEEE International Conference on Robotics and Automation ◽

10.1109/robot.1993.292041 ◽

2002 ◽

Cited By ~ 3

Author(s):

A. Giua ◽

F. DiCesare

Keyword(s):

Petri Nets ◽

Reachability Set

Download Full-text

Petri nets properties related to the unboundness and analyzed using coverability multigraph

Journal of Applied Mathematics Statistics and Informatics ◽

10.2478/jamsi-2014-001 ◽

2014 ◽

Vol 10 (2) ◽

pp. 51-67 ◽

Cited By ~ 1

Author(s):

Branislav Hrúz ◽

Iveta Dirgová Ľuptáková ◽

Miroslav Beňo

Keyword(s):

Petri Nets ◽

State Space ◽

Petri Net ◽

Discrete Event Systems ◽

Discrete Event ◽

System Model ◽

Reachability Graph ◽

Reachability Set ◽

Event Systems ◽

System States

Abstract Petri nets represent a powerful tool for modeling the discrete event systems. The Petri net markings correspond to the system states. The infinity of the marking set means that the Petri net is unbounded and this may be the sign of an incorrect system model. In that case instead of the reachability set and the reachability graph the coverability set and the coverability multigraph can be used to represent the Petri net state space. A systematic way of building the notion of the coverability set and coverability multigraph based on the notion of the ω -marking is given in the paper. Algorithm for its construction is introduced. Then the use of the coverability multigraph for the analysis of several properties of the unbounded Petri nets is described.

Download Full-text

Acceleration For Presburger Petri Nets

10.29007/8wkd ◽

2018 ◽

Author(s):

Jerome Leroux

Keyword(s):

Petri Nets ◽

Petri Net ◽

Open Problem ◽

Direct Consequence ◽

Reachability Problem ◽

Presburger Arithmetic ◽

Acceleration Techniques ◽

Reachability Set ◽

Bounded Language ◽

Inductive Invariants

The reachability problem for Petri nets is a central problem of net theory. The problem is known to be decidable by inductive invariants definable in the Presburger arithmetic. When the reachability set is definable in the Presburger arithmetic, the existence of such an inductive invariant is immediate. However, in this case, the computation of a Presburger formula denoting the reachability set is an open problem. Recently this problem got closed by proving that if the reachability set of a Petri net is definable in the Presburger arithmetic, then the Petri net is flatable, i.e. its reachability set can be obtained by runs labeled by words in a bounded language. As a direct consequence, classical algorithms based on acceleration techniques effectively compute a formula in the Presburger arithmetic denoting the reachability set.

Download Full-text