时序逻辑（Temporal Logic）

时序逻辑是一种扩展了经典逻辑的形式系统，它引入了描述时间流逝的模态算子，使人们能够表达诸如某事最终会发生、某事永远保持成立这类与时间相关的断言，是刻画动态系统行为的重要工具。

概述

时序逻辑源于哲学逻辑对时态命题的研究，由阿瑟·普赖尔（Arthur Prior）奠基。阿米尔·普努埃利（Amir Pnueli）于1977年将其引入计算机科学，用来规约和验证并发程序的性质，并因此获得图灵奖。它成为形式化验证不可或缺的规约语言。

核心特点

• 时序算子：包括总是、最终、直到、下一步等，用来描述性质在时间轴上的分布。
• 线性时序逻辑：假设时间是一条单一的线，每个时刻只有唯一后继，适合描述单条执行路径的性质。
• 计算树逻辑：把时间看作分叉的树，允许对所有路径或存在某条路径进行量化，能表达分支可能性。
• 安全性与活性：安全性断言坏事永不发生，活性断言好事终将发生，是两类基本性质。

应用场景

时序逻辑是模型检测的规约语言，用于表达并发协议、硬件电路、分布式系统应满足的正确性要求。它还用于运行时验证、需求规约、以及人工智能中的规划与推理。许多验证工具直接接受时序逻辑公式作为待检查的性质。

常见问题

问：线性时序逻辑和计算树逻辑哪个更强？答：两者表达能力互不包含，各有对方无法表达的性质。线性时序逻辑擅长描述单条路径上的时序约束，计算树逻辑擅长描述路径分支的存在性与全称性，实践中常根据需求选用，也有兼容两者的更强逻辑。

问：安全性和活性有什么直观区别？答：安全性可以在有限步内被证伪，一旦坏事发生就能立即指出；活性只能在无限行为上判断，因为好事迟迟不发生并不能在任何有限时刻断定它永远不会发生。