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

《基于Craig插值的线性混成系统符号化模型检测.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第7期电子学报Vo1．42No．72014年7月ACrAELlSCI'R0NICASINICAJu1．2014基于Craig插值的线性混成系统符号化模型检测陈祖希，徐中伟，霍伟伟，喻钢(1．同济大学电子与信息工程学院，上海201804；2．上海大学悉尼工商学院，上海201800)摘要：最强后件的计算是模型检测算法的核心．本文使用一阶逻辑可满足性模线性算术理论给出线性混成自动机的有界模型检测表示公式，利用一阶逻辑公式不可满足情况下的插值存在性定理，对线性混成自动机的有界模型检测公式进行指定的划分，使用支持线性算术插值计算的可满足性模理论后端证明引擎的

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

3、线性混成自动机；符号模型检验；混成系统中图分类号：TP311．1文献标识码：A文章编号：0372．2112(2014)07．1338．09电子学报URL：http：／／www．ejourna1．org．cnDOI：10．3969／j．issn．0372—2112．2014．07．014SymbolicModelCheckingforLinearHybridSystemsBaseonCraigInterpolationCHENZu．xi，XUZhong-wei，HUOWei．wei2,YUGan(1．SchoolofElectronicsandInf

4、ormation，TonalUniversity，∞咖201804，China；2．SHU-UTSBusinessSchool，ShanghaiUniversity，Shanghai201800，China)Abstract：Thekeytomodelchecking~gofithmisthecomputationofs~ongestpostcondidon．ThisarticleencodestheboundedmodelcheckingproblemforlinearhybridautomataasformulaofSATModulotheor

5、iesforlineararithmetic．Wedividedtheformulaintotwospecificpartstoobtaintheinterpolationwithalineartimecomplexity．AccordingtothepropertiesofCraigin—terpolationtheoremforfirstorderlogic，theinterpolationasanover-approximationstrongestpostconditionandcanreplacetheorigi—nalstrongest

6、postconditionusedinsymbolicmodelcheckingforhybridautomatawithexponentialtimecomplexity．ThismethoddoesnotrequiretotheIrausitionrelationisfullyexpandedthesameasboundedmodelcheckingtochecksatisfiability，also．Weim—plementthehybridsystemsmodelcheckingalgorithmwithoutfalsecounter-ex

7、ampleusingtheovevapproximafionstrongestpostconditionoperatortogetherwithboundedmodelcheckingalgorithm．ExperimentsshowthatourapproachCallbemoreeficientthanboundedmodelcheckingforhybridsystems．Keywords：Craiginterpolation；satisfiabilitymodulotheories；linearhybridautomata；modelche

8、cking；hybridsystems交互的系统．这种连续和离散行为，以及行为之间的交1引言互使得混成系统表现出了比一般系