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

前言 第1章 绪论 1.1 研究背景 1.2 研究现状 1.2.1 有限状态并发系统控制流的模型检测 1.2.2 安全多方计算协议的模型检测 1.2.3 多处理器抢占式实时系统的模型检测 1.3 内容概述 第2章 基础知识 2.1 原型Petri网 2.1.1 常用的集合符号 2.1.2 原型Petri网的定义 2.1.3 原型Petri网的性质 2.2 时间Petri网 2.2.1 时间Petri网的定义 2.2.2 时间Petri网的状态类图 2.3 优先级时间Petri网 2.3.1 优先级时间Petri网的定义 2.3.2 状态类图 2.4 模型检测 第3章 简化有序二叉决策图 3.1 布尔函数简介 3.1.1 布尔函数 3.1.2 布尔函数的其他描述形式 3.2 简化有序二叉决策图简介 3.2.1 ROBDD的定义 3.2.2 ROBDD的性质 3.3 ROBDD的变量排序方法 3.3.1 动态变量排序法 3.3.2 静态变量排序法 3.4 基于ROBDD符号表达Petri网 3.4.1 基于ROBDD符号表达安全Petri网 3.4.2 基于ROBDD符号表达有界Petri网 第4章 计算树逻辑模型检测 4.1 计算树逻辑 4.1.1 CTL的语法与语义 4.1.2 CTL的标准范式 4.2 CTL的传统验证方法 4.3 基于ROBDD的CTL验证方法 4.3.1 **种符号模型检测CTL的方法 4.3.2 第二种符号模型检测CTL的方法 4.4 应用实例 4.4.1 柔性制造系统 4.4.2 多线程程序 4.5 实验与分析 4.5.1 哲学家就餐问题 4.5.2 资源分配系统 4.5.3 埃拉托色尼筛选法 4.5.4 n皇后问题 第5章 知识Petri网 5.1 知识Petri网的定义 5.2 带有等价关系的可达图RGER 5.3 基于ROBDD符号表达RGER 第6章 知识计算树逻辑模型检测 6.1 知识计算树逻辑 6.2 基于RGER的CTLK的验证方法 6.3 基于ROBDD的CTLK的验证方法 6.3.1 **种符号模型检测CTLK的方法 6.3.2 第二种符号模型检测CTLK的方法 6.4 应用实例：密码学家就餐协议 第7章 带有计时器的时间Petri网 7.1 传统的四种带有计时器的时间Petri网 7.1.1 调度扩展时间Petri网 7.1.2 抢占式时间Petri网 7.1.3 带有抑止超弧的时间Petri网 7.1.4 计时器时间Petri网 7.2 优先级时间点区间Petri网 7.2.1 优先级时间点区间Petri网PToPN的定义 7.2.2 PToPN的状态图 第8章 时间计算树逻辑模型检测 8.1 时间计算树逻辑 8.1.1 TCTL的语法与语义 8.1.2 TCTL的标准范式 8.2 基于 PToPN的TCTL的验证方法 8.3 带有时间未知数的时间计算树逻辑 8.3.1 TCTLx的语法与语义 8.3.2 基于PToPN的TCTLx的验证方法 8.4 应用实例 8.4.1 系统描述与两个不同的网模型 8.4.2 基于TCTLx的性质规约 8.4.3 实验结果与分析 第9章 模型检测器 9.1 模型检测器框架概述 9.2 CTL模型检测器 9.3 CTLK模型检测器 9.4 TCTL模型检测器 9.5 TCTLx模型检测器 第10章 总结与展望 10.1 总结 10.2 展望 参考文献