Robust Model Checking of Timed Automata under Clock Drifts

Timed automata have an idealized semantics where clocks are assumed to be perfectly continuous and synchronized, and guards have infinite precision. These assumptions cannot be realized physically. In order to ensure that correct timed automata designs can be implemented on real-time platforms, several authors have suggested that timed automata be studied under robust semantics. A timed automaton H is said to robustly satisfy a property if there is a positive epsilon and/or a positive delta such that the automaton satisfies the property even when the clocks are allowed to drift by epsilon and/or guards are enlarged by delta. In this paper we show that, 1. checking omega-regular properties when only clocks are perturbed or when both clocks and guards are perturbed, is PSPACE-complete; and 2. one can compute the exact reachable set of a bounded timed automaton when clocks are drifted by infinitesimally small amount, using polynomial space. In particular, we remove the restrictive assumption on the timed automaton that its region graph only contains progress cycles, under which the second result above has been previously established.