Time Analysis of the State Space of Real-time Preemptive Systems

We present in this paper an algorithm making it possible an efficient time analysis of the state space of preemptive real time systems modeled using Time Petri Nets with inhibitor arcs. For this effect, we discuss how to determine from the reachability graph linear and quantitative properties of the remote model. Then, we propose an algorithm to compute an approximation of the minimal and the maximal time distances of any firing sequence. Contrarily to other techniques, our algorithm enjoys a linear complexity time cost and can be performed on the fly when building the reachability graph without requiring to extend the original model with observers.