%0 Journal Article
%T Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking
%A Jian-Hua Zhao
%A Xuan-Dong Li
%A Tao Zheng
%A Guo-Liang Zheng
%A <br>Jian-Hua Zhao
%A Xuan-Dong Li
%A Tao Zheng
%A and Guo-Liang Zheng
%J 计算机科学技术学报
%D 2006
%I 
%X 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.
%K formal method
%K model checking
%K timed automaton<br>模拟检测
%K 同步自动机械
%K 可达性
%K 时钟变量
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=F57FEF5FAEE544283F43708D560ABF1B&aid=14CE6F403EA481F53AE16E2EFEFFB400&yid=37904DC365DD7266&vid=659D3B06EBF534A7&iid=CA4FD0336C81A37A&sid=2001E0D53B7B80EC&eid=987EDA49D8A7A635&journal_id=1000-9000&journal_name=计算机科学技术学报&referenced_num=0&reference_num=12