Checking Temporal Duration Properties of Timed Automata

In this paper, the problem of checking a timed automaton for a DurationCalculus formula of the form Temporal Duration Property is addressed. Itis shown that Temporal Duration Properties are in the class of discretisablereal-time properties of Timed Automata, and an algorithm is given to solvethe problem based on linear programming techniques and the depth-firstsearch method in the integral region graph of the automaton. Thecomplexity of the algorithm is in the same class as that of the solutionof the reachability problem of timed automata.