克里普克結構

本文介紹了在模型檢測中使用的克里普克結構。對於更一般介紹，請參見克里普克語義'。

克里普克結構（或稱Kripke結構）是遷移系統的一個變種，最初由索爾·克里普克^[1]提出，用於在模型檢測^[2]中表示一個系統的行為。克里普克結構本身是一個圖，其結點表示系統可達的狀態，其邊表示狀態的遷移。有一個標號函數將結點與結點所具有的性質的集合映射起來。時序邏輯傳統上是由克里普克結構進行解釋的。^{[來源請求]}

形式化定義

設 AP 為 原子命題 的集合，比如：包含變量、常量和謂詞符號的布爾表達式。 Clarke et al.^[3] 將一個定義在 AP 上的克里普克結構定義為一個四元組 M =(S, I, R, L)，其中：

一個有限狀態集合 S.
一個初始狀態集合 I ⊆ S.
一個遷移關係 R ⊆ S × S ，其中 R 是一個左部滿射的多值函數，即∀s ∈ S ∃s' ∈ S 使得 (s,s') ∈ R.
一個標號函數（或稱「解釋函數」） L: S →2^AP.

由於R 是一個多值函數，因此通過克里普克結構，總是能夠構建一個無窮路徑。死鎖狀態可以建模為僅存在一條指向自身的的出邊。標號函數 L 定義為：對於每個狀態 s ∈ S，L(s) 表示所有在 s 中有效的原子命題構成的集合。

克里普克結構 M 中的一條路徑是指一個狀態序列 ρ = s_1,s_2,s_3,...，其中，對於每個 i > 0，存在關係 R(s_i,s_i+1) 。路徑 ρ 上的單詞是指一個原子命題集合的序列 w=L(s₁),L(s₂),L(s₃),...，也就是定義在字母表2^AP上的一個 ω單詞。

由這一定義，僅包含一個初始狀態 i ∈ I 的一個Kripke結構可以通過一個單例輸入字母表被一個摩爾型有限狀態機識別，同時其輸出函數為克里普克結構的標號函數。^[4]

例子

設原子命題集合 AP ={p, q}。 p和q可以模任意可以由克里普克結構建模的系統中的布爾命題。

右圖表示了一個克里普克結構 M =(S, I, R, L)，其中：

S = {s₁, s₂, s₃}
I = {s₁}
R = {(s₁, s₂), (s₂,s₁), (s₂,s₃), (s₃、s₃)}
L = {(s₁, {p、q}), (s₂, {q}), (s₃, {p})}

M 可能產生一條路徑 ρ = s1,s2,s1,s2,s3,s3,s3,... 以及一個單詞 w = {p,q},{q},{p,q},{q},{p},{p},{p},...，其中 w 是執行路徑 ρ 對應的單詞。 M 可以產生屬於語言 ({p, q}{q})*({p})^ω∪({p, q}{q})^ω 的執行路徑。

與其他表示方式的關係

儘管這一術語被普遍使用於模型檢測社區，一些模型檢測的教科書上並沒有（或者實際上並沒有）以這種擴展的方式定義克里普克結構，而只是簡單使用了「（帶標號的）遷移系統」的概念，同時添加了一個包含原子命題 AP 集合的動作的集合 Act 。於是，遷移關係因此被定義為 S × Act × S 集合的子集，標號函數 L （L 如上文定義）即對應於動作集合 Act。在這種定義方法中，通過抽取動作標籤而得到的二元關係被稱為狀態圖。^[5]

Clarke et al. 重新定義了克里普克結構為一個轉換集合（而不僅僅是一個轉換）。當定義了模型μ-演算的語義時，轉換集合等價於上文中的標號遷移。

參見

參考文獻

^ Kripke, Saul, 1963, 「Semantical Considerations on Modal Logic,」 Acta Philosophica Fennica, 16: 83-94
^ Clarke, Edmund M. (2008): The Birth of Model Checking. in: Grumberg, Orna and Veith, Helmut eds.: 25 Years of Model Checking, Vol. 5000: Lecture Notes in Computer Science.
^ Clarke, Grumberg and Peled: "Model Checking", page 14.
^ Klaus Schneider. Verification of reactive systems: formal methods and algorithms. Springer. 2004: 45. ISBN 978-3-540-00296-3.
^ Christel Baier; Joost-Pieter Katoen. Principles of model checking. The MIT Press. : 20–21 and 94–95. ISBN 978-0-262-02649-9.

[1] Kripke, Saul, 1963, 「Semantical Considerations on Modal Logic,」 Acta Philosophica Fennica, 16: 83-94

[2] Clarke, Edmund M. (2008): The Birth of Model Checking. in: Grumberg, Orna and Veith, Helmut eds.: 25 Years of Model Checking, Vol. 5000: Lecture Notes in Computer Science.

[3] Clarke, Grumberg and Peled: "Model Checking", page 14.

[Schneider2004-4] Klaus Schneider. Verification of reactive systems: formal methods and algorithms. Springer. 2004: 45. ISBN 978-3-540-00296-3.

[BaierKatoen2008-5] Christel Baier; Joost-Pieter Katoen. Principles of model checking. The MIT Press. : 20–21 and 94–95. ISBN 978-0-262-02649-9.

[1]

[2]

[3]

[4]

[5]