17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
Computing Reachability Relations in Timed Automata
Copenhagen, Denmark
July 22-July 25
ISBN: 0-7695-1483-9
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, composition and star of the class of 2n-automata that represent reachability relations in timed automata.