Checking Reachability Properties for Timed Automata via SAT
Checking Reachability Properties for Timed Automata via SAT
复制标题
通过 SAT 检查定时自动机的可达性属性
DOI：
--
复制
发表时间：
2002
影响因子：
0.8
通讯作者：
W. Penczek
中科院分区：
文献类型：
--
作者：
B. Wozna;A. Zbrzezny;W. Penczek
本文研究了时间自动机的可达性检验问题。其主要思想在于将著名的前向可达性算法和有界模型检测(BMC)方法相结合。为了检验满足某种期望性质的状态的可达性，首先将时间自动机的转移关系迭代展开到一定深度，并将其编码为命题公式。接下来，将期望的性质转换为命题公式，并检查上述两个公式的合取的可满足性。当已经找到满足该性质的状态或者已经搜索到时间自动机的所有状态时，可以终止转移关系的展开。实验结果有力地证明了该方法的有效性。
The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the desired property is translated to a propositional formula and the satisfiability of the conjunction of the two defined above formulas is checked. The unfolding of the transition relation can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results.