基于Petri網的計算樹邏輯模型檢測

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

暫缺《基于Petri網的計算樹邏輯模型檢測》作者簡介