基于PETRI网的计算树逻辑模型检测9787030772848
正版图书，可开发票，请放心购买。
￥ 72.58 6.7折 ￥ 108 全新
库存13件
广东广州
认证卖家担保交易快速发货售后保障
作者刘关俊，何雷锋著
出版社科学出版社
ISBN9787030772848
出版时间2024-01
装帧平装
开本其他
定价108元
货号14835647
上书时间2024-08-19
- 店主推荐
- 最新上架
商品详情
- 品相描述：全新
- 商品描述
-
目录
目录
前言
第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
内容摘要
本书主要介绍原型Petri网、知识Petri网、带有优先级的时间Petri网，用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模，如刻画并发、选择、冲突、多方交互、多方认知过程、（抢占式）资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求，如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍使用这些Petri网模型验证以上时序逻辑的算法。另外，本书介绍简化有序二叉决策图，介绍如何将其用于表达Petri网的状态、状态间的迁移关系及状态间的等价关系，并将其应用于计算树逻辑与知识计算树逻辑的模型检测上。本书可供从事模型检测、Petri网、形式化方法等理论及其应用方面的研究人员使用。
精彩内容
本书介绍了基于Petri网的计算数逻辑模型检测方法，主要内容分为以下三个部分：一、基于原型Petri网的计算树逻辑（CTL）模型检测，结合OBDD技术提出了一种更高效的验证方法以缓解它的状态爆炸问题；二、对多智能体系统的正确性验证，提出了带有认知的Petri网，模拟多智能体系统，然后结合OBDD技术提出了一种更高效的验证计算树认知逻辑（CTLK）的方法；三、对实时系统的正确性验证，提出了点区间优先级时间Petri网，模拟抢占式实时系统，如多核多任务实时系统，并由此给出了一种验证时间计算树逻辑（TCTL）的方法。同时介绍了我们开发的模型检测工具，并针对一些应用实例，展示了我们的模型与检测算法的优点。
— 没有更多了 —
以下为对购买帮助不大的评价