Timed Automata May Cause Some Troubles
Patricia Bouyer August 2002 |
Abstract:
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 does not support a natural implementation and, in practice,
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 details this widening operator and the forward analysis algorithm that uses it. 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, that uses such a widening operator, and which is correct. This goes really against what one could think. We then study in details 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 Available as PostScript, PDF, DVI. |