On Checking Timed Automata For Linear Duration Invariants

VICTOR A. BRABERMAN; DANG VNA HUNG

Madrid, Espania

Conferencia; RTSS -IEEE International Real-time Systems Symposium; 1998

IEEE

In this work, we address the problem of verifying a Timed Automaton for Duration Calculus formula in the form of Linear Duration Invariants. Accurate methods seem not practical even for small examples. We present a conservative method for solving the problem that is based on linear programming techniques applied on an algebraic representation of Timed Automata. We also provide a translation procedure from Timed Automata to this sort of regular expressions for real-time languages. Some previous linear programming-based approaches work for algebraic notations which are less expresive than Timed Automata. In comparison to these approaches, our method is more general: Timed Automata are our starting point and we provide an accurate answer to the problem for a larger (and representative) class of them