商品详情
书名：基于Petri网的计算树逻辑模型检测
定价：108.0
ISBN：9787030772848
作者：刘关俊,何雷锋
版次：1
出版时间：2024-01
内容提要：
本书主要介绍原型 Petri 网、知识 Petri 网、带有优先级的时间 Petri网，用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模，如刻画并发、选择、冲突、多方交互、多方认知过程、（抢占式）资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求，如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍使用这些 Petri 网模型验证以上时序逻辑的算法。另外，本书介绍简化有序二叉决策图，介绍如何将其用于表达 Petri 网的状态、状态间的迁移关系及状态间的等价关系，并将其应用于计算树逻辑与 知识计算树逻辑的模型检测上。
目录：
目录
前言
第1章 绪论 1
1.1 研究背景 1
1.2 研究现状 3
1.2.1 有限状态并发系统控制流的模型检测 3
1.2.2 安全多方计算协议的模型检测 5
1.2.3 多处理器抢占式实时系统的模型检测 7
1.3 内容概述 9
第2章 基础知识 11
2.1 原型 Petri 网 11
2.1.1 常用的集合符号 11
2.1.2 原型 Petri 网的定义 12
2.1.3 原型 Petri 网的性质 15
2.2 时间 Petri 网 16
2.2.1 时间 Petri 网的定义 17
2.2.2 时间 Petri 网的状态类图 18
2.3 优先级时间 Petri 网 21
2.3.1 优先级时间 Petri 网的定义 21
2.3.2 状态类图 21
2.4 模型检测 22
第3章 简化有序二叉决策图 24
3.1 布尔函数简介 24
3.1.1 布尔函数 24
3.1.2 布尔函数的其他描述形式 27
3.2 简化有序二叉决策图简介 31
3.2.1 ROBDD 的定义 31
3.2.2 ROBDD 的性质 33
3.3 ROBDD 的变量排序方法 34
3.3.1 动态变量排序法 35
3.3.2 静态变量排序法 37
3.4 基于 ROBDD 符号表达 Petri 网 41
3.4.1 基于 ROBDD 符号表达安全 Petri 网 41
3.4.2 基于 ROBDD 符号表达有界 Petri 网 49
第4章 计算树逻辑模型检测 59
4.1 计算树逻辑 59
4.1.1 CTL 的语法与语义 59
4.1.2 CTL 的标准范式 62
4.2 CTL 的传统验证方法 62
4.3 基于 ROBDD 的 CTL 验证方法 66
4.3.1 第一种符号模型检测 CTL 的方法 67
4.3.2 第二种符号模型检测 CTL 的方法 70
4.4 应用实例 73
4.4.1 柔性制造系统 73
4.4.2 多线程程序 74
4.5 实验与分析 76
4.5.1 哲学家就餐问题 77
4.5.2 资源分配系统 84
4.5.3 埃拉托色尼筛选法 86
4.5.4 n 皇后问题 89
第5章 知识 Petri 网 92
5.1 知识 Petri 网的定义 92
5.2 带有等价关系的可达图 RGER 93
5.3 基于 ROBDD 符号表达 RGER 97
第6章 知识计算树逻辑模型检测 100
6.1 知识计算树逻辑 100
6.2 基于 RGER 的 CTLK 的验证方法 102
6.3 基于 ROBDD 的 CTLK 的验证方法 108
6.3.1 第一种符号模型检测 CTLK 的方法 108
6.3.2 第二种符号模型检测 CTLK 的方法 111
6.4 应用实例：密码学家就餐协议 116
第7章 带有计时器的时间 Petri 网 127
7.1 传统的四种带有计时器的时间 Petri 网 127
7.1.1 调度扩展时间 Petri 网 127
7.1.2 抢占式时间 Petri 网 130
7.1.3 带有抑止超弧的时间 Petri 网 132
7.1.4 计时器时间 Petri 网 135
7.2 优先级时间点区间 Petri 网 138
7.2.1 优先级时间点区间 Petri 网 PToPN 的定义 138
7.2.2 PToPN 的状态图 141
第8章 时间计算树逻辑模型检测 145
8.1 时间计算树逻辑 145
8.1.1 TCTL 的语法与语义 145
8.1.2 TCTL 的标准范式 147
8.2 基于 PToPN 的 TCTL 的验证方法 148
8.3 带有时间未知数的时间计算树逻辑 155
8.3.1 TCTLx 的语法与语义 155
8.3.2 基于 PToPN 的 TCTLx 的验证方法 157
8.4 应用实例 159
8.4.1 系统描述与两个不同的网模型 159
8.4.2 基于 TCTLx 的性质规约 163
8.4.3 实验结果与分析 165
第9章 模型检测器 169
9.1 模型检测器框架概述 169
9.2 CTL 模型检测器 170
9.3 CTLK 模型检测器 173
9.4 TCTL 模型检测器 175
9.5 TCTLx 模型检测器 177
第10章 总结与展望 180
10.1 总结 180
10.2 展望 181
参考文献 183
定价：108.0
ISBN：9787030772848
作者：刘关俊,何雷锋
版次：1
出版时间：2024-01
内容提要：
本书主要介绍原型 Petri 网、知识 Petri 网、带有优先级的时间 Petri网，用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模，如刻画并发、选择、冲突、多方交互、多方认知过程、（抢占式）资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求，如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍使用这些 Petri 网模型验证以上时序逻辑的算法。另外，本书介绍简化有序二叉决策图，介绍如何将其用于表达 Petri 网的状态、状态间的迁移关系及状态间的等价关系，并将其应用于计算树逻辑与 知识计算树逻辑的模型检测上。
目录：
目录
前言
第1章 绪论 1
1.1 研究背景 1
1.2 研究现状 3
1.2.1 有限状态并发系统控制流的模型检测 3
1.2.2 安全多方计算协议的模型检测 5
1.2.3 多处理器抢占式实时系统的模型检测 7
1.3 内容概述 9
第2章 基础知识 11
2.1 原型 Petri 网 11
2.1.1 常用的集合符号 11
2.1.2 原型 Petri 网的定义 12
2.1.3 原型 Petri 网的性质 15
2.2 时间 Petri 网 16
2.2.1 时间 Petri 网的定义 17
2.2.2 时间 Petri 网的状态类图 18
2.3 优先级时间 Petri 网 21
2.3.1 优先级时间 Petri 网的定义 21
2.3.2 状态类图 21
2.4 模型检测 22
第3章 简化有序二叉决策图 24
3.1 布尔函数简介 24
3.1.1 布尔函数 24
3.1.2 布尔函数的其他描述形式 27
3.2 简化有序二叉决策图简介 31
3.2.1 ROBDD 的定义 31
3.2.2 ROBDD 的性质 33
3.3 ROBDD 的变量排序方法 34
3.3.1 动态变量排序法 35
3.3.2 静态变量排序法 37
3.4 基于 ROBDD 符号表达 Petri 网 41
3.4.1 基于 ROBDD 符号表达安全 Petri 网 41
3.4.2 基于 ROBDD 符号表达有界 Petri 网 49
第4章 计算树逻辑模型检测 59
4.1 计算树逻辑 59
4.1.1 CTL 的语法与语义 59
4.1.2 CTL 的标准范式 62
4.2 CTL 的传统验证方法 62
4.3 基于 ROBDD 的 CTL 验证方法 66
4.3.1 第一种符号模型检测 CTL 的方法 67
4.3.2 第二种符号模型检测 CTL 的方法 70
4.4 应用实例 73
4.4.1 柔性制造系统 73
4.4.2 多线程程序 74
4.5 实验与分析 76
4.5.1 哲学家就餐问题 77
4.5.2 资源分配系统 84
4.5.3 埃拉托色尼筛选法 86
4.5.4 n 皇后问题 89
第5章 知识 Petri 网 92
5.1 知识 Petri 网的定义 92
5.2 带有等价关系的可达图 RGER 93
5.3 基于 ROBDD 符号表达 RGER 97
第6章 知识计算树逻辑模型检测 100
6.1 知识计算树逻辑 100
6.2 基于 RGER 的 CTLK 的验证方法 102
6.3 基于 ROBDD 的 CTLK 的验证方法 108
6.3.1 第一种符号模型检测 CTLK 的方法 108
6.3.2 第二种符号模型检测 CTLK 的方法 111
6.4 应用实例：密码学家就餐协议 116
第7章 带有计时器的时间 Petri 网 127
7.1 传统的四种带有计时器的时间 Petri 网 127
7.1.1 调度扩展时间 Petri 网 127
7.1.2 抢占式时间 Petri 网 130
7.1.3 带有抑止超弧的时间 Petri 网 132
7.1.4 计时器时间 Petri 网 135
7.2 优先级时间点区间 Petri 网 138
7.2.1 优先级时间点区间 Petri 网 PToPN 的定义 138
7.2.2 PToPN 的状态图 141
第8章 时间计算树逻辑模型检测 145
8.1 时间计算树逻辑 145
8.1.1 TCTL 的语法与语义 145
8.1.2 TCTL 的标准范式 147
8.2 基于 PToPN 的 TCTL 的验证方法 148
8.3 带有时间未知数的时间计算树逻辑 155
8.3.1 TCTLx 的语法与语义 155
8.3.2 基于 PToPN 的 TCTLx 的验证方法 157
8.4 应用实例 159
8.4.1 系统描述与两个不同的网模型 159
8.4.2 基于 TCTLx 的性质规约 163
8.4.3 实验结果与分析 165
第9章 模型检测器 169
9.1 模型检测器框架概述 169
9.2 CTL 模型检测器 170
9.3 CTLK 模型检测器 173
9.4 TCTL 模型检测器 175
9.5 TCTLx 模型检测器 177
第10章 总结与展望 180
10.1 总结 180
10.2 展望 181
参考文献 183
- 科学出版社旗舰店 （微信公众号认证）
- 科学出版社秉承多年来形成的“高层次、高水平、高质量”和“严肃、严密、严格”的优良传统与作风，始终坚持为科技创新服务、为传播与普及科学知识服务、为科学家和广大读者服务的宗旨。
- 扫描二维码，访问我们的微信店铺
- 随时随地的购物、客服咨询、查询订单和物流...
