Deriving Unbounded Reachability Proof of Linear Hybrid Automata during Bounded Checking Procedure
Deriving Unbounded Reachability Proof of Linear Hybrid Automata during Bounded Checking Procedure
复制标题
在有界检查过程中推导线性混合自动机的无界可达性证明
DOI：
10.1109/tc.2016.2604308
复制
发表时间：
2017-03-01
影响因子：
3.7
通讯作者：
Li, Xuandong
中科院分区：
文献类型：
--
作者：
Xie, Dingbao;Xiong, Wen;Li, Xuandong
线性混合自动机（LHA）的可及性分析是一个重要问题。经典模型检查（CMC）技术是不可扩展的，不能保证终止。另一方面，有限的模型检查（BMC）的执行更具成本效益，但不能保证安全的安全性。在本文中，我们试图弥合BMC和CMC之间的差距，以进行LHA的可及性分析。在LHA的BMC期间，典型的过程可以发现一组不满意的约束核心，可以将其映射到LHA图结构中的路径段。如果连接初始位置和目标位置的每条路径都必须经过如此不可行的路径段，则目标位置完全无法达到。基于此特征，我们提出了一种基于LTL模型检查的方法，以检查目标位置是否被阻止。为了进一步优化性能，我们提出了一种基于自动机的解决方案，以逐步检查LTL规范，并采用直接算法以检查接受条件，以避免对产品自动机的显式结构。
Reachability analysis of linear hybrid automata (LHA) is an important problem. Classical model checking (CMC) technique is not scalable and not guaranteed to terminate. On the other hand, bounded model checking (BMC) is more cost-effective to conduct but can not guarantee the safety beyond the bound. In this paper, we seek to bridge the gap between BMC and CMC for reachability analysis of LHA. During BMC of LHA, typical procedures can discover sets of unsatisfiable constraint cores, which can be mapped back to path segments in the graph structure of LHA. If every path connecting the initial and target location has to go through such infeasible path segment, the target location is entirely not reachable. Based on this characteristic, we propose a LTL model checking based approach to check whether the target location is blocked. To further optimize the performance, we propose an automata based solution to check the LTL specification incrementally and adopt an on-the-fly algorithm to check the accepting condition to avoid an explicit construction of product automata.