广东职业技术学院图书馆书目检索系统

Online Public Access Catalogue

题名/责任者:

基于Petri网的计算树逻辑模型检测/刘关俊, 何雷锋著

出版发行项:

北京:科学出版社,2024.1

ISBN及定价:

978-7-03-077284-8/CNY108.00

载体形态项:

195页:图;24cm

个人责任者:

刘关俊 著

个人责任者:

何雷锋 著

学科主题:

计算机科学-研究

中图法分类号:

TP3

责任者附注:

刘关俊, 同济大学教授, 博士生导师。2011年7月毕业于同济大学计算机软件与理论专业, 获得工学博士学位, 同年赴新加坡科技设计大学从事博士后工作, 2013年进入同济大学计算机科学系工作, 随后受德国洪堡基金资助于洪堡大学从事第二个博士后工作。主要从事形式化方法、Petri网、模型检测等方面的理论与应用研究。何雷锋, 2023年1月获得同济大学计算机科学与技术专业博士学位。主要从事Petri网、计算树逻辑、模型检测等方面的理论与应用研究。

书目附注:

有书目 (第183-195页)

提要文摘附注:

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

使用对象附注:

本书可供从事模型检测、Petri网、形式化方法等理论及其应用方面的研究人员使用

豆瓣简介：