Linear duration invariants (LDI) are important safety properties of
real-time systems. They can be easily formulated in terms of a class
of chop-free formulas in the Duration Calculus (DC). Compared to other
temporal logics, the specification in DC is simpler, neater and more
importantly easier to understand. However, directly model checking
them  is more difficult than model checking properties formulated in
 the computation tree logic
(CTL). In this paper, we present a technique for the verification of
the satisfaction of an LDI  D by a timed automaton A  by model
checking a CTL property. For this, we construct an untimed   automaton G
 from  A, and prove that A satisfies
D iff  D is is satisfied by the set of all  paths of G. We then construct a CTL 
formula  and simply check if G satisfies this formula. By this, we
convert the problem of verification of the LDI to the problem of model
checking CTL formula. As a result,  the CTL model checking techniques
and tools, such as UPPAAL, can be used for verification of LDI
specified in the DC.

This paper is accepted for presentation and publication in the 
proceedings ICTAC 2008 in LNCS. The research supported by the project 
of National Natural Science Foundation of China (No.60603037) and HTTS
project funded by Macau Science and Technology
Development Fund.