|
000
|
01767nam0 2200265 450
|
|
001
|
2442080658
|
|
010
|
|
@a978-7-03-077284-8@dCNY108.00
|
|
100
|
|
@a20240115d2024 em y0chiy0120 ea
|
|
101
|
0
|
@achi
|
|
102
|
|
@aCN@b110000
|
|
105
|
|
@aak a 000yy
|
|
106
|
|
@ar
|
|
200
|
1
|
@a基于Petri网的计算树逻辑模型检测@Aji yu Petri wang de ji suan shu luo ji mo xing jian ce@f刘关俊, 何雷锋著
|
|
210
|
|
@a北京@c科学出版社@d2024.01
|
|
215
|
|
@a195页@c图@d24cm
|
|
314
|
|
@a刘关俊, 同济大学教授, 博士生导师。2011年7月毕业于同济大学计算机软件与理论专业, 获得工学博士学位, 同年赴新加坡科技设计大学从事博士后工作, 2013年进入同济大学计算机科学系工作, 随后受德国洪堡基金资助于洪堡大学从事第二个博士后工作。主要从事形式化方法、Petri网、模型检测等方面的理论与应用研究。何雷锋, 2023年1月获得同济大学计算机科学与技术专业博士学位。主要从事Petri网、计算树逻辑、模型检测等方面的理论与应用研究。
|
|
320
|
|
@a有书目 (第183-195页)
|
|
330
|
|
@a本书主要介绍原型Petri网、知识Petri网、带有优先级的时间Petri网, 用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模, 如刻画并发、选择、冲突、多方交互、多方认知过程、(抢占式) 资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求, 如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍在网模型之上的针对这些时序逻辑的模型检测算法。另外, 本书介绍简化有序二叉决策图, 介绍如何将其用于表达Petri网的状态、状态间的迁移关系及状态间的等价关系, 并将其应用于计算树逻辑与知识计算树逻辑的模型检测上。
|
|
586
|
|
@a
|
|
606
|
0
|
@a计算机科学@Aji suan ji ke xue@x研究
|
|
690
|
|
@aTP3@v5
|
|
701
|
0
|
@a刘关俊@Aliu guan jun@4著
|
|
701
|
0
|
@a何雷锋@Ahe lei feng@4著
|
|
801
|
0
|
@aCN@c20240115
|
|
905
|
|
@dTP3@eL612@f1@sTP3/L612@S@Z
|
|
|
|
|
| |
| 基于Petri网的计算树逻辑模型检测/刘关俊, 何雷锋著.-北京：科学出版社，2024.01 |
| 195页：图；24cm |
| |
| |
| ISBN 978-7-03-077284-8：CNY108.00 |
| 本书主要介绍原型Petri网、知识Petri网、带有优先级的时间Petri网, 用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模, 如刻画并发、选择、冲突、多方交互、多方认知过程、(抢占式) 资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求, 如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍在网模型之上的针对这些时序逻辑的模型检测算法。另外, 本书介绍简化有序二叉决策图, 介绍如何将其用于表达Petri网的状态、状态间的迁移关系及状态间的等价关系, 并将其应用于计算树逻辑与知识计算树逻辑的模型检测上。 |
| ● |
正题名：基于Petri网的计算树逻辑模型检测
索取号：TP3/L612
预约/预借
| 序号
|
登录号
|
条形码
|
馆藏地/架位号
|
状态
|
备注
|
|
1
|
21617262
|
216172629
|
自科库301/301自科库 100排2列6层/
[索取号:TP3/L612]
|
在馆
|
|
