A Proof System for Timed Automata

A proof system for timed automata is presented, based on a CCS-style language for describing timed automata. It consists of the standard monoid laws for bisimulation and a set of inference rules. The judgements of the proof system are conditional equations of the form phirhd t=u where phi is a clock constraint and t, u are terms denoting timed automata. It is proved that the proof system is complete over the recursion-free subset of the language. The completeness proof relies on the notion of symbolic timed bisimulation. Two variations of the axiomatisation are also discussed, one on timed automata by associating an invariant constraint to each node and the other on bisimulation by abstracting away delay transitions.Note: To be included in the proceedings of FOSSACS'0