模型检测（Model Checking）

模型检测是一种自动验证有限状态系统是否满足给定规约的形式化方法，它把系统建模为状态转移结构，把待验证性质写成时序逻辑公式，然后由算法自动、穷尽地检查所有可能状态以判定性质是否成立。

概述

模型检测由埃德蒙·克拉克（Edmund Clarke）、艾伦·埃默森（Allen Emerson）与约瑟夫·西弗基斯（Joseph Sifakis）在二十世纪八十年代分别独立创立，三人于2007年共获图灵奖。与需要人工引导的定理证明不同，模型检测在可行范围内是全自动的，且在性质不成立时能给出一条反例路径帮助定位缺陷。

核心原理

• 状态转移系统：把被验证系统抽象为状态和状态间转移的集合，通常表示为克里普克结构。
• 时序逻辑：用线性时序逻辑或计算树逻辑描述系统随时间演化应满足的性质，如安全性与活性。
• 穷尽搜索：算法遍历可达状态空间，判断每条执行路径是否都符合规约。
• 反例：当性质不成立时，返回一条违反性质的具体执行轨迹。
• 状态爆炸：状态数随并发组件指数增长，是模型检测的核心难题。

应用场景

模型检测广泛用于硬件电路验证、通信协议正确性检查、并发与分布式系统的死锁检测，以及安全关键软件的验证。符号模型检测借助二元决策图和可满足性求解技术处理超大状态空间，使其能应对工业级规模的设计。

常见问题

问：状态爆炸问题怎么应对？答：常用技术包括用二元决策图符号化表示状态集合、基于可满足性求解的有界模型检测、偏序归约消除等价的并发交错、以及抽象化把大系统近似为小系统，从而压缩需要探索的状态空间。

问：模型检测和定理证明各有什么优劣？答：模型检测自动且能给出反例，但受状态爆炸限制，通常处理有限状态系统；定理证明能处理无限状态和更一般的性质，但往往需要专家人工介入，两者互补。