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

定　　价：108 元

• 作者：刘关俊，何雷锋
• 出版时间：2024/1/1
• ISBN：9787030772848
• 出 版 社：科学出版社

• 中图法分类：TP3 
• 页码：208
• 版次：31
• 开本：B5

内容简介

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

更多科学出版社服务，请扫码获取。