Abstract :
In this paper we present a complete proof system for timed automata.
It extends our previous axiomatisation of timed bisimulation for the
class of loop-free timed automata with {\em unique fixpoint
induction}. To our knowledge, this is the first algebraic theory for
the whole class of timed automata with a completeness result, thus
fills a gape in the theory of timed automata. It demonstrates that
timed automata is as mathematically tractable as standard process
algebras. The proof of the completeness result relies on the notion
of {\em symbolic timed bisimulation}, adapted from the work on
value--passing processes.
