顯式狀態(tài)遷移模型-在線瀏覽
2024-12-14 16:35本頁面
【正文】 : 狀態(tài)的標(biāo)號 : 28 標(biāo)號 Kripke模型：安全性質(zhì) 系統(tǒng)的互斥性質(zhì)表示為安全性質(zhì) 29 標(biāo)號 Kripke模型：響應(yīng)性質(zhì) 系統(tǒng)具備的部分性質(zhì)包括響應(yīng)性質(zhì) (不滿足 ) 30 擴(kuò)展標(biāo)號 Kripke模型 31 z0 z12 z35 z67 z97 z46 z20 z24 z47 ? 抽象狀態(tài)變化圖 : z78 z55 p,q,r p: a=s0 q: b=t0 r: t=0 s: a=s0?b=t0 p p p,r q q q r r 32 z0 z12 z35 z67 z97 z46 z20 z24 z47 ? 抽象狀態(tài)變化圖 : z78 z55 p?q?r p: a=s0 q: b=t0 r: t=0 s: a=s0?b=t0 ?p??q??r ?p??q??r p??q?r p??q??r p??q??r ?p?q??r ?p?q??r ?p?q??r ?p??q?r ?p??q?r 33 z0 z12 z35 z67 z97 z46 z20 z24 7? 抽象狀態(tài)變化圖 : z78 z55 p?q?r p: a=s0 q: b=t0 r: t=0 s: a=s0?b=t0 ?p??q??r p??q?r p??q??r p??q??r ?p?q??r ?p?q??r ?p?q??r ?p??q?r ?p??q 34 擴(kuò)展標(biāo)號 Kripke模型 ? 系統(tǒng)狀態(tài) ? 狀態(tài)變化 ? 初始狀態(tài) ? 狀態(tài)信息 抽象狀態(tài) 二元組 狀態(tài) 集合 公式 擴(kuò)展標(biāo)號 Kripke模型 35 擴(kuò)展標(biāo)號 Kripke模型：例子 ? 狀態(tài)集合： ? 遷移關(guān)系： ? 初始狀態(tài)集： ? 標(biāo)號函數(shù)： { z0, z1, z2, z3, …
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1