Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets

In this paper, we propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behavior of bounded Time Petri Nets (TPN) with strong time semantics. The main feature of this abstract representation compared to existing approaches is the used criterion to encapsulate the elapsing of time within each node of the TAG (called aggregate), and how to maintain the relative differences between the firing times of enabled transitions. We prove that the TAG preserves timed traces and reachable states of the corresponding TPN. Another interesting and novel feature of the TAGs is the possibility of extracting an explicit run from any of its traces. Thus, we supply an algorithm that maps an abstract run of the TAG to an explicit timed trace (involving a relative elapsed time before each fired transition) of the corresponding TPN. Moreover, the fact that the TAG preserves the timed behavior of the corresponding TPN makes it directly usable in order to check both event- and state-based timed properties as well as the Zenoness property. Zenoness is a pathological behavior which violate a fundamental progress requirement for timed systems stating that it should be possible for time to diverge. A TPN is said to be Zeno when it admits a run where an infinity of transitions are fired in a finite amount of time. We give an algorithm allowing to detect the Zenoness of bounded TPNs and compare the size of the TAG to two well known approaches namely the state class graph and the zone-based graph methods.