Using non-convex approximations for efficient analysis of timed automata

FréDéRic Herbreteau, Dileep Kini, B. Srivathsan & Igor Walukiewicz
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....