Robustness and Implementability of Timed Automata

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 [Pur98] and prove that the implementability problem is decidable.

• Type: Conference
• Year: 2004
• Where: FORMATS
• Authors: Martin De Wulf, Laurent Doyen, Nicolas Markey, Jean-François Raskin
• Keywords: ASAP Semantics, FORMATS 2004, Reaction Delay, Timed Automata