Abstract of Paper

Expressiveness of Updatable Timed Automata
by Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, Antoine Petit

Abstract:

Since their introduction by Alur and Dill [AD90, AD94], timed automata are
one of the most widely studied model for real-time systems. The syntactic
extension of so-called updatable timed automata allows much more powerful
updates of clocks than the reset operation proposed in the original model.
This new model, for which decidability of emptiness has been characterized
in [BDFP00a], has been used successfully to modelize in a concise way, and
then verify, suitable classes of real-time systems like the ATM protocol ABR   
[BF99]. But the expressive power of updatable timed automata was an open
(mainly theoretical) question.  In this paper we solve completely this
problem by proving that any language accepted by an updatable timed
automaton (from a decidable class) is also accepted by a ``classical''
timed automaton with $\varepsilon$-transitions. We propose even more precise
results by showing that
\begin{itemize}
\item Any updatable timed automaton using only deterministic updates is
strongly bisimilar to a classical timed automaton
\item Anupdatable timed automaton using arbitrary updates is weakly
bisimilar (but not strongly bisimilar) to a classical timed automaton with
$\varepsilon$-transitions.
\end{itemize}