Checking Temporal Duration Properties of Timed Automata

作     者：李勇 Dang Van Hung 

作者机构：State Key Laboratory of Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing 210093 P.R. China International Institute for Software Technology The United Nations University P.O. Box 3058 Macao SAR P.R. China 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：2002年第17卷第6期

页      面：689-698页

核心收录：

学科分类：0808[工学-电气工程] 08[工学] 0835[工学-软件工程] 0701[理学-数学] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：国家自然科学基金 国家高技术研究发展计划(863计划) 

主　　题：model checking duration calculus timed automata 

摘      要：In this paper, the problem of checking a timed automaton for a Duration Cal-culus formula of the form Temporal Duration Property is addressed. It is shown that TemporalDuration Properties are in the class of discretisable real-time properties of Timed Automata,and an algorithm is given to solve the problem based on linear programming techniques andthe depth-first search method in the integral region graph of the automaton. The complexityof the algorithm is in the same class as that of the solution of the reachability problem of timedautomata.