一階邏輯及其到Kripke Structure的轉換
阿新 • • 發佈：2018-11-26
First order logic: logical connectives and quantifications
- Describe states of concurrent system with first order logic
- V={v1,…,vn}is the set of system variables.
- Variables in V range over a finite set D
- A valuation for V is a function s: V→D
- A state is described by giving values for all of the elements in V
- State: Write a formula that is true for that valuation
反應系統(Reactive System)
反應系統需要和環境頻繁的發生作用且不會停止，具有以下特性：
- 狀態（state）：狀態表示系統瞬時的快照或狀態描述，主要可以用系統各個變數的變數值。
- 過渡（也有譯作遷移的，transition）：過渡表示從一個狀態到另一個狀態，一組狀態決定系統的一個過渡。
- 計算（computation）：計算表示一個狀態的無限序列，每個狀態由上一個狀態通過過渡得到。
Kripke Structure
Kripke 結構即過渡(遷移)系統的變化，在模型檢查中用來表示系統的行為，也可以用來描述上述的反應系統。Kripke 結構由狀態集合(S)、過渡集合(R)以及標記函式(L)組成。該標記函式標記各狀態下使得該狀態為true的變數集合。Kripke 結構是一個狀態過渡圖，路徑可以建模反應系統的計算。基於此，使用一階邏輯公式形式化併發系統。 定義AP為一組原子命題，則Kripke結構M為在原子命題上的一個四元組M=(S,S0,R,L),其中A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke,[1] used in model checking[2] to represent the behavior of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labelling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.
-wikipedia Kripke structure (model checking)
- S是有限的狀態集合。
- S0是S的子集，表示初始狀態。
- R是S的笛卡兒積，表示過渡(遷移)關係，且必須包含所有的，也就是說每個s總會有s’使得（s,s’）在關係R中。
- L是標記函式，標記原子命題使某狀態為真。
一階邏輯轉換到Kripke Structure
- D表示V的valuation集合。
- 狀態S的集合D X D得到(X表示笛卡兒積)。
- 初始狀態S0通過V中的valuation(0)獲得。
- 若s和s’是兩個狀態，則過渡(遷移)R(s,s’)成立的條件是每一個v屬於V使得s(v)和每一個v’屬於V’使得s(v’)為真。
- 標記函式L(s)是原子命題集合的子集，該集合使得狀態s成立。對於布林變數的v，若v屬於L(s)，則s(v)=true，若v不屬於L(s)，則s(v)=false。
