  We present abstraction-refinement algorithms for model checking safety
properties of timed automata. The abstraction domain we consider abstracts away
zones by restricting the set of clock constraints that can be used to define
them, while the refinement procedure computes the set of constraints that must
be taken into consideration in the abstraction so as to exclude a given
spurious counterexample. We implement this idea in two ways: an enumerative
algorithm where a lazy abstraction approach is adopted, meaning that possibly
different abstract domains are assigned to each exploration node; and a
symbolic algorithm where the abstract transition system is encoded with Boolean
formulas.
