本站支持尊重有效期内的版权/著作权,所有的资源均来自于互联网网友分享或网盘资源,一旦发现资源涉及侵权,将立即删除。希望所有用户一同监督并反馈问题,如有侵权请联系站长或发送邮件到ebook666@outlook.com,本站将立马改正
图书基本信息 | |
图书名称 | Petri网的元展-一种并发系统模型检测方法 |
作者 | 刘关俊 |
定价 | 99元 |
出版社 | 教育科学出版社 |
ISBN | 9787030662590 |
出版日期 | |
字数 | |
页码 | |
版次 | |
装帧 | |
开本 | |
商品重量 |
内容提要 | |
Petri网的元展:一种并发系统模型检测方法主要介绍Petri网的元展这一用于并发系统模型检测的方法,利用元展检测并发系统健壮性兼容性与死锁,并利用元展检测能够表达更多的并发系统设计需求的计算树逻辑,同时还探讨了健壮性兼容性死锁等判定问题的复杂度Petri网的元展:一种并发系统模型检测方法共10章,具有严格的形式化定义丰富的示例与图文解释严谨的定理及其证明,以及清晰的算法描述 |
目录 | |
序言 章 绪论 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 基于元展的资源分配... |