 |
|
|
CSC -- Efficient computation of the Coverability Set of Petri nets  |
|
|
|
|
|
CSC -- Efficient computation of the Coverability Set of Petri nets |
|
Petri nets are a very widespread formalism for the representation and the analysis of e.a. concurrent systems or business processes... They have been widely studied since their introduction in the 60's.
States of a Petri nets are called markings. A notable property of Petri nets is that their reachability set (i.e., the set of all the possible states that the Petri net can reach) is, in general, infinite. Moreover, this set is difficult to represent and handle, since it is known to be non-semi-linear (it cannot be represented in the Pressburger arthmetics, for instance).
As a consequence, several approximations of this reachability set, which are easier to represent and manipulate, have been studied. The most prominent of these approximations is called the coverability set. This set is an over-approximation of the reachable markings that is still conservative for many meaningful properties of the net, such as:
The coverability set of a Petri net is known to be computable, since the works of Karp and Miller (see references hereunder). Since then, several alternatives to the Karp and Miller algorithm have been proposed, in order to improve on its efficiency. Unfortunately, several of them are not correct, in the sense that they may compute an under-approximation of the reachable markings, or they may not terminate (see references hereunder).
This tool implements the efficient algorithm introduced by Geeraerts, Raskin and Van Begin, in 2007. The implementation is built on top of the IST datastructure, a symbolic structure for representing sets of tuples of interval of integer numbers. Experiments show that this implementation can handle instances of Petri nets with 50 places, whereas the Karp and Miller procedure can hardly cope with nets of 20 places.
You can download here version 0.1 of CSC. This prototype is still experimental, and the output it produces is sometimes very verboose...
The archive contains the sources of CSC, as well as the .spec files describing the examples we have tried. For a description of the examples, go here. For a description of the syntax of the input go here.
To compile the tool, uncompress the sources, then type ./configure, followed by make. The archive contains all the necessary sources to compile (including the IST library).
People involved in the development of this tool: