A Symbolic Decision Procedure for Robust Safety of Timed Systems

We present a symbolic algorithm for deciding safety (reachability) of timed systems modelled as Timed Automata (TA), under the notion of robustness w.r.t. infinitesimal clock-drift. The algorithm uses a “neighbourhood” operator on zones that is efficient to compute. In contrast to other approaches for robustly deciding reachability of TA, which are either region based [1], [2], or involve a combination of forward and backward analyses when zone-based [3], ours is a zone-based fully forward algorithm that requires no special treatment of cycles in TA, and can be applied to target states that need not be closed.

• Type: Conference
• Year: 2007
• Where: TIME
• Authors: Mani Swaminathan, Martin Fränzle
• Keywords: Logical Reasoning, Robustness W.r.t, Symbolic Algorithm, TIME 2007, Timed Systems