Nicolas Markey

Résumé

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.},
}