Computing the State Class Timed Automaton of a Time Petri Net

Abstract. This report describes a method for building the state class graph of a bounded time Petri net (TPN) as a timed automaton (TA). We consider bounded TPN, whose un-derlying net is not necessarily bounded. We prove that the obtained TA is timed-bisimilar to the initial TPN. The number of clocks of the automaton is much lower than with other methods available. We have implemented the method, and give some experimental results in this report, illustrating the efficiency of the translation algorithm in terms of clock number