克里普克結構
- 本文介紹了佇模型檢測中使用的克里普克結構。對閣較一般來介紹，來請參見克里普克語義'。
克里普克結構（抑是稱 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 _ → 二 AP .
因為 _ R _ 是一个多值函數，所以通過克里普克結構，總是會當構建一个無窮路草。死鎖的狀態會當建模為干焦有一條指向家己的出邊。標號函數 _ L _ 定義做：對每一个狀態 _ s _ ∈ _ S _，_ L _ ( _ s _ ) 表示所有咧 _ s _ 中有效的原子命題構成的集合。
克里普克結構 _ M _ 中的一條 _ 路徑 _ 是講一个狀態序列 ρ=_ s _ 一 , _ s _ 二 , _ s _ 三 , . . .，其中，對著每一个 i > 零，存在關係 _ R _ ( _ s _ i , _ si + 一 _ )。路徑 ρ 上的 _ 單詞 _ 是講一个原子命題集合的序列 _ w _=_ L _ ( s 一 ) , _ L _ ( s 二 ) , _ L _ ( s 三 ) , . . .，也就是定義在字母表二 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 _ 可能產生一條路徑 ρ=s 一 , s 二 , s 一 , s 二 , s 三 , s 三 , s 三 , . . . 猶閣一个單詞 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 . 重新定義矣克里普克結構為一个轉換集合（毋但是一个轉換）。 當定義矣模型 μ-演算的語義的時陣，轉換集合等價於上文中的標號搬徙。
參見
- 時間邏輯
- 模型檢測
- 克里普克語義
- 線性時序邏輯
- 計算樹邏輯