扫一扫
关注中图网
官方微博
本类五星书更多>
-
>
湖南省志(1978-2002)?铁路志
-
>
公路车宝典(ZINN的公路车维修与保养秘籍)
-
>
晶体管电路设计(下)
-
>
基于个性化设计策略的智能交通系统关键技术
-
>
德国克虏伯与晚清火:贸易与仿制模式下的技术转移
-
>
花样百出:贵州少数民族图案填色
-
>
识木:全球220种木材图鉴
反应式和并发系统的时序逻辑 版权信息
- ISBN：9787302644972
- 条形码：9787302644972 ; 978-7-302-64497-2
- 装帧：平装-胶订
- 册数：暂无
- 重量：暂无
- 所属分类：>
反应式和并发系统的时序逻辑 本书特色
本书全面介绍了时序逻辑和作者开发的反应式程序的计算模型，是该领域的经典和权威著作。
反应式和并发系统的时序逻辑 内容简介
反应式和并发系统指实时运行的计算系统，如操作系统、控制系统、交互系统和并发系统。这些系统很难规约、实现和验证，主要原因是系统与其环境之间及系统本身的并行进程之间交互的复杂性，在交互时间上的微小变化可能导致接近不同的行为。 时序逻辑是一种形式化规约语言，可用于刻画和分析反应式系统中有关时间和行为方面的属性。它提供了一种简单、自然但准确的方式来讨论交互发生的顺序，而无须采用绝对时间度量。 本书全面介绍了时序逻辑和作者开发的反应式程序的计算模型。 本书是国际有名计算机科学家Zohar Manna和Amir Pnueli（图灵奖得主）的代表作，适合作为计算机、软件工程、人工智能、自动化等专业高年级本科生、研究生的教材或参考书，也可供相关领域的研究人员和技术开发人员参考。
反应式和并发系统的时序逻辑 目录
第Ⅰ部分并 发 模 型 第1章基本模型 1.1通用模型 1.1.1基础语言 1.1.2基本转换系统 1.1.3转换关系ρτ 1.1.4使能与非使能转换 1.1.5空转换与勤勉转换 1.1.6计算 1.1.7具体模型 1.2模型1： 转换图 1.2.1声明 1.2.2进程 1.2.3基本转换系统图 1.2.4用交错表示并发性 1.2.5调度 1.3模型2： 共享变量文本 1.3.1简单语句 1.3.2复合语句 1.3.3程序 1.3.4文本程序中的标记 1.3.5标记等价关系 1.3.6文本语言中的位置 1.4共享变量文本语义 1.4.1状态变量和状态 1.4.2转换 1.4.3初始条件 1.4.4计算 1.4.5下标变量 1.5语句间的结构关系 1.5.1子语句 1.5.2控制谓词at、after和in 1.5.3语句的使能性 1.5.4进程和并行语句 1.5.5竞争语句 1.6行为等价 1.6.1初步近似 1.6.2可观测和可简化的行为 1.6.3转换系统的等价性 1.6.4语句一致性 1.6.5例子 1.6.6模拟与实现 1.7分组语句 1.7.1分组语句 1.7.2与分组语句关联的转换 1.8信号量语句 1.8.1信号量需求 1.8.2信号量语句 1.8.3互斥信号量的应用 1.8.4信号量的其他应用 1.9区域语句 1.9.1比较信号量和区域语句 1.9.2选择语句中的同步 1.10模型3： 消息传递文本 1.10.1通信语句 1.10.2缓冲能力 1.10.3例子 1.10.4条件通信语句 1.10.5同步模型和异步模型的比较 1.10.6公平服务器 1.11模型4： Petri网 1.11.1网 1.11.2标记 1.11.3图形化表示 1.11.4点火 1.11.5Petri系统 1.11.6例子 问题 文献注释 第2章真并发模型 2.1交错和并发 2.1.1重叠执行 2.1.2交错计算 2.1.3细粒度 2.2限制临界引用 2.2.1临界引用 2.2.2语句的LCR约束 2.2.3LCR程序 2.2.4需要额外保护 2.2.5每个程序都有一个LCR精化 2.2.6每个程序都有一个LCR等价 2.2.7语义临界引用 2.2.8合并语句 2.2.9with语句 2.3弱公平性 2.3.1公平性需求 2.3.2不公平计算 2.3.3弱公平性 2.3.4弱公平性需求 2.4弱公平性需求的含义 2.4.1不能保证选择公平性 2.4.2转换弱公平性与进程弱公平性 2.4.3弱公平性调度 2.4.4不能检测弱公平性 2.4.5非公平转换 2.5强公平性 2.5.1弱公平性不足 2.5.2强公平性需求 2.5.3强公平性调度 2.6同步语句 2.7通信语句 2.7.1同步通信互斥 2.7.2异步通信互斥 2.8总结: 公平转换系统 2.9Petri网公平性 2.9.1弱公平性 2.9.2非一元网转换的强公平性 2.9.3互斥 2.10公平性语义 2.10.1公平性防止有限区分 2.10.2公平性和随机选择 问题 文献注释 第Ⅱ部分规约 第3章时序逻辑 3.1状态公式 3.1.1状态语言 3.1.2状态公式语义 3.2时序公式： 将来算子 3.3时序公式： 过去算子 3.3.1简单例子 3.3.2可满足性和有效性 3.3.3等价性、一致性和蕴涵性 3.3.4可替换性 3.3.5过去公式和将来公式 3.3.6的较弱形式 3.3.7算子的基本集合 3.3.8限制型算子 3.4时序算子的基本属性 3.4.1模式及其有效性 3.4.2单调性 3.4.3自反性 3.4.4限制性 3.4.5扩展性 3.4.6对偶性 3.4.7强算子和弱算子 3.4.8幂等性 3.4.9吸收性 3.4.10上一时刻和下一时刻的交换性 3.4.11全称算子和存在算子 3.4.12引用变量的下一个值和前一个值 3.4.13语义弱公平性 3.5证明系统 3.6证明系统公理 3.6.1将来公理 3.6.2过去公理 3.6.3混合公理 3.6.4状态重言式公理 3.7基本推理规则 3.7.1泛化规则和特指规则 3.7.2替换规则 3.7.3分离规则 3.8导出规则 3.8.1指定规则 3.8.2命题推理规则 3.8.3蕴涵分离规则 3.8.4蕴涵命题推理规则 3.8.5从蕴涵到规则 3.8.6证明举例 3.9等词和量词 3.9.1参数化的句子符号 3.9.2带参数模式的规则GEN 3.9.3带量词公式的规则INST 3.9.4变量替换 3.9.5等词公理 3.9.6框架公理 3.9.7证明举例 3.9.8变量的下一个值和前一个值 3.9.9量词公理 3.9.10量词规则 3.9.11证明举例 3.10从一般有效性到程序有效性 3.10.1计算对应的模型 3.10.2程序有效性和状态有效性 3.10.3扩展演绎系统 3.10.4建立P状态有效性 3.10.5建立P有效性 3.10.6程序依赖规则 3.10.7导出规则 3.10.8时序语义公理 问题 文献注释
第4章程序属性 4.1局部语言 4.1.1位置谓词 4.1.2转换的使能性 4.1.3终止谓词 4.1.4转换谓词 4.1.5通信谓词 4.1.6规约变量 4.2属性分类 4.2.1安全性 4.2.2保证性 4.2.3义务性 4.2.4响应性 4.2.5持续性 4.2.6反应性 4.2.7反应性类是*大的类 4.2.8分类 4.2.9标准公式 4.2.10安全性活性分类 4.3安全性例子： 状态不变性 4.3.1全局不变性 4.3.2部分正确性 4.3.3无死锁性 4.3.4局部无死锁性 4.3.5容错性 4.3.6互斥性 4.3.7通信事件的不变性 4.4安全性例子： 过去不变性 4.4.1单调性 4.4.2缺乏主动响应 4.4.3无重复输出 4.4.4先进先出 4.4.5严格优先性 4.4.6有界超越 4.5进展性例子： 从保证性到反应性 4.5.1终止性和完全正确性 4.5.2保证性事件 4.5.3间歇断言 4.5.4无个体饥荒和无活锁 4.5.5可访问性 4.5.6确保响应 4.5.7*终有界性 4.5.8表示公平性需求 4.5.9*终可靠性 4.6例子： 资源分配 4.6.1消息传递方式 4.6.2消息传递方式的安全性 4.6.3消息传递方式的进展性 4.6.4共享变量方式 4.6.5共享变量方式的安全性 4.6.6共享变量方式的进展性 4.7规约语言表达能力 4.7.1观察奇偶性 4.7.2量词公式描述奇偶性 4.7.3有重复输入的缓冲 4.7.4量词公式描述缓冲 4.7.5通信历史变量 4.8反应模块规约 4.8.1模块语句 4.8.2模块规约 4.8.3执行模块的任务 4.8.4模块实现的障碍 4.8.5模块的计算 4.9复合模块规约 4.9.1层次分解 4.9.2更改超越一次的变量 4.9.3分解安全性规约 4.9.4异步通信模块 4.9.5同步通信模块 4.9.6资源重新分配 问题 文献注释
参考文献
展开全部
书友推荐
- >
罗庸西南联大授课录
罗庸西南联大授课录
¥17.6¥32.0 - >
上帝之肋:男人的真实旅程
上帝之肋:男人的真实旅程
¥19.3¥35.0 - >
推拿
推拿
¥12.2¥32.0 - >
朝闻道
朝闻道
¥10.2¥23.8 - >
龙榆生：词曲概论/大家小书
龙榆生：词曲概论/大家小书
¥9.9¥24.0 - >
中国历史的瞬间
中国历史的瞬间
¥14.8¥38.0 - >
伊索寓言-世界文学名著典藏-全译本
伊索寓言-世界文学名著典藏-全译本
¥6.1¥19.0 - >
李白与唐代文化
李白与唐代文化
¥10.4¥29.8
本类畅销
-
黑科技驱动世界的100项技术
¥21.9¥69.8 -
黑科技:驱动世界的100项技术(八品)
¥21.9¥69.8 -
指火控弹道与射击诸元理论
¥38.7¥49 -
智能照明工程手册
¥29.9¥49.8 -
光电直读光谱分析技术与应用
¥38.7¥49 -
服务型制造
¥76.3¥109
