顯式狀態(tài)遷移模型-資料下載頁
2025-10-02 16:35本頁面
【正文】 } { (z0,z35), (z0,z12), … } { z0 } L: L(z0)=p?q?r,… 命題公式 36 s01 s0 s1 s2 s11 s02 s12 p,q p p q p?q 擴(kuò)展標(biāo)號(hào) Kripke模型：例 2 p,q q s2 p,q 37 擴(kuò)展標(biāo)號(hào) Kripke模型：例 2 ? 狀態(tài)集合： ? 遷移關(guān)系： ? 初始狀態(tài)集： ? 標(biāo)號(hào)函數(shù)： { s0, s1 ,s2 } { (s0,s1),(s1,s1),(s1,s2),(s2,s2) } { s0 } L: L(s0)=p, L(s1)=q, L(s2)=p?q 38 公平 Kripke模型 39 z0 z12 z35 z67 z97 z46 z20 z24 z47 ? 抽象狀態(tài)變化圖 : z78 z55 40 z0 z12 z35 z67 z97 z46 z20 z24 z47 ? 抽象狀態(tài)變化圖 : z78 z55 進(jìn)程 A的運(yùn)行 進(jìn)程 B的運(yùn)行 41 公平 Kripke 模型 ? 系統(tǒng)狀態(tài) ? 狀態(tài)變化 ? 初始狀態(tài) ? 公平性約束 抽象狀態(tài) 二元組 狀態(tài) 集合 狀態(tài) 集合的集合 公平 Kripke 模型 42 公平 Kripke 模型：例子 ? 狀態(tài)集合： ? 遷移關(guān)系： ? 初始狀態(tài)集： ? 公平性約束： { z0, z1, z2, z3, … } { (z0,z35), (z0,z12), … } { z0 } { {z35,z67, … }, {z12,z20, …} } 43 Kripke模型：安全性質(zhì) 系統(tǒng)的互斥性質(zhì)表示為安全性質(zhì) 44 Kripke模型：響應(yīng)性質(zhì) 系統(tǒng)具備的部分性質(zhì)包括響應(yīng)性質(zhì) (不滿足 )
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1