  A popular method for solving reachability in timed automata proceeds by
enumerating reachable sets of valuations represented as zones. A na\"ive
enumeration of zones does not terminate. Various termination mechanisms have
been studied over the years. Coming up with efficient termination mechanisms
has been remarkably more challenging when the automaton has diagonal
constraints in guards.
  In this paper, we propose a new termination mechanism for timed automata with
diagonal constraints based on a new simulation relation between zones.
Experiments with an implementation of this simulation show significant gains
over existing methods.
