模型检测

模型检测是一种自动验证有限状态系统的技术。

核心思想

通过穷举系统所有可能状态，验证是否满足给定的时序逻辑性质。

输入

• 系统模型（有限状态机）
• 性质规约（LTL/CTL）

主要挑战

• 状态爆炸问题
• 无限状态系统

解决方案

• 符号模型检测
• 有界模型检测
• 抽象精化