刘关俊，何雷锋，著，基于Petri网的计算树逻辑模型检测，科学出版社，2024.1

本书主要介绍原型Petri 网、知识Petri 网、带有优先级的时间Petri网，用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模，如刻画并发、选择、冲突、多方交互、多方认知过程、（抢占式）资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求，如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍使用这些Petri 网模型验证以上时序逻辑的算法。另外，本书介绍简化有序二叉决策图，介绍如何将其用于表达Petri 网的状态、状态间的迁移关系及状态间的等价关系，并将其应用于计算树逻辑与知识计算树逻辑的模型检测上。本书可供从事模型检测、Petri 网、形式化方法等理论及其应用方面的研究人员使用。