D | |
---|---|

[DDM+08] | Martin De Wulf,
Laurent Doyen,
Nicolas Markey, and
Jean-François Raskin.
Robust Safety of Timed Automata.
Formal Methods in System Design 33(1-3):45-84. Springer-Verlag, December 2008.
- Abstract
Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened by Δ>0 and clocks can drift by ε>0. The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks. We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parameters Δ and ε such that the timed automaton never enters the bad states under the relaxed semantics.
@article{fmsd33(1-3)-DDMR, author = {De{~}Wulf, Martin and Doyen, Laurent and Markey, Nicolas and Raskin, Jean-Fran{\c c}ois}, title = {Robust Safety of Timed Automata}, publisher = {Springer-Verlag}, journal = {Formal Methods in System Design}, volume = {33}, number = {1-3}, pages = {45-84}, year = {2008}, month = dec, doi = {10.1007/s10703-008-0056-7}, abstract = {Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened by~\(\Delta>0\) and clocks can drift by~\(\epsilon>0\). The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks.\par We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parameters~\(\Delta\) and~\(\epsilon\) such that the timed automaton never enters the bad states under the relaxed semantics.}, } |

- 1
- 1
- 1
- 1