CAJ | 학술논문

最强后件的计算是模型检测算法的核心。本文使用一阶逻辑可满足性模线性算术理论给出线性混成自动机的有界模型检测表示公式，利用一阶逻辑公式不可满足情况下的插值存在性定理，对线性混成自动机的有界模型检测公式进行指定的划分，使用支持线性算术插值计算的可满足性模理论后端证明引擎的线性时间复杂度的消解反证技术获得这两部分公式间的插值公式，按一阶逻辑 Craig 插值的性质，所得到的插值公式就是模型检测过程中最强后件公式的上近似表示。有效地避免了使用逻辑编码方案实现线性混成自动机模型检测过程中需要双指数时间复杂度的量词消去操作求取最强后件公式，也不需像有界模型检测按步长展开变迁公式进行可满足性判定。最后本文在此最强后件计算的基础上，以有界模型检测技术作为反例确认方法，实现了一种无假反例的混成系统近似可达集计算算法。实验证明该算法与目前已经得到广泛工业应用的有界模型检测算法相比具有更优的性能。
최강후건적계산시모형검측산법적핵심。본문사용일계라집가만족성모선성산술이론급출선성혼성자동궤적유계모형검측표시공식，이용일계라집공식불가만족정황하적삽치존재성정리，대선성혼성자동궤적유계모형검측공식진행지정적화분，사용지지선성산술삽치계산적가만족성모이론후단증명인경적선성시간복잡도적소해반증기술획득저량부분공식간적삽치공식，안일계라집 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 .