クリプキ構造（モデル検査）

この記事では、モデル検査で使用される Kripke 構造について説明します。より一般的な説明については、Kripke セマンティクスを参照してください。

クリプキ構造は遷移システムのバリエーションであり、もともとはソール・クリプキ^[1]によって提案され、モデル検査^[2]でシステムの振る舞いを表現するために使われています。これは、ノードがシステムの到達可能な状態を表し、エッジが状態遷移を表すグラフと、各ノードを対応する状態で保持される一連のプロパティにマッピングするラベリング関数で構成されています。時相論理は伝統的にクリプキ構造の観点から解釈されます。^[要出典]

正式な定義

$APを$ 原子命題、すなわち変数、定数、述語記号から構成されるブール値式のセットとする。クラークら^[3]は $AP$ 上のクリプキ構造を4組 $M = (S 、 I 、 R 、 L)$ として定義し、これは次の式で構成される。

状態の有限集合 $S$ 。
初期状態の集合 $I \subseteq S$ 。
遷移関係 $R \subseteq S \times S$ であって、 $R$ は左全、すなわち、 $\foralls \in S \existss' \in S$ であって、 $(s,s') \in R$ である。
ラベル付け（または解釈）関数 $L ： S \to 2AP$ 。

$Rは$ 左全であるため、クリプキ構造を通る無限パスを構築することが常に可能です。デッドロック状態は、それ自体に戻る単一の出力エッジによってモデル化できます。ラベル付け関数 $L は、各状態$ $s \in S$ に対して、 $s$ で有効なすべての原子命題の集合 $L (s)$ を定義します。

構造 $M$ のパスとは、各 $i$ $> 0に対して$ $R$ $($ $s$ $i$ $,$ $s$ $i$ $+1$ $)$ が成り立つような状態 $ρ$ $=$ $s$ $1$ $、$ $s$ $2$ $、$ $s$ $3$ $、 ...$ のシーケンスです。パス $ρ上の$ 単語は、原子命題の集合 $w$ $=$ $L$ $($ $s$ $1$ $)、$ $L$ $($ $s$ $2$ $)、$ $L$ $($ $s$ $3$ $)、 ...$ のシーケンスであり、これはアルファベット $2$ $AP$ 上のω 単語です。

この定義によれば、クリプキ構造（例えば、初期状態i∈Iを1つだけ持つ $）は、$ シングルトン入力アルファベットを持ち、出力関数がそのラベリング関数であるムーアマシンと同一 $視$ される可能性がある。 ^[4]

例

原子命題の集合を $AP = {p, q}$ とします。 $p$ と $q は$ 、クリプキ構造がモデル化しているシステムの任意のブール特性をモデル化できます。

右の図はクリプキ構造 $M = (S, I, R, L)$ を示しており、ここで

$S = {s 1 、s 2 、s 3}$ 。
$私は = {s 1}$ です。
$R = {(s 1, s 2)、(s 2, s 1) (s 2, s 3)、(s 3, s 3)}$ 。
$L = {(s 1, {p, q}), (s 2, {q}), (s 3, {p})}$ 。

$M は$ パス $ρ = s 1 、 s 2 、 s 1 、 s 2 、 s 3 、 s 3 、 s 3 、 ...$ を生成する可能性があり、 $w = {p, q}、 {q}、 {p, q}、 {q}、 {p}、 {p}、 {p}、 ...$ はパス $ρ$ 上の実行ワードです。 $M は、$ 言語 $({p, q}{q})*({p}) ω \cup ({p, q}{q}) ω$ に属する実行ワードを生成できます。

他の概念との関係

この用語はモデル検査コミュニティでは広く使われているが、モデル検査に関する教科書の中には「クリプキ構造」をこのように拡張した定義をしていないもの（あるいはまったく定義していないもの）もあり、単に（ラベル付きの）遷移システムの概念を使用している。この遷移システムにはアクションの集合 $Act も$ 含まれ、遷移関係は $S \times Act \times S$ のサブセットとして定義され、さらにこれを拡張して原子命題の集合と状態のラベル付け関数（上記で定義した $L ）も含まれるようになっている。このアプローチでは、アクションラベルを抽象化して得られる2項関係は$ 状態グラフと呼ばれる。^[5]

クラークらは、様相μ計算の意味を定義する際に、クリプキ構造を（1つだけではなく）遷移の集合として再定義した。これは上記のラベル付き遷移と同等である。[ ^6]

参照

参考文献

^ クリプキ、ソール、1963、「様相論理に関する意味論的考察」、アクタ・フィロソフィカ・フェンニカ、16: 83-94
^ Clarke, Edmund M. (2008): モデル検査の誕生。Grumberg, Orna および Veith, Helmut 編: モデル検査の 25 年、第 5000 巻: コンピュータサイエンスの講義ノート。Springer Berlin Heidelberg、p. 1-26。
^ Clarke, Edmund M. Jr; Grumberg, Orna ; Peled, Doron (1999 年 12 月)。モデル検査。サイバーフィジカルシステムシリーズ。MIT プレス。p. 14。ISBN 978-0-262-03270-4。
^ クラウス・シュナイダー (2004)。リアクティブシステムの検証：形式手法とアルゴリズム。シュプリンガー。p. 45。ISBN 978-3-540-00296-3。
^ クリステル・バイヤー;ヨースト・ピーター・カトーエン(2008)。モデル検査の原則。 MITプレス。 20〜21ページおよび94〜95ページ。ISBN 978-0-262-02649-9。
^ クラーク他 p.98

[1] クリプキ、ソール、1963、「様相論理に関する意味論的考察」、アクタ・フィロソフィカ・フェンニカ、16: 83-94

[2] Clarke, Edmund M. (2008): モデル検査の誕生。Grumberg, Orna および Veith, Helmut 編: モデル検査の 25 年、第 5000 巻: コンピュータサイエンスの講義ノート。Springer Berlin Heidelberg、p. 1-26。

[Clarke1999-3] Clarke, Edmund M. Jr; Grumberg, Orna ; Peled, Doron (1999 年 12 月)。モデル検査。サイバーフィジカルシステムシリーズ。MIT プレス。p. 14。ISBN 978-0-262-03270-4。

[Schneider2004-4] クラウス・シュナイダー (2004)。リアクティブシステムの検証：形式手法とアルゴリズム。シュプリンガー。p. 45。ISBN 978-3-540-00296-3。

[BaierKatoen2008-5] クリステル・バイヤー;ヨースト・ピーター・カトーエン(2008)。モデル検査の原則。 MITプレス。 20〜21ページおよび94〜95ページ。ISBN 978-0-262-02649-9。

[6] クラーク他 p.98