Characterization of the expressive power of silent transitions in timed automata

• Autorzy: Berard, B. , Petit, A. , Diekert, V. , Gastin, P.
• Języki publikacji: EN

Abstrakty

EN

Timed automata are among the most widely studied models for real-time systems. Silent transitions, i.e., e-transitions, have already been proposed in the original paper on timed automata by Alur and Dill. We show that class TLe of timed languages recognized by automata with e-transitions, is more robust and more expressive than the corresponding class TL without e-transitions. We then focus on e-transitions without reset, i.e. 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 e-transitions without reset and then the remaining ones. Then, we prove that a timed automaton such that no e-transition which resets clocks lies on any directed cycle, can be effectively transformed into a timed automaton without e-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 e-transition, which resets some clock, on a cycle and which is not equivalent to any e-free timed automaton. To show this, we develop a promising new technique based on the notion of precise action.

• Czasopismo: Fundamenta Informaticae
• Rocznik: 1998
• Tom: Vol. 36, nr 2,3
• Strony: 145-182
• Opis fizyczny: tab., wykr., bibliogr. 28 poz.

Twórcy

autor

Berard, B.

autor

Petit, A.

autor

Diekert, V.

autor

Gastin, P.

• LSV, CNRS URA 2236, ENS de Cachan, 61 av. du Pres. Wilson, F-94235 Cachan Cedex, France,