●序言
第1章 緒論 1
1.1 研究背景 1
1.2 研究現狀與問題 3
1.3 研究內容 4
第2章 基本知識 6
2.1 袋集 6
2.2 並發繫統的Petri網模型 7
2.2.1 Petri網的定義 7
2.2.2 可達性、活性、死鎖與活鎖 9
2.2.3 結構良好的Petri網子類及其性質 11
2.2.4 工作流網及其健壯性 13
2.2.5 跨組織工作流網及其兼容性 15
2.2.6 資源分配網及其無死鎖性 16
2.3 計算樹邏輯 17
第3章 並發繫統若干判定問題的復雜度 20
3.1 一些經典的 PSPACE接近與NP接近問題 20
3.1.1 線性有界自動機接受問題 20
3.1.2 布爾可滿足性問題與Tautology問題 21
3.1.3 劃分問題 22
3.2 工作流網健壯性判定問題的復雜度 22
3.2.1 健壯性判定問題是PSPACE難的 22
3.2.2 有界工作流網健壯性問題是PSPACE接近的 32
3.3 一些特殊結構的工作流網健壯性問題的復雜度 34
3.3.1 無環工作流網健壯性問題是co-NP接近的 34
3.3.2 安全非對稱選擇工作流網健壯性問題是co-NP難的 37
3.3.3 無環非對稱選擇工作流網健壯性等價於弱健壯性 41
3.3.4 自由選擇工作流網健壯性等價於弱健壯性 43
3.4 跨組織工作流網兼容性判定問題的復雜度 44
3.5 資源分配網死鎖判定問題的復雜度 45
3.5.1 安全的資源分配網死鎖判定問題是NP接近的 45
3.5.2 賦權的資源分配網死鎖判定問題是NP接近的 48
第4章 Petr展 51
4.1 Petri網的展開 51
4.1.1 並發與衝突 51
4.1.2 分支進程 51
4.1.3 展開 54
4.2 Petr展的定義 55
4.2.1 切與可能擴展 55
4.2展 58
4.3 Pet展的有限性 60
4.4 有界Pet展的完整性 62
4.5 Pet展的生成算法 63
4.5.1 展開的生成算法 63
4.5展的生成算法 64
第5章展的工作流繫統健壯性檢測 69
5.1 工展的特性 69
5.1.1 無界工展的特性 69
5.1.2 有界工展的特性 73
5.2展的健壯性判定 76
5.2.1 充分必要條件 76
5.2.2 充分性證明 79
5.2.3 必要性證明 80
5.3 應用實例：電梯調度繫統 82
5.3.1 電梯調度繫統描述 82
5.3.2 電梯調度繫統的工作流網模型 83
5.3.3展分析電梯調度繫統 84
第6章展的跨組織工作流網兼容性檢測 86
6.1展判定跨組織工作流網兼容性 86
6.2 允許簡單回路的跨組織工作流網：SCIWF-網 88
6.3 SCIWF-網的T-構件與帽的定義 89
6.3.1 無環FCWF-網的T-構件與帽 89
6.3.2 SCIWF-網的T-構件與帽 91
6.4 基於T-構件與帽的SCIWF-網兼容性判定 97
6.4.1 充要條件 97
6.4.2 判定弱兼容性的算法 101
6.4.3 判定兼容性的算法 102
6.5 應用實例：三方交互的訂貨流程 103
6.5.1 三方交互的訂貨流程簡介及其 SCIWF-網模型 103
6.5.2 三方交互的兼容性分析 104
第7章展的資源分配繫統死鎖檢測 105
7.1 資源展的特性 105
7.2展的資源分配網死鎖檢測 107
7.3 應用實例一：哲學家就餐問題 108
7.3.1 哲學家就餐問題描述 108
7.3.2 哲學家就餐問題的資源分配網模型 108
7.3.3展分析哲學家就餐問題 109
7.4 應用實例二：柔性制造繫統 111
7.4.1 柔性制造繫統描述 111
7.4.2 柔性制造繫統的資源分配網模型 113
7.4.3展分析柔性制造繫統 113
第8章展的計算樹邏輯公式檢測 114
8.1展檢測計算樹邏輯的思路 114
8.2 原子展上的標記算法 116
8.2.1展中並發關繫 116
8.2.2 基於無向圖極大團求解切 121
8.2.3 原子命題的標記 123
8.3 經典邏輯展上的標記算法 124
8.3.1 φ的標記 124
8.3.2 φ1∨φ2 的標記 124
8.3.3 φ1∧φ2 的標記 124
8.4 時序展上的標記算法 124
8.4.1 EXφ的標記 125
8.4.2 EFφ的標記 127
8.4.3 E[φ1Uφ2] 的標記 128
8.4.4 AXφ的標記 130
8.4.5 AFφ的標記 131
8.4.6 A[φ1Uφ2] 的標記 133
8.5 應用實例：無饑餓的哲學家就餐 134
8.5.1 無饑餓的哲學家就餐問題描述及其Petri網模型 134
8.5.2展檢測無饑餓性 137
8.5.3 實驗結果 138
第9章 模型檢測工具BUCKER簡介 140
第10章 總結與展望 143
參考文獻 145
關鍵詞中英文對照表 157
