Robust Model Checking of Timed Automata under Clock Drifts

Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan

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 ε and/or a positive δ such that the automaton satisfies the property even when the clocks are allowed to drift by ε and/or guards are enlarged by δ. In this paper we show that, 1. checking ω-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.

20th International Conference on Hybrid systems: computation and control (HSCC), 2017
Download: BIB PS PDF