Lazy abstractions for timed automata