Timed automata are among the most widely studied models for real-time systems. Silent transitions, i.e., #epsilon#-transitions, have already been proposed in the original paper on timed automata by Alur and Dill [2]. In [7] it is shown that #epsilon#-transitions can be removed, if they do not reset clocks; moreover #epsilon#-transitions strictly increase the power of timed automata, if there is a self-loop containing #epsilon#-transitions which reset some clocks. The authors of [7] left open the problem about the power of the #epsilon#-transitions which reset clocks, if they do not lie on any cycle. The present paper settles this open question. Precisely, we prove that a timed automaton such that no #epsilon#-transition with nonempty reset set lies on any directed cycle can be effectively transformed into a timed automaton without #epsilon#-transitions. Interestingly, this main result holds under the assumption of non-Zenoness and it is false otherwise. precies time which allows to show that some timed languages are not recognizable by any #epsilon#-free timed automaton.
展开▼
