克里普克結構

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

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

形式化定義

設 AP 為 原子命題 的集合，比如：包含變量、常量和謂詞符號的布爾表達式。 Clarke et al. 將一個定義在 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結構可以通過一個單例輸入字母表被一個摩爾型有限狀態機識別，同時其輸出函數為克里普克結構的標號函數。

例子

設原子命題集合 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。在這種定義方法中，通過抽取動作標籤而得到的二元關係被稱為狀態圖。

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

參見

• 時間邏輯
• 模型檢測
• 克里普克語義
• 線性時序邏輯
• 計算樹邏輯