Timed Automata (TA) [1] have emerged as an important formalism for the formal modelling and analysis of timed systems. Reachability analysis forms the core of TA-based verification tools such as UPPAAL [2], which implement a zone-based Forward Reachability Analysis (FRA) algorithm. This analysis, however, does not consider realistic models that are robust w.r.t imprecisions such as drift in the clocks. On the other hand, existing techniques for "robust" reachability analysis of TA [3, 4, 5], which deal with such imprecisions, are not straight-forward to implement. The approaches in [3, 4] are region-based, while that of [5], though zone-based, involves a forward and backward fixpoint alternation, and may not necessarily terminate.
Citation:
Mani Swaminathan, Martin Franzle, "A Symbolic Decision Procedure for Robust Safety of Timed Systems," time, pp.192, 14th International Symposium on Temporal Representation and Reasoning (TIME'07), 2007