Time Analysis of the State Space of Real-Time Preemptive Systems
The authors 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, they discuss how to determine from the reachability graph linear and quantitative properties of the remote model. Then, they propose an algorithm to compute an approximation of the minimal and the maximal time distances of any firing sequence. Contrarily to other techniques, their 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.