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

• 作者: 喻钢 徐中伟 陈祖希 霍伟伟
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: Craig 插值 可满足性模理论 线性混成自动机 符号模型检验 混成系统
• 年，卷（期）: 2014,（7）
• 所属期刊栏目: 学术论文
• 页码范围: 1338-1346
• 页数: 9页
• 分类号: TP311.1
• 字数: 12435字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2014.07.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐中伟	同济大学电子与信息工程学院	95	644	13.0	20.0
2	喻钢	上海大学悉尼工商学院	24	147	7.0	11.0
3	陈祖希	同济大学电子与信息工程学院	5	17	3.0	4.0
4	霍伟伟	上海大学悉尼工商学院	9	40	3.0	6.0