On checking timed automata for linear duration invariants

Abstract

We address the problem of verifying a timed automaton for a real time property written in duration calculus in the form of linear duration invariants. We present a conservative method for solving the problem using the linear programming techniques. First, we provide a procedure to translate timed automata into a sort of regular expression for timed languages. Then, we extend the linear programming based approaches by L.X. Dong and D.V. Hung (1996) to this algebraic notation for the timed automata. Our results are more general than the ones presented by Dong and Hung, i.e., timed automata are our starting point, and we can provide an accurate answer to the problem for a larger class of them.