A calculus for timed automata

Abstract. A language for representing timed automata is introduced. Its semantics i defined in terms of timed automata. This language is complete in the sense that any timed automaton can be represented by a term in the language. We also define a direct operational semantics for the language in terms of (timed) transition systems. This is proven to be equivalent (or, more precisely, timed bisimilar) to the interpretation in terms of timed automata. In addition, a set of axioms is given that is shown to be sound for timed bisimulation. Finally, we introduce several features including the parallel composition and derived time operations like wait, time-out and urgency. We conclude with an example and show that we can eliminate non-reachable states using algebraic techniques. 1 In t roduct ion A real-time system is a system whose behaviour is constrained by requirements on the time in which events can occur. Sometimes, systems are implemented as timed systems in the sense that they fulfil certain timing conditions to give them an acceptable performance. Other systems depend on timing conditions in a more essential way, viz. because their functional correctness depends upon certain critical tinting conditions being fulfilled. Therefore, it becomes interesting to study the formal verification of such systems. In the last years, several formal techniques have been developed to specify and verify real-time systems. For instance, many well-known process algebras hav