Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking  

作　　者：赵建华 李宣东 郑滔 郑国梁 

机构地区：[1]State Key Laboratory of Novel Software Technology, Nanjing University, Nanjing 210093, P.R. China [2]Department of Computer Science and Technology, Nanjing University, Nanjing 210093, P.R. China

出　　处：《Journal of Computer Science & Technology》2006年第1期41-51,共11页计算机科学技术学报（英文版）

基　　金：Supported by the National Natural Science Foundation of China （Grant Nos. 60203009, 60233020 and 60425204）, the NSF of Jiangsu Province （Grant No. BK2003408） and the National Basic Research 973 Program of China （Grant No. 2002CB312001）.

摘　　要：Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and spaceefficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficlency of reachability analysis.Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and spaceefficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficlency of reachability analysis.

关 键 词：formal method model checking timed automaton 

分 类 号：TP2[自动化与计算机技术—检测技术与自动化装置]