基于Petri网的计算树逻辑模型检测
正版保障 假一赔十 电子发票
¥
70.19
6.5折
¥
108
全新
库存4件
作者刘关俊, 何雷锋著
出版社科学出版社
ISBN9787030772848
出版时间2024-01
装帧平装
开本其他
定价108元
货号4531538
上书时间2024-12-30
商品详情
- 品相描述:全新
- 商品描述
-
目录
本书主要介绍原型Petri网、知识Petri网、带有优先级的时间Petri网, 用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模, 如刻画并发、选择、冲突、多方交互、多方认知过程、(抢占式) 资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求, 如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍在网模型之上的针对这些时序逻辑的模型检测算法。另外, 本书介绍简化有序二叉决策图, 介绍如何将其用于表达Petri网的状态、状态间的迁移关系及状态间的等价关系, 并将其应用于计算树逻辑与知识计算树逻辑的模型检测上。
内容摘要
本书主要介绍原型Petri网、知识Petri网、带有优先级的时间Petri网,用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模,如刻画并发、选择、冲突、多方交互、多方认知过程、(抢占式)资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求,如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍使用这些Petri网模型验证以上时序逻辑的算法。另外,本书介绍简化有序二叉决策图,介绍如何将其用于表达Petri网的状态、状态间的迁移关系及状态间的等价关系,并将其应用于计算树逻辑与知识计算树逻辑的模型检测上。本书可供从事模型检测、Petri网、形式化方法等理论及其应用方面的研究人员使用。
— 没有更多了 —
以下为对购买帮助不大的评价