\title{Timed Automata with Urgent Transitions\thanks{A first version of this
paper appeared in \cite{BT01}}}

\author{Roberto Barbuti \and Luca Tesei}

\begin{abstract} 
In this paper we propose an extension to the formalism of timed
automata by allowing urgent transitions. An urgent transition is a
transition which must be taken within a fixed time interval from its
enabling time and it has higher priority than other non-urgent
transitions enabled in the same state.  We give a set of rules
formally describing the behavior of urgent transitions and we show
that, from a language theoretic point of view, the addition of urgency
does not improve the expressive power of timed automata.  From a
specification point of view, the use of urgent transitions allows
shorter and clear specifications of behaviors involving urgency and
priority.  We use timed automata with urgent transitions for
specifying a multicast protocol for mobile computing.  \\ \ \\
\noindent {\bf Keywords:} real-time systems, timed automata, modular
specification, parallel composition.  
\end{abstract}