Several problems in the domain of verification of real-time systems
translate to checking whether a set of states is reachable in a timed
automaton.
The possibility to reach, starting from a state q, another state r
in a timed automata depends essentially on the clock values with which
one starts from state q.
Moreover, even if r is reachable by starting from q with the clock
values denoted by the vector v, the set of clock values when reaching
r is in general an uncountable set.
The dependence between clock values when starting from q and clock
values when reaching r, call it the reachability relation defined
by q and r, is an important characteristics for the timed automaton,
and its algorithmic computation would be another way of attacking
verification problems in timed automata.
This algorithmic computation is the subject of this paper.
Our approach is to build the reachability relations by computing
unions, compositions and reflexive-transitive closures of such
relations.
The main feature that allows us to take this approach is a
representation of relations by means of finite automata:
we introduce 2n-automata as a new representation of the relations
that are associated to each transition in a timed automaton.
The idea is that each tuple in the relation is coded by a run
in the 2n-automaton.
We then show that these automata are closed under union, concatenation
and (for mild conditions) star and have a decidable emptiness problem.
We also show that the mild conditions are necessary since in general
star closure is not possible, and that the 2n-automata arising
from the relational semantics of timed automata bear these mild
conditions.
