Verifying Linear Duration Constraints of Timed Automata

 This report aims at developing a technique for verifying if a timed automaton satisfies a linear duration constraint on the automaton states. The constraints are represented in the form of linear duration invariants - a simple class of Chop-free Duration Calculus (DC) formulas. We prove that linear duration invariants of a timed automaton are discretisable, and reduce checking if a timed automaton satisfies a linear duration invariant to checking if the integer timed region graph of the original automaton satisfies the same linear duration invariant. The latter can be done with exhausted search on graphs. In comparison to the techniques in the literatures, our one is more powerful; it works for the standard semantics of DC and general form of timed automata while the others cannot be applied.