本書主要介紹原型 Petri 網(wǎng)、知識(shí) Petri 網(wǎng)、帶有優(yōu)先級(jí)的時(shí)間 Petri網(wǎng)，用于對(duì)有限狀態(tài)并發(fā)系統(tǒng)控制流、安全多方計(jì)算協(xié)議、多處理器搶占式實(shí)時(shí)系統(tǒng)等在一定層級(jí)上的抽象建模，如刻畫并發(fā)、選擇、沖突、多方交互、多方認(rèn)知過程、（搶占式）資源分配、事件的實(shí)時(shí)性約束等。本書介紹的計(jì)算樹邏輯、知識(shí)計(jì)算樹邏輯、時(shí)間計(jì)算樹邏輯等可以用于規(guī)約這些系統(tǒng)所關(guān)注的設(shè)計(jì)需求，如無(wú)死鎖、公平性、隱私性、可調(diào)度性、最壞執(zhí)行時(shí)間等。本書重點(diǎn)介紹使用這些 Petri 網(wǎng)模型驗(yàn)證以上時(shí)序邏輯的算法。另外，本書介紹簡(jiǎn)化有序二叉決策圖，介紹如何將其用于表達(dá) Petri 網(wǎng)的狀態(tài)、狀態(tài)間的遷移關(guān)系及狀態(tài)間的等價(jià)關(guān)系，并將其應(yīng)用于計(jì)算樹邏輯與 知識(shí)計(jì)算樹邏輯的模型檢測(cè)上。

更多科學(xué)出版社服務(wù)，請(qǐng)掃碼獲取。