モデルが特定の安全性制約(プロパティ)に違反しないことを証明する手法はどれか。

モデルチェッキングは全探索を用いて、モデルが定義された論理制約を破ることがないかを確認する。