模型检测

在计算机科学领域，模型检测或属性检测是一种用于验证系统的有限状态模型是否满足给定规范（即正确性）的方法。这种方法通常应用于硬件或软件系统；在此类系统中，规范不仅包含安全性需求（例如避免导致系统崩溃的状态），同时也包含活性需求（例如避免活锁现象）。

为了能够通过算法解决此类问题，系统的模型及其规范均需使用精确的数学语言进行形式化表述。为此，该问题被转化为逻辑范畴下的任务，即验证某个特定的结构是否满足给定的逻辑公式。这一通用概念适用于多种逻辑类型及各类结构。最基础的模型检测问题，即是验证给定的结构是否满足命题逻辑中的某个公式。

参见

• 抽象释义
• 自動化定理證明
• 二元决策图
• 形式验证
• 线性时序逻辑
• 程序分析
• 靜態程序分析