On checking timed automata for linear duration invariants

In this work, 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 expressions for timed languages. Then, we extend the linear programming-based approaches in [10] to this algebraic notation for the timed automata. Our results in this paper are more general than the ones presented in [IO]. Namely, Timed Automata are our starting point, and we can provide an accurate answer to the problem for a larger class of them.