%0 Journal Article
%T Reachability Checking of Finite Precision Timed Automata<br>有限精度时间自动机的可达性检测
%A YAN Rong-Jie
%A LI Guang-Yuan
%A XU Yu-Bo
%A LIU Chun-Ming
%A TANG Zhi-Song
%A <br>晏荣杰
%A 李广元
%A 徐雨波
%A 刘春明
%A 唐稚松
%J 软件学报
%D 2006
%I 
%X To relieve the state space explosion problem, and accelerate the speed of model checking, this paper introduces the concept of finite precision timed automata (FPTAs) and proposes a data structure to represent its symbolic states. FPTAs only record the integer values of clock variables together with the order of their most recent resets to reduce the state space. The constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding FPTA are provided, and then an algorithm for reachability analysis is presented. Finally, the paper presents some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure.
%K finite precision timed automata
%K symbolic method
%K model checking
%K reachability<br>有限精度时间自动机
%K 符号化方法
%K 模型检测
%K 可达性
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=C1C0945E7CF265FD&yid=37904DC365DD7266&vid=BCA2697F357F2001&iid=CA4FD0336C81A37A&sid=CA4FD0336C81A37A&eid=F3090AE9B60B7ED1&journal_id=1000-9825&journal_name=软件学报&referenced_num=4&reference_num=27