| Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking |
| |
| 作者姓名： | Jian-Hua Zhao Xuan-Dong Li Tao Zheng and Guo-Liang Zheng |
| |
| 作者单位： | [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 |
| |
| 基金项目： | 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 space-efficiency. 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-efficiency of reachability analysis.
|
| 关 键 词： | 模拟检测 同步自动机械 可达性 时钟变量 |
| 收稿时间： | 2004-08-30 |
| 修稿时间： | 2004-08-302005-08-09 |
Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking |
| |
| Jian-Hua Zhao,Xuan-Dong Li,Tao Zheng,and Guo-Liang Zheng.Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking[J].Journal of Computer Science and Technology,2006,21(1):41-51. |
| |
| Authors: | Jian-Hua Zhao Xuan-Dong Li Tao Zheng Guo-Liang Zheng |
| |
| Affiliation: | (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 |
| |
| Abstract: | 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. |
| |
| Keywords: | formal method model checking timed automaton |
| 本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
