扫一扫
关注中图网
官方微博
本类五星书更多>
-
>
决战行测5000题(言语理解与表达)
-
>
软件性能测试.分析与调优实践之路
-
>
第一行代码Android
-
>
深度学习
-
>
Unreal Engine 4蓝图完全学习教程
-
>
深入理解计算机系统-原书第3版
-
>
Word/Excel PPT 2013办公应用从入门到精通-(附赠1DVD.含语音视频教学+办公模板+PDF电子书)
基于PETRI网的计算树逻辑模型检测 版权信息
- ISBN：9787030772848
- 条形码：9787030772848 ; 978-7-03-077284-8
- 装帧：平装胶订
- 册数：暂无
- 重量：暂无
- 所属分类：>
基于PETRI网的计算树逻辑模型检测 本书特色
介绍了我们开发的模型检测工具，并针对一些应用实例，展示了我们的模型与检测算法的优点。
基于PETRI网的计算树逻辑模型检测 内容简介
本书介绍了基于Petri网的计算数逻辑模型检测方法，主要内容分为以下三个部分：一、基于原型Petri网的计算树逻辑（CTL）模型检测，结合OBDD技术提出了一种更高效的验证方法以缓解它的状态爆炸问题；二、对多智能体系统的正确性验证，提出了带有认知的Petri网，模拟多智能体系统，然后结合OBDD技术提出了一种更高效的验证计算树认知逻辑（CTLK）的方法；三、对实时系统的正确性验证，提出了点区间优先级时间Petri网，模拟抢占式实时系统，如多核多任务实时系统，并由此给出了一种验证时间计算树逻辑（TCTL）的方法。同时介绍了我们开发的模型检测工具，并针对一些应用实例，展示了我们的模型与检测算法的优点。
基于PETRI网的计算树逻辑模型检测 目录
前言
第1章 绪论
1.1 研究背景
1.2 研究现状
1.2.1 有限状态并发系统控制流的模型检测
1.2.2 安全多方计算协议的模型检测
1.2.3 多处理器抢占式实时系统的模型检测
1.3 内容概述
第2章 基础知识
2.1 原型Petri网
2.1.1 常用的集合符号
2.1.2 原型Petri网的定义
2.1.3 原型Petri网的性质
2.2 时间Petri网
2.2.1 时间Petri网的定义
2.2.2 时间Petri网的状态类图
2.3 优先级时间Petri网
2.3.1 优先级时间Petri网的定义
2.3.2 状态类图
2.4 模型检测
第3章 简化有序二叉决策图
3.1 布尔函数简介
3.1.1 布尔函数
3.1.2 布尔函数的其他描述形式
3.2 简化有序二叉决策图简介
3.2.1 ROBDD的定义
3.2.2 ROBDD的性质
3.3 ROBDD的变量排序方法
3.3.1 动态变量排序法
3.3.2 静态变量排序法
3.4 基于ROBDD符号表达Petri网
3.4.1 基于ROBDD符号表达安全Petri网
3.4.2 基于ROBDD符号表达有界Petri网
第4章 计算树逻辑模型检测
4.1 计算树逻辑
4.1.1 CTL的语法与语义
4.1.2 CTL的标准范式
4.2 CTL的传统验证方法
4.3 基于ROBDD的CTL验证方法
4.3.1 **种符号模型检测CTL的方法
4.3.2 第二种符号模型检测CTL的方法
4.4 应用实例
4.4.1 柔性制造系统
4.4.2 多线程程序
4.5 实验与分析
4.5.1 哲学家就餐问题
4.5.2 资源分配系统
4.5.3 埃拉托色尼筛选法
4.5.4 n皇后问题
第5章 知识Petri网
5.1 知识Petri网的定义
5.2 带有等价关系的可达图RGER
5.3 基于ROBDD符号表达RGER
第6章 知识计算树逻辑模型检测
6.1 知识计算树逻辑
6.2 基于RGER的CTLK的验证方法
6.3 基于ROBDD的CTLK的验证方法
6.3.1 **种符号模型检测CTLK的方法
6.3.2 第二种符号模型检测CTLK的方法
6.4 应用实例：密码学家就餐协议
第7章 带有计时器的时间Petri网
7.1 传统的四种带有计时器的时间Petri网
7.1.1 调度扩展时间Petri网
7.1.2 抢占式时间Petri网
7.1.3 带有抑止超弧的时间Petri网
7.1.4 计时器时间Petri网
7.2 优先级时间点区间Petri网
7.2.1 优先级时间点区间Petri网PToPN的定义
7.2.2 PToPN的状态图
第8章 时间计算树逻辑模型检测
8.1 时间计算树逻辑
8.1.1 TCTL的语法与语义
8.1.2 TCTL的标准范式
8.2 基于 PToPN的TCTL的验证方法
8.3 带有时间未知数的时间计算树逻辑
8.3.1 TCTLx的语法与语义
8.3.2 基于PToPN的TCTLx的验证方法
8.4 应用实例
8.4.1 系统描述与两个不同的网模型
8.4.2 基于TCTLx的性质规约
8.4.3 实验结果与分析
第9章 模型检测器
9.1 模型检测器框架概述
9.2 CTL模型检测器
9.3 CTLK模型检测器
9.4 TCTL模型检测器
9.5 TCTLx模型检测器
第10章 总结与展望
10.1 总结
10.2 展望
参考文献
展开全部
基于PETRI网的计算树逻辑模型检测 作者简介
刘关俊，男，教授，博士生导师。2011年获得同济大学计算机软件与理论专业博士学位，同年赴新加坡科技设计大学从事博士后研究工作；2013年回国，并进入同济大学计算机科学系任教，同年获得德国洪堡基金资助，赴柏林洪堡大学从事博士后研究工作。 主要从事形式化方法、模型检测、Petri网等方面的理论与应用研究，目前也从事机器学习及其在网络交易欺诈检测方面的研究。已出版学术专著1本，发表学术论文90余篇，包括Science China Information Sciences、ACM Transactions on Embedded Computing Systems、ACM Transactionson Cyber-Physical Systems、IEEE Transactions on Services Computing、IEEE Transactions on Industrial Informatics等期刊论文近50篇，以及国际Petri网年会（International Conference on Application and Theory of Petri Nets and Concurrency）等会议论文40余篇。 刘关俊主持国家自然科学基金面上项目与青年基金项目、上海市曙光计划人才项目、中央高校交叉项目（重大）等多项，获得国家科技进步奖二等奖、上海市科技进步奖一等奖、中国电子学会自然科学一等奖、吴文俊人工智能技术发明奖一等奖、上海市优秀博士论文奖以及首届教育部国务院学位委员会博士研究生学术新人奖等。刘关俊是中国计算机学会形式化方法专委会委员、中国自动化学会网络信息服务专委会委员、中国人工智能学会智能空天系统专委会委员、IEEESenior Member。 何雷锋，2023年1月获得同济大学计算机科学与技术专业博士学位。何雷锋主要从事Petri网、计算树逻辑、模型检测等方面的理论与应用研究。在《软件学报》、IEEE Transactions on Industrial Informatics、IEEE Transactions on Computational Social Systems等国内外期刊上发表学术论文10余篇，开发了（符号）模型检测工具。
书友推荐
- >
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
¥6.3¥14.0 - >
山海经
山海经
¥20.4¥68.0 - >
伊索寓言-世界文学名著典藏-全译本
伊索寓言-世界文学名著典藏-全译本
¥6.1¥19.0 - >
莉莉和章鱼
莉莉和章鱼
¥16.0¥42.0 - >
月亮与六便士
月亮与六便士
¥13.4¥42.0 - >
名家带你读鲁迅:朝花夕拾
名家带你读鲁迅:朝花夕拾
¥10.5¥21.0 - >
诗经-先民的歌唱
诗经-先民的歌唱
¥15.1¥39.8 - >
新文学天穹两巨星--鲁迅与胡适/红烛学术丛书(红烛学术丛书)
新文学天穹两巨星--鲁迅与胡适/红烛学术丛书(红烛学术丛书)
¥9.9¥23.0
本类畅销
-
”互联网+“时代计算机算法的应用及其实践研究
¥19.9¥59 -
微服务设计
¥52.8¥69 -
图说深度学习:用可视化方法理解复杂概念
¥109¥188 -
计算机基础
¥17.2¥31 -
改变未来的九大算法
¥50¥68 -
生成式AI入门与AWS实战
¥77.8¥99.8
