内容推荐 本书主要介绍原型Petri网、知识Petri网、带有优先级的时间Petri网,用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模,如刻画并发、选择、冲突、多方交互、多方认知过程、(抢占式)资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求,如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍使用这些Petri网模型验证以上时序逻辑的算法。另外,本书介绍简化有序二叉决策图,介绍如何将其用于表达Petri网的状态、状态间的迁移关系及状态间的等价关系,并将其应用于计算树逻辑与知识计算树逻辑的模型检测上。 本书可供从事模型检测、Petri网、形式化方法等理论及其应用方面的研究人员使用。 作者简介 刘关俊,男,教授,博士生导师。2011年获得同济大学计算机软件与理论专业博士学位,同年赴新加坡科技设计大学从事博士后研究工作;2013年回国,并进入同济大学计算机科学系任教,同年获得德国洪堡基金资助,赴柏林洪堡大学从事博士后研究工作。 主要从事形式化方法、模型检测、Petri网等方面的理论与应用研究,目前也从事机器学习及其在网络交易欺诈检测方面的研究。已出版学术专著1本,发表学术论文90余篇,包括Science China Information Sciences、ACM Transactions on Embedded Computing Systems、ACM Transactionson Cyber-Physical Systems、IEEE Transactions on Services Computing、IEEE Transactions on Industrial Informatics等期刊论文近50篇,以及国际Petri网年会(International Conference on Application and Theory of Petri Nets and Concurrency)等会议论文40余篇。 刘关俊主持国家自然科学基金面上项目与青年基金项目、上海市曙光计划人才项目、中央高校交叉项目(重大)等多项,获得国家科技进步奖二等奖、上海市科技进步奖一等奖、中国电子学会自然科学一等奖、吴文俊人工智能技术发明奖一等奖、上海市优秀博士论文奖以及首届教育部国务院学位委员会博士研究生学术新人奖等。刘关俊是中国计算机学会形式化方法专委会委员、中国自动化学会网络信息服务专委会委员、中国人工智能学会智能空天系统专委会委员、IEEESenior Member。 目录 前言 第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 展望 参考文献 |