A Symbolic Decision Procedure for Robust Safety of Timed Systems

Timed automata (TA) (Alur and Dill, 1994) 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 (Bengtsson and Yi, 2004), which implement a zone-based forward reachability analysis (FRA) algorithm. We present here a symbolic (zone-based) FRA algorithm for deciding safety (reachability) of TA, which is robust w.r.t clock-drift, and which involves minimal overhead w.r.t the standard FRA algorithm of UPPAAL and is guaranteed to terminate in a number of iterations comparable to the standard case.