Checking timed automata for linear duration properties

被引：4

作者：

Zhao, JH ^{[1
]}

Van Hung, D

机构：

[1] Nanjing Univ, Dept Comp Sci & Technol, State Key Lab Novel Software Technol, Nanjing 210093, Peoples R China

[2] UN Univ, Int Inst Software Technol, Macau, Peoples R China

来源：

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY | 2000年 / 15卷 / 05期

基金：

中国国家自然科学基金;

关键词：

model checking; duration calculus; real-time system;

D O I：

10.1007/BF02950405

中图分类号：

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

学科分类号：

0812 ;

摘要：

It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M. An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes. Based on this, a method is proposed for checking whether M satisfies D. In some cases, the number of equivalence classes is too large for a computer to manipulate. A technique for reducing the search-space for checking linear duration property is also described. This technique is more suitable for the case in this paper than those in the literature because most of those techniques are designed for reachability analysis.

引用

页码：423 / 429

页数：7