Using zone graph method for computing the state space of a time petri net

Abstract

Presently, the method to verify quantitative time properties on Time Petri Nets is the use of observers. The state space is then computed to test the reachability of a given marking. The main method to compute the state space of a Time Petri Net has been introduced by BERTHOMIEU and DIAZ [BD91]. It is known as the "state class method". We present in this paper a new efficient method to compute the state space of a bounded Time Petri Net as a marking graph, based on the region graph method used for Timed Automaton [AD94]. The algorithm is proved to be exact with respect to the reachability of a marking and it computes a graph which nodes are exactly the reachable markings of the Time Petri Net. The tool implemented computes faster than TINA, a tool for constructing the state space using classes, and allows to test on-the-fly the reachability of a given marking. © Springer-Verlag 2004.