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.