Timed automata [1] are finite automata extended with clocks that can be tested and reset on the transitions of the automaton. The clocks allow to constrain the delays between actions of the automaton. Timed automata have been successfully used to model and verify real-time systems. The tool UPPAAL [9] is used by critical software designers and numerous case studies have been reported [10].
The state-space of a timed automaton is uncountable. Verification algorithms thus use an abstract representation of the state-space. Coarser abstractions yield smaller representations, hence more efficient verification algorithms. Several abstractions have been introduced [2,3] in an effort to define the coarsest abstraction possible. The idea is to abstract a zone Z by adding clock valuations that are simulated by a valuation in Z. Such an abstraction is obviously sound for reachability. The main difficulty is to find a simulation relation that yields a finite and small number of abstracted zones to guarantee termination and efficiency of verification algorithms.
A first approach consists in finding the coarsest simulation relation for a given timed automaton to verify. However, this problem is EXPTIME-complete whereas reachability is "only" PSPACE-complete. The standard solution is thus to use only a part of the information available in the automaton. Abstractions in [3] consider the constants that appear in the guards of the automaton. It has recently been shown that aLU is the coarsest abstraction that is sound for all timed automata that use constants bounded by L and U [5]. There are two ways to get better abstractions. The first one is to optimize the bounds L and U [4,6].
Another approach is to extract more precise information from the
automaton than the constants L and U. The natural step beyond considering
constants in the guards is to consider the guards themselves. We don't
want to collect all the guards from the automaton but only those that are
relevant to solve the reachability problem. Counterexample-guided
abstraction and refinement [7] is a family of techniques that have been
introduced to that purpose. In particular, McMillan has proposed an
algorithm based on interpolation that is very efficient in selecting
relevant guards [8]. We propose to adapt this algorithm to the context of
timed automata. To that purpose, we first need to define interpolation of
zones. Then, interpolants need to be propagated over paths in the
automaton to refine the abstract representation of the state-space.
Finally, we need to define an asbtraction based on these interpolants that
is sound and complete for reachability.