D | |
---|---|

[DDM+04] | Martin De Wulf,
Laurent Doyen,
Nicolas Markey, and
Jean-François Raskin.
Robustness and Implementability of Timed Automata.
In FORMATS-FTRTFT'04,
Lecture Notes in Computer Science 3253, pages 118-133. Springer-Verlag, September 2004.
- Abstract
In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by Δ to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter Δ for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a Δ. We show that this question is closely related to a notion of robustness for timed automata defined in (A. Puri: *Dynamical Properties of Timed Automata*. FTRTFT, 1998) and prove that the implementability problem is decidable.
@inproceedings{ftrtft2004-DDMR, author = {De{~}Wulf, Martin and Doyen, Laurent and Markey, Nicolas and Raskin, Jean-Fran{\c c}ois}, title = {Robustness and Implementability of Timed Automata}, editor = {Lakhnech, Yassine and Yovine, Sergio}, booktitle = {{P}roceedings of the {J}oint {I}nternational {C}onferences on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal {T}echniques in {R}eal-Time and {F}ault-Tolerant {S}ystems ({FTRTFT}'04)}, acronym = {{FORMATS-FTRTFT}'04}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3253}, pages = {118-133}, year = {2004}, month = sep, doi = {10.1007/978-3-540-30206-3_10}, abstract = {In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by \(\Delta\) to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter \(\Delta\) for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a \(\Delta\). We show that this question is closely related to a notion of robustness for timed automata defined in (A.~Puri: \textit{Dynamical Properties of Timed Automata}. FTRTFT, 1998) and prove that the implementability problem is decidable.}, } |

- 1
- 1
- 1
- 1