21/8/16 4
什么是模型检查？
定义 [Clarke & Emerson 1981]
“Model checking is an automated technique that, give
n a finite-state model of a system and a logical proper
ty, systematically checks whether this property holds f
or (a given initial state in) that model.”
基本思想
用状态迁移系统 (S) 表示系统的行为，用模态 / 时序
逻辑公式 (F) 描述系统的性质。这样用数学问题“状态
迁移系统 S 是否是公式 F 的一个模型？”来判定“系统是
否具有所期望的性质” ， S F?
评论0