On-The-Fly Model Checking of Timed Properties on Time Petri Nets

Abstract. This paper deals with model checking of timed systems mod-eled by Time Petri nets (TPN). We propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behavior of bounded TPNs with strong time semantics. The main feature of this abstract rep-resentation compared to existing approaches is the encoding of the time information. This is done in a pure way within each node of the TAG allowing to compute the minimum and maximum elapsed time in every path of the graph. The TAG preserves runs and reachable states of the corresponding TPN and allows for on-the-fly verification of reachability properties. We illustrate in this paper how the TAG can be used to check some usual timed reachability properties and we supply an algorithm for extracting an explicit timed trace (involving the elapsed time before each fired transition) from an abstract run of the TAG. The TAG-based ap-proach is implemented and compared to two well known TPNs analysis approaches.