A Class of Automata for Computing
Reachability Relations in Timed Systems
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 the NATO Advanced Research Workshop on Verification of Infinite State System (VISSAS'05), Timisoara, March 17-22, Romania, 2005.