學生看的系統分析與驗證筆記——Kripke structure

目錄   Kripe結構 一階邏輯公式表示併發系統 基礎定義 描述併發系統的狀態 描述併發系統的狀態變遷 從一階邏輯公式構造KS Kripe結構 首先給出Kripke的定義： 令AP是原子命題，則AP上的四元組M稱爲Kripke結構，，其中 是一個有限的集合，它的每一個元素稱爲一個狀態，即狀態的有限集 是初始狀態集 是變遷關係 是標識函數，標識在某個狀態下爲真的原子命題集 當我們並不關心初始狀態時

>>阅读原文<<