Timed Automata with Urgent Transitions

In this paper we propose an extension to the formalism of timed automata by allowing urgent transitions. A urgent transition is a transition which must be taken within a fixed time interval from its enabling time. We give a set of rules formally describing the behaviour 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. However, from a specification point of view, the use of urgent transitions is crucial, especially in modular specification of systems.