Sciweavers

TIME
2007
IEEE

A Symbolic Decision Procedure for Robust Safety of Timed Systems

13 years 10 months ago
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.
Mani Swaminathan, Martin Fränzle
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where TIME
Authors Mani Swaminathan, Martin Fränzle
Comments (0)