Résumé | We consider the classic reachability problem for timed automata:
given an automaton, decide if there exists a path from its initial state
to a given target state. The standard solution to this problem involves
computing the *zone graph* of the automaton, which in principle could be
infinite. In order to make the graph finite, zones are approximated using
an extrapolation operator. For reasons of efficiency it is required that an
extrapolation of a zone is always a zone; and in particular that it is *convex*.
We propose a new solution to the reachability problem that uses no
such extrapolation operators. To ensure termination, we provide an
efficient algorithm to check if a zone is included in the
*region closure* of another. Although theoretically better,
closure cannot be used in the standard algorithm since a closure of
a zone may not be convex.
The structure of this new algorithm permits to calculate
approximating parameters on-the-fly during exploration of the zone
graph, as opposed to the current methods which do it by a static
analysis of the automaton prior to the exploration. This allows for
further improvements in the algorithm. Promising experimental results
are presented.
Joint work with Frédéric Herbreteau, Dileep Kini, Igor Walukiewicz
|