机读格式显示(MARC)

• 000 01863nam0 2200277 450

• 001 0000359038

• 005 20240925104000.0

• 010 __ |a 978-7-03-077284-8 |d CNY108.00

• 100 __ |a 20240115d2024 em y0chiy50 ea

• 101 0_ |a chi

• 102 __ |a CN |b 110000

• 105 __ |a ak a 000yy

• 106 __ |a r

• 200 1_ |a 基于Petri网的计算树逻辑模型检测 |A ji yu Petri wang de ji suan shu luo ji mo xing jian ce |f 刘关俊, 何雷锋著

• 210 __ |a 北京 |c 科学出版社 |d 2024.1

• 215 __ |a 195页 |c 图 |d 24cm

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

• 320 __ |a 有书目 (第183-195页)

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

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

• 606 0_ |a 计算机科学 |A ji suan ji ke xue |x 研究

• 690 __ |a TP3 |v 5

• 701 _0 |a 刘关俊 |A liu guan jun |4 著

• 701 _0 |a 何雷锋 |A he lei feng |4 著

• 801 _0 |a CN |b GDPTC |c 20240925

• 905 __ |a GDPTC |d TP3/959