Better abstractions for timed automata

One such abstraction is the a≼LU abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets, it has not been used in implementations. Firstly, we prove that a≼LU abstraction is the coarsest abstraction with respect to LU-bounds that is sound and complete for reachability. Secondly, we provide an efficient technique to use the a≼LU abstraction to solve the reachability problem.