Characterization of the Expressive Power of Silent Transitions in Timed Automata

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].