基于Petri网的计算树逻辑模型检测

本书主要介绍原型Petri网、知识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.1ROBDD的定义31
3.2.2ROBDD的性质33
3.3ROBDD的变量排序方法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.1CTL的语法与语义59
4.1.2CTL的标准范式62
4.2CTL的传统验证方法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.4n皇后问题89
第5章知识Petri网92
5.1知识Petri网的定义92
5.2带有等价关系的可达图RGER93
5.3基于ROBDD符号表达RGER97
第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.2PToPN的状态图141
第8章时间计算树逻辑模型检测145
8.1时间计算树逻辑145
8.1.1TCTL的语法与语义145
8.1.2TCTL的标准范式147
8.2基于PToPN的TCTL的验证方法148
8.3带有时间未知数的时间计算树逻辑155
8.3.1TCTLx的语法与语义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.2CTL模型检测器170
9.3CTLK模型检测器173
9.4TCTL模型检测器175
9.5TCTLx模型检测器177
第10章总结与展望180
10.1总结180
10.2展望181
参考文献183