Forward Analysis of Updatable Timed Automata

Timed automata are a widely studied model. Its decidability has been proved using the so-called region automaton construction. This construction provides a correct abstraction for the behaviours of timed automata, but it suffers from a state explosion and is thus not used in practice. Instead, algorithms based on the notion of zones are implemented using adapted data structures like DBMs. When we focus on forward analysis algorithms, the exact computation of all the successors of the initial configurations does not always terminate. Thus, some abstractions are often used to ensure termination, among which, a widening operator on zones.In this paper, we study in detail this widening operator and the corresponding forward analysis algorithm. This algorithm is most used and implemented in tools like KRONOS and UPPAAL. One of our main results is that it is hopeless to find a forward analysis algorithm for general timed automata, that uses such a widening operator, and which is correct. This goes really against what one could think. We then study in detail this algorithm in the more general framework of updatable timed automata, a model which has been introduced as a natural syntactic extension of classical timed automata. We describe subclasses of this model for which a correct widening operator can be found.