Reachability Checking of Finite Precision Timed Automata

Abstract: 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. Key words: finite precision timed automata; symbolic method; model checking; reachability 摘 要: 为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度 时间自动机(finite precision timed automata,简 称 FPTA)作为实时系统的形式模 型,并提出了一种数据结