基于 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 transition 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 插值的性质，所得到的插值公式就是模型检测过程中最强后件公式的上近似表示。有效地避免了使用逻辑编码方案实现线性混成自动机模型检测过程中需要双指数时间复杂度的量词消去操作求取最强后件公式，也不需像有界模型检测按步长展开变迁公式进行可满足性判定。最后本文在此最强后件计算的基础上，以有界模型检测技术作为反例确认方法，实现了一种无假反例的混成系统近似可达集计算算法。实验证明该算法与目前已经得到广泛工业应用的有界模型检测算法相比具有更优的性能。