TY - GEN
T1 - Robust model checking of timed automata under clock drifts
AU - Roohi, Nima
AU - Prabhakar, Pavithra
AU - Viswanathan, Mahesh
N1 - Publisher Copyright:
© 2017 Copyright held by the owner/author(s). Publication rights licensed to ACM.
Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.
PY - 2017/4/13
Y1 - 2017/4/13
N2 - 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 T-L is said to robustly satisfy a property if there is a positive e and/or a positive 5 such that the automaton satisfies the property even when the clocks are allowed to drift by e and/or guards are enlarged by 5. 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 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.
AB - 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 T-L is said to robustly satisfy a property if there is a positive e and/or a positive 5 such that the automaton satisfies the property even when the clocks are allowed to drift by e and/or guards are enlarged by 5. 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 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.
UR - http://www.scopus.com/inward/record.url?scp=85019032826&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85019032826&partnerID=8YFLogxK
U2 - 10.1145/3049797.3049821
DO - 10.1145/3049797.3049821
M3 - Conference contribution
AN - SCOPUS:85019032826
T3 - HSCC 2017 - Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (part of CPS Week)
SP - 153
EP - 162
BT - HSCC 2017 - Proceedings of the 20th International Conference on Hybrid Systems
PB - Association for Computing Machinery
T2 - 20th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2017
Y2 - 18 April 2017 through 20 April 2017
ER -