Computing Reachability Relations in Timed Automata

We give an algorithmic calculus of the reachability relations on clock values defined by timed automata. Our approach is a modular one, by  computing unions, compositions and reflexive-transitive closure (star) of "atomic'' relations. The essential tool is a new representation technique for n-clock relations -- the 2n-automata -- and our strategy is to show the closure under union, concatenation and star of the class of 2n-automata that represent reachability relations in timed automata.

Proceedings of 17th IEEE Symposium on Logics in Computer Science (LICS 2002)”, IEEE Computer Society Press, Copenhagen, Denmark, pages 177-186, 2002.

 gzipped postscript file.