跳至內容

克里普克結構

維基百科,自由的百科全書
本文介紹了在模型檢測中使用的克里普克結構。對於更一般介紹,請參見克里普克語義'。

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

形式化定義

[編輯]

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

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

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

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

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

例子

[編輯]

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

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

  • S = {s1, s2, s3}
  • I = {s1}
  • R = {(s1, s2), (s2,s1), (s2,s3), (s3、s3)}
  • L = {(s1, {p、q}), (s2, {q}), (s3, {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. 重新定義了克里普克結構為一個轉換集合(而不僅僅是一個轉換)。當定義了模型μ-演算的語義時,轉換集合等價於上文中的標號遷移。

參見

[編輯]

參考文獻

[編輯]
  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.
  4. ^ Klaus Schneider. Verification of reactive systems: formal methods and algorithms. Springer. 2004: 45. ISBN 978-3-540-00296-3. 
  5. ^ Christel Baier; Joost-Pieter Katoen. Principles of model checking. The MIT Press. : 20–21 and 94–95. ISBN 978-0-262-02649-9.