Affiliations: LSV, CNRS URA 2236, ENS de Cachan, 61 av. du Prés. Wilson, F-94235 Cachan Cedex, France, email: berard,petit@lsv.ens-cachan.fr | Inst. für Informatik, Universität Stuttgart, Breitwiesenstr. 20-22, D-70565 Stuttgart, Germany, email: diekert@informatik.uni-stuttgart.de | LIAFA, Université Paris 7, 2, place Jussieu, F-75251 Paris Cedex 05, France, email: gastin@liafa.jussieu.fr
Note: [] Address for correspondence: LSV, CNRS URA 2236, ENS de Cachan, 61 av. du Prés. Wilson, F-94235 Cachan Cedex, France.
Note: [] Address for correspondence: Inst. für Informatik, Universität Stuttgart, Breitwiesenstr. 20-22, D-70565 Stuttgart, Germany.
Note: [] Address for correspondence: LIAFA, Université Paris 7, 2, place Jussieu, F-75251 Paris Cedex 05, France.
Abstract: Timed automata are among the most widely studied models for real-time systems. Silent transitions, i.e., ϵ-transitions, have already been proposed in the original paper on timed automata by Alur and Dill [3]. We show that the class TLϵ of timed languages recognized by automata with ϵ-transitions, is more robust and more expressive than the corresponding class TL without ϵ-transitions. We then focus on ϵ-transitions without reset, i.e. ϵ-transitions which do not reset clocks. We propose an algorithm to construct, given a timed automaton, an equivalent one without such transitions. This algorithm is in two steps, it first suppresses the cycles of ϵ-transitions without reset and then the remaining ones. Then, we prove that a timed automaton such that no ϵ-transition which resets clocks lies on any directed cycle, can be effectively transformed into a timed automaton without ϵtransitions. Interestingly, this main result holds under the assumption of non-Zenoness and it is false otherwise. To complete the picture, we exhibit a simple timed automaton with an ϵ-transition, which resets some clock, on a cycle and which is not equivalent to any ϵ-free timed automaton. To show this, we develop a promising new technique based on the notion of precise action. This paper presents a synthesis of the two conference communications [9] and [13].
