Petri網的元展：一種并發(fā)系統(tǒng)模型檢測方法

目錄
序言
第1章 緒論 1
1.1 研究背景 1
1.2 研究現(xiàn)狀與問題 3
1.3 研究內容 4
第2章 基本知識 6
2.1 袋集 6
2.2 并發(fā)系統(tǒng)的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章 并發(fā)系統(tǒng)若干判定問題的復雜度 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 無環(huán)工作流網健壯性問題是co-NP完全的 34
3.3.2 安全非對稱選擇工作流網健壯性問題是co-NP難的 37
3.3.3 無環(huán)非對稱選擇工作流網健壯性等價于弱健壯性 41
3.3.4 自由選擇工作流網健壯性等價于弱健壯性 43
3.4 跨組織工作流網兼容性判定問題的復雜度 44
3.5 資源分配網死鎖判定問題的復雜度 45
3.5.1 安全的資源分配網死鎖判定問題是NP完全的 45
3.5.2 賦權的資源分配網死鎖判定問題是NP完全的 48
第4章 Petri網的元展 51
4.1 Petri網的展開 51
4.1.1 并發(fā)與沖突 51
4.1.2 分支進程 51
4.1.3 展開 54
4.2 Petri網的元展的定義 55
4.2.1 切與可能擴展 55
4.2.2 元展 58
4.3 Petri網元展的有限性 60
4.4 有界Petri網元展的完整性 62
4.5 Petri網元展的生成算法 63
4.5.1 展開的生成算法 63
4.5.2 元展的生成算法 64
第5章 基于元展的工作流系統(tǒng)健壯性檢測 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 應用實例：電梯調度系統(tǒng) 82
5.3.1 電梯調度系統(tǒng)描述 82
5.3.2 電梯調度系統(tǒng)的工作流網模型 83
5.3.3 基于元展分析電梯調度系統(tǒng) 84
第6章 基于元展的跨組織工作流網兼容性檢測 86
6.1 基于元展判定跨組織工作流網兼容性 86
6.2 允許簡單回路的跨組織工作流網：SCIWF-網 88
6.3 SCIWF-網的T-構件與帽的定義 89
6.3.1 無環(huán)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章 基于元展的資源分配系統(tǒng)死鎖檢測 105
7.1 資源分配網元展的特性 105
7.2 基于元展的資源分配網死鎖檢測 107
7.3 應用實例一：哲學家就餐問題 108
7.3.1 哲學家就餐問題描述 108
7.3.2 哲學家就餐問題的資源分配網模型 108
7.3.3 基于元展分析哲學家就餐問題 109
7.4 應用實例二：柔性制造系統(tǒng) 111
7.4.1 柔性制造系統(tǒng)描述 111
7.4.2 柔性制造系統(tǒng)的資源分配網模型 113
7.4.3 基于元展分析柔性制造系統(tǒng) 113
第8章 基于元展的計算樹邏輯公式檢測 114
8.1 基于元展檢測計算樹邏輯的思路 114
8.2 原子命題在元展上的標記算法 116
8.2.1 求解元展中并發(fā)關系 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