A Complete Axiomatisation for Timed Automata

Huimin Lin, Wang Yi

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


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.

Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Maintainer fsttcs20@cse.iitd.ernet.in.
Start Conference Manager
Conference Systems