Robust Model Checking of Timed Automata under Clock Drifts
Nima Roohi, Pavithra Prabhakar, Mahesh Viswanathan · 2017
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 stud- ied under robust semantics. A timed automaton H is said to robustly satisfy a property if there is a positive -- and/or a positive -- 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 re- move 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.