Perturbed timed automata. (English) Zbl 1078.68070

Alur, Rajeev; La Torre, Salvatore; Madhusudan, P.

Morari, Manfred (ed.) et al., Hybrid systems: Computation and control. 8th international workshop, HSCC 2005, Zurich, Switzerland, March 9–11, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25108-1/pbk). Lecture Notes in Computer Science 3414, 70-85 (2005).

Summary: We consider timed automata whose clocks are imperfect. For a given perturbation error \(0<\varepsilon<1\) the perturbed language of a timed automaton is obtained by letting its clocks change at a rate within the interval \([1-\varepsilon, 1+\varepsilon]\). We show that the perturbed language of a timed automaton with a single clock can be captured by a deterministic timed automaton. This leads to a decision procedure for the language inclusion problem for systems modeled as products of 1-clock automata with imperfect clocks. We also prove that determinization and decidability of language inclusion are not possible for multi-clock automata, even with perturbation.
For the entire collection see [Zbl 1069.68011].

MSC:

68Q45

Formal languages and automata