In this paper we show how to translate bounded-length verification problems for timed automata into formulae in difference logic, a propositional logic enriched with timing constraints. We describe the principles of a satisfiability checker specialized
for this logic that we have implemented and report some preliminary experimental results.
This work was partially supported by the EC project IST-2001-35302 AMETIST (Advanced Methods for Timed Systems).