Kripke structure (model checking) とは

この記事では、モデル検査で使用されるKripke構造について説明します。より一般的な説明については、Kripkeのセマンティクスを参照してください。
Kripke構造は、元々Saul Kripkeによって提案された遷移システムの変形であり、システムの動作を表すためのモデル検査に使用されます。これは、基本的にノードがシステムの到達可能な状態を表し、エッジが状態遷移を表すグラフです。ラベリング機能は、各ノードを、対応する状態で保持されているプロパティのセットにマップする。時間的論理は、伝統的にクリプケ構造によって解釈される。