モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。モデル検査はハードウェア設計に適用されることが最も多い。ソフトウェアに対するモデル検査は決定不能であるため、アルゴリズム的な手法だけでは完全ではなく、証明も反証もできない場合がある。モデルはハードウェア記述言語や専用の言語で記述されたソースコードの形態となるのが一般的である。そのようなプログラムは有限状態機械に対応付けられ、ノード（接点）とエッジから成る有向グラフで表される。原子命題の集合は各ノードと対応し、一般にメモリ要素の内容に対応する。ノードはシステムの状態を表し、エッジはある状態から他の状態への遷移可能性を意味する。その場合、原子命題は実行のある時点で保持される基本的属性を表す。問題を形式的に表現すると次のようになる。時相論理の論理式 "p" で表される属性について、初期状態 "s" のモデル "M" があるとき、formula_1 が成り立つかどうかを決定する。ハードウェアの場合のように "M" が有限であれば、モデル検査はグラフ探索に帰着できる。実世界の問題を扱おうとしたとき、モデル検査は状態組み合わせ爆発問題（状態の数が膨大となって検査不能となること）に直面する。これに対応する方法はいくつか存在する。モデル検査は当初、離散状態系の論理的正当性を調べるために開発されたが、リアルタイムシステムや限定された形式のハイブリッドシステムにも対応できるよう拡張されてきている。

出典:wikipedia