0去购物车结算
购物车中还没有商品，赶紧选购吧！
当前位置: > 基于Petri网的计算树逻辑模型检测

相同语种的商品

销售排行榜

浏览历史

基于Petri网的计算树逻辑模型检测


联系编辑
 
标题：
 
内容：
 
联系方式：
 
  
基于Petri网的计算树逻辑模型检测
  • 书号：9787030772848
    作者：刘关俊,何雷锋
  • 外文书名：
  • 装帧：平装
    开本：B5
  • 页数：198
    字数：260000
    语种：zh-Hans
  • 出版社：科学出版社
    出版时间：2024-01-01
  • 所属分类：
  • 定价： ￥108.00元
    售价： ￥85.32元
  • 图书介质:
    纸质书

  • 购买数量： 件  可供
  • 商品总价：

相同系列
全选

内容介绍

样章试读

用户评论

全部咨询

本书主要介绍原型 Petri 网、知识 Petri 网、带有优先级的时间 Petri网，用于对有限状态并发系统控制流、安全多方计算协议、多处理器抢占式实时系统等在一定层级上的抽象建模，如刻画并发、选择、冲突、多方交互、多方认知过程、（抢占式）资源分配、事件的实时性约束等。本书介绍的计算树逻辑、知识计算树逻辑、时间计算树逻辑等可以用于规约这些系统所关注的设计需求，如无死锁、公平性、隐私性、可调度性、最坏执行时间等。本书重点介绍使用这些 Petri 网模型验证以上时序逻辑的算法。另外，本书介绍简化有序二叉决策图，介绍如何将其用于表达 Petri 网的状态、状态间的迁移关系及状态间的等价关系，并将其应用于计算树逻辑与 知识计算树逻辑的模型检测上。
样章试读
  • 暂时还没有任何用户评论
总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页

全部咨询(共0条问答)

  • 暂时还没有任何用户咨询内容
总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页
用户名： 匿名用户
E-mail：
咨询内容：

目录

  • 目录
    前言
    第1章 绪论 1
    1.1 研究背景 1
    1.2 研究现状 3
    1.2.1 有限状态并发系统控制流的模型检测 3
    1.2.2 安全多方计算协议的模型检测 5
    1.2.3 多处理器抢占式实时系统的模型检测 7
    1.3 内容概述 9
    第2章 基础知识 11
    2.1 原型 Petri 网 11
    2.1.1 常用的集合符号 11
    2.1.2 原型 Petri 网的定义 12
    2.1.3 原型 Petri 网的性质 15
    2.2 时间 Petri 网 16
    2.2.1 时间 Petri 网的定义 17
    2.2.2 时间 Petri 网的状态类图 18
    2.3 优先级时间 Petri 网 21
    2.3.1 优先级时间 Petri 网的定义 21
    2.3.2 状态类图 21
    2.4 模型检测 22
    第3章 简化有序二叉决策图 24
    3.1 布尔函数简介 24
    3.1.1 布尔函数 24
    3.1.2 布尔函数的其他描述形式 27
    3.2 简化有序二叉决策图简介 31
    3.2.1 ROBDD 的定义 31
    3.2.2 ROBDD 的性质 33
    3.3 ROBDD 的变量排序方法 34
    3.3.1 动态变量排序法 35
    3.3.2 静态变量排序法 37
    3.4 基于 ROBDD 符号表达 Petri 网 41
    3.4.1 基于 ROBDD 符号表达安全 Petri 网 41
    3.4.2 基于 ROBDD 符号表达有界 Petri 网 49
    第4章 计算树逻辑模型检测 59
    4.1 计算树逻辑 59
    4.1.1 CTL 的语法与语义 59
    4.1.2 CTL 的标准范式 62
    4.2 CTL 的传统验证方法 62
    4.3 基于 ROBDD 的 CTL 验证方法 66
    4.3.1 第一种符号模型检测 CTL 的方法 67
    4.3.2 第二种符号模型检测 CTL 的方法 70
    4.4 应用实例 73
    4.4.1 柔性制造系统 73
    4.4.2 多线程程序 74
    4.5 实验与分析 76
    4.5.1 哲学家就餐问题 77
    4.5.2 资源分配系统 84
    4.5.3 埃拉托色尼筛选法 86
    4.5.4 n 皇后问题 89
    第5章 知识 Petri 网 92
    5.1 知识 Petri 网的定义 92
    5.2 带有等价关系的可达图 RGER 93
    5.3 基于 ROBDD 符号表达 RGER 97
    第6章 知识计算树逻辑模型检测 100
    6.1 知识计算树逻辑 100
    6.2 基于 RGER 的 CTLK 的验证方法 102
    6.3 基于 ROBDD 的 CTLK 的验证方法 108
    6.3.1 第一种符号模型检测 CTLK 的方法 108
    6.3.2 第二种符号模型检测 CTLK 的方法 111
    6.4 应用实例：密码学家就餐协议 116
    第7章 带有计时器的时间 Petri 网 127
    7.1 传统的四种带有计时器的时间 Petri 网 127
    7.1.1 调度扩展时间 Petri 网 127
    7.1.2 抢占式时间 Petri 网 130
    7.1.3 带有抑止超弧的时间 Petri 网 132
    7.1.4 计时器时间 Petri 网 135
    7.2 优先级时间点区间 Petri 网 138
    7.2.1 优先级时间点区间 Petri 网 PToPN 的定义 138
    7.2.2 PToPN 的状态图 141
    第8章 时间计算树逻辑模型检测 145
    8.1 时间计算树逻辑 145
    8.1.1 TCTL 的语法与语义 145
    8.1.2 TCTL 的标准范式 147
    8.2 基于 PToPN 的 TCTL 的验证方法 148
    8.3 带有时间未知数的时间计算树逻辑 155
    8.3.1 TCTLx 的语法与语义 155
    8.3.2 基于 PToPN 的 TCTLx 的验证方法 157
    8.4 应用实例 159
    8.4.1 系统描述与两个不同的网模型 159
    8.4.2 基于 TCTLx 的性质规约 163
    8.4.3 实验结果与分析 165
    第9章 模型检测器 169
    9.1 模型检测器框架概述 169
    9.2 CTL 模型检测器 170
    9.3 CTLK 模型检测器 173
    9.4 TCTL 模型检测器 175
    9.5 TCTLx 模型检测器 177
    第10章 总结与展望 180
    10.1 总结 180
    10.2 展望 181
    参考文献 183
帮助中心
公司简介
联系我们
常见问题
新手上路
发票制度
积分说明
购物指南
配送方式
配送时间及费用
配送查询说明
配送范围
快递查询
售后服务
退换货说明
退换货流程
投诉或建议
版权声明
经营资质
营业执照
出版社经营许可证

中国科技出版传媒股份有限公司　版权所有

　

京ICP备14028887号-5　 京ICP证150976号 京公网安备 11010102004214号

北京东黄城根北街16号 邮编：100717 Email:webmaster@mail.sciencep.com