反应式和并发系统指实时运行的计算系统，如操作系统、控制系统、交互系统和并发系统。这些系统很难规约、实现和验证，主要原因是系统与其环境之间及系统本身的并行进程之间交互的复杂性，在交互时间上的微小变化可能导致完全不同的行为。 时序逻辑是一种形式化规约语言，可用于刻画和分析反应式系统中有关时间和行为方面的属性。它提供了一种简单、自然但精确的方式来讨论交互发生的顺序，而无须采用绝对时间度量。本书全面介绍了时序逻辑和作者开发的反应式程序的计算模型。 本书是国际著名计算机科学家Zohar Manna和Amir Pnueli（图灵奖得主）的代表作，适合作为计算机、软件工程、人工智能、自动化等专业高年级本科生、研究生的教材或参考书，也可供相关领域的研究人员和技术开发人员参考。

第Ⅰ部分 并发模型
第1章 基本模型
1.1 通用模型
1.1.1 基础语言
1.1.2 基本转换系统
1.1.3 转换关系pι
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.5 Petri系统
1.11.6 例子
问题
文献注释
第2章 真并发模型
2.1 交错和并发
2.1.1 重叠执行
2.1.2 交错计算
2.1.3 细粒度
2.2 限制临界引用
……
第Ⅱ部分 规约
参考文献