本書主要介紹Petri網(wǎng)的元展這一用于并發(fā)系統(tǒng)模型檢測的方法，利用元展檢測并發(fā)系統(tǒng)健壯性、兼容性與死鎖，并利用元展檢測能夠表達更多的并發(fā)系統(tǒng)設計需求的計算樹邏輯，同時還探討了健壯性、兼容性、死鎖等判定問題的復雜度。全書共10章，具有嚴格的形式化定義、豐富的示例與圖文解釋、嚴謹?shù)亩ɡ砑捌渥C明，以及清晰的算法描述。

更多科學出版社服務，請掃碼獲取。