  The reachability problem for timed automata asks if there exists a path from
an initial state to a 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 in current algorithms
extrapolation of a zone is always a zone and in particular it is convex.
  In this paper, we propose to solve the reachability problem without such
extrapolation operators. To ensure termination, we provide an efficient
algorithm to check if a zone is included in the so called 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.
  An additional benefit of the proposed approach is that it 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.
