基于Craig插值的线性混成系统符号化模型检测  

Symbolic Model Checking for Linear Hybrid Systems Base on Craig Interpolation

作　　者：陈祖希[1] 徐中伟[1] 霍伟伟[2] 喻钢[2] 

机构地区：[1]同济大学电子与信息工程学院,上海201804 [2]上海大学悉尼工商学院,上海201800

出　　处：《电子学报》2014年第7期1338-1346,共9页Acta Electronica Sinica

基　　金：国家自然科学基金(No.60674004;No.61075002;No.71302048);十二五国家科技支撑计划(No.2011BAG01B03);国家863高技术研究发展计划(No.2012AA112801);铁道部重点研究发展计划(No.2012AA112801)

摘　　要：最强后件的计算是模型检测算法的核心.本文使用一阶逻辑可满足性模线性算术理论给出线性混成自动机的有界模型检测表示公式,利用一阶逻辑公式不可满足情况下的插值存在性定理,对线性混成自动机的有界模型检测公式进行指定的划分,使用支持线性算术插值计算的可满足性模理论后端证明引擎的线性时间复杂度的消解反证技术获得这两部分公式间的插值公式,按一阶逻辑Craig插值的性质,所得到的插值公式就是模型检测过程中最强后件公式的上近似表示.有效地避免了使用逻辑编码方案实现线性混成自动机模型检测过程中需要双指数时间复杂度的量词消去操作求取最强后件公式,也不需像有界模型检测按步长展开变迁公式进行可满足性判定.最后本文在此最强后件计算的基础上,以有界模型检测技术作为反例确认方法,实现了一种无假反例的混成系统近似可达集计算算法.实验证明该算法与目前已经得到广泛工业应用的有界模型检测算法相比具有更优的性能.The key to model checking algorithm is the computation of strongest post condition. This article encodes the bounded model checking problem for linear hybrid automata as formula of SAT Modulo theories for linear arithmetic. We divided the formula into two specific parts to obtain the interpolation with a linear time complexity. According to the properties of Craig in- terpolation theorem for first order logic, the interpolation as an over-approximation strongest post condition and can replace the origi- nal strongest post condition used in symbolic model checking for hybrid automata with exponential time complexity. This method does not require to the Iransition relation is fully expanded the same as bounded model checking to check satisfiability, also. We im- plement the hybrid systems model checking algorithm without false counter-example using the over-approximation strongest post condition operator together with bounded model checking algorithm. Experiments show that our approach can be more efficient than bounded model checking for hybrid systems.

关 键 词：Craig插值 可满足性模理论 线性混成自动机 符号模型检验 混成系统 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]