Efficient computation of state space over approximation of preemptive real time systems

In preemptive real time systems, clocks that are associated with tasks, can be suspended and resumed afterwards. The exact analyzes of such systems induce unfortunately an exponential computation complexity. To reduce the latter, we present in this paper an algorithm allowing an efficient computation of a DBM over approximation of the state class graph of such systems modeled using Time Petri Nets with inhibitor arcs. For this effect, we express each class of the approximated graph as a pair (M, D^~) where M is a marking and D^~ is a matrix encoding the DBM time constraints. Therefore, thanks to the definition of a suitable class equivalence condition, the enumeration process yields a much compact graph than other existing DBM approximation techniques, such that the computation complexity of each class is square in the number of enabled transitions. To advocate our proposal, we give some experimental results that compare our algorithm with other existing approaches.