On checking timed automata for linear duration invariants

被引：5

作者：

Braberman, VA ^{[1
]}

Van Hung, D ^{[1
]}

机构：

[1] UBA, FCEYN, Buenos Aires, DF, Argentina

来源：

19TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS | 1998年

关键词：

D O I：

10.1109/REAL.1998.739752

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：264 / 273

页数：10