학술논문
On checking timed automata for linear duration invariants
Document Type
Conference
Author
Source
Proceedings 19th IEEE Real-Time Systems Symposium (Cat. No.98CB36279) Real-time systems 98 Real-Time Systems Symposium, 1998. Proceedings. The 19th IEEE. :264-273 1998
Subject
Language
ISSN
1052-8725
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.