Towards Building the State Class Graph of the TSPN Model
In this paper, we propose an enumerative approach to build the state class graph of the T S P N ( Time Stream Petri Net) model. A T S P N model is a Petri net augmented with intervals on arcs and synchronization rules on transitions. It can be used to model complex systems, and it is proved to be more expressive than T P N ( Time Petri Nets). In contrast with T P N where each class accessible in the graph is given as a pair ( M, D) where M is a marking and D is a system of D B M inequalities, a T S P N class in this form is much complex to compute. To tackle this issue, we introduce a new formalism called the time distance function to define a T S P N class. This function makes it possible to determine an efficient algorithm to compute each class of the graph in a square complexity time. Finally, we show how to exploit the T S P N state class graph ( when finite), to check over either linear properties of the model, or to compute minimal and maximal time distances of any firing sequence.
state class graph time stream petri net time petri net time distance function difference bound matrix multimedia