View article

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. 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. 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.