扫一扫
关注中图网
官方微博
本类五星书更多>
-
>
决战行测5000题(言语理解与表达)
-
>
软件性能测试.分析与调优实践之路
-
>
第一行代码Android
-
>
深度学习
-
>
Unreal Engine 4蓝图完全学习教程
-
>
深入理解计算机系统-原书第3版
-
>
Word/Excel PPT 2013办公应用从入门到精通-(附赠1DVD.含语音视频教学+办公模板+PDF电子书)
Petri网的元展:一种并发系统模型检测方法 版权信息
- ISBN：9787030662590
- 条形码：9787030662590 ; 978-7-03-066259-0
- 装帧：一般胶版纸
- 册数：暂无
- 重量：暂无
- 所属分类：>
Petri网的元展:一种并发系统模型检测方法 内容简介
本书以Petri网这一刻画并发系统的数学模型为基础，提出了一种偏序结构的验证系统行为正确性的方法：元展。主要内容包括：系统性界定了行为正确性判定的复杂度，给出了构造元展的算法，提出了利用元展验证死锁、活锁、健壮性、兼容性的充分必要条件，提出了利用元展检测线性时序逻辑、计算树逻辑的算法，同时介绍了所开发的模型检测工具，并且将一些应用实例来展示所提方法的有效性。
Petri网的元展:一种并发系统模型检测方法 目录
目录
序言
第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章 Petri网的元展 51
4.1 Petri网的展开 51
4.1.1 并发与冲突 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章 基于元展的工作流系统健壮性检测 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
序言
第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章 Petri网的元展 51
4.1 Petri网的展开 51
4.1.1 并发与冲突 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章 基于元展的工作流系统健壮性检测 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
展开全部
Petri网的元展:一种并发系统模型检测方法 作者简介
刘关俊，男，教授，博士生导师。2011年获得同济大学计算机软件与理论专业博士学位，同年赴新加坡科技设计大学从事博士后研究工作；2013年回国，并进入同济大学计算机科学系任教，同年获得德国洪堡基金资助，赴柏林洪堡大学从事博士后研究工作。 主要从事形式化方法、模型检测、Petri网等方面的理论与应用研究，目前也从事机器学习及其在网络交易欺诈检测方面的研究。已出版学术专著1本，发表学术论文90余篇，包括Science China Information Sciences、ACM Transactions on Embedded Computing Systems、ACM Transactionson Cyber-Physical Systems、IEEE Transactions on Services Computing、IEEE Transactions on Industrial Informatics等期刊论文近50篇，以及靠前Petri网年会（International Conference on Application and Theory of Petri Nets and Concurrency）等会议论文40余篇。 刘关俊主持国家自然科学基金面上项目与青年基金项目、上海市曙光计划人才项目、中央高校交叉项目（重大）等多项，获得国家科技进步奖二等奖、上海市科技进步奖一等奖、中国电子学会自然科学一等奖、吴文俊人工智能技术发明奖一等奖、上海市很好博士论文奖以及首届教育部国务院学位委员会博士研究生学术新人奖等。刘关俊是中国计算机学会形式化方法专委会委员、中国自动化学会网络信息服务专委会委员、中国人工智能学会智能空天系统专委会委员、IEEESenior Member。
书友推荐
- >
经典常谈
经典常谈
¥19.5¥39.8 - >
二体千字文
二体千字文
¥14.0¥40.0 - >
月亮与六便士
月亮与六便士
¥18.1¥42.0 - >
人文阅读与收藏·良友文学丛书:一天的工作
人文阅读与收藏·良友文学丛书:一天的工作
¥16.5¥45.8 - >
中国历史的瞬间
中国历史的瞬间
¥16.7¥38.0 - >
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
¥6.3¥14.0 - >
我从未如此眷恋人间
我从未如此眷恋人间
¥17.5¥49.8 - >
回忆爱玛侬
回忆爱玛侬
¥9.8¥32.8
本类畅销
-
”互联网+“时代计算机算法的应用及其实践研究
¥19.9¥59 -
微服务设计
¥52.8¥69 -
图说深度学习:用可视化方法理解复杂概念
¥109¥188 -
计算机基础
¥17.2¥31 -
改变未来的九大算法
¥50¥68 -
生成式AI入门与AWS实战
¥77.8¥99.8
