1 基本概念
时态逻辑是一种将“时间”纳入形式推理框架的逻辑系统。它关注命题在不同时间点或时间区间中的真值变化，并借助专门的时态算子描述事件先后、持续、终止和反复出现等关系。与只讨论静态真假关系的传统逻辑相比，时态逻辑更适合刻画动态过程。
1.1 定义与研究对象
时态逻辑的研究对象主要是那些随时间变化而成立的命题，以及这些命题之间在时间轴上的联系。它不仅关心某个断言在某一时刻是否为真，也关心它在过去是否曾为真、在未来是否必然成立，或者是否会在某个阶段反复出现。
1.1.1 时间维度中的命题真值
在时态逻辑中，同一个命题在不同时间点上可以具有不同的真值。例如，“系统已启动”在某一时刻可能为假，而在之后的时刻变为真。这类变化使得命题的判断不再是一次性的，而是与时间索引紧密相关。
1.1.2 时态逻辑与传统逻辑的区别
传统逻辑通常默认命题的真假在讨论范围内是固定的，重点在于推理形式是否有效。时态逻辑则在此基础上增加了时间结构，使公式能够表达“何时为真”“何时曾经为真”“何时将为真”等信息，因此更能描述过程性和演化性现象。
1.2 核心时态算子
时态逻辑的表达能力，很大程度上依赖于若干核心算子。这些算子用于把时间关系嵌入命题公式中，从而形成更丰富的语义。
1.2.1 过去时态算子
过去时态算子用来描述在当前时刻之前发生的事实，例如“曾经”“一直以来曾经成立”等。它常用于回溯历史状态，适合表达日志、记忆和既往条件。
1.2.2 现在时态算子
现在时态算子用于指出命题在当前时刻的成立状况。虽然在很多形式系统中“现在”本身无需特殊符号即可理解，但在某些扩展体系里，它仍可作为与过去、未来对照的基准。
1.2.3 将来时态算子
将来时态算子用于描述未来时刻的可能性或必然性，如“下一步”“最终”“总会”等。它在程序验证和系统行为分析中尤为重要，因为它可以表达后续状态是否满足预期条件。
1.3 语法与语义
时态逻辑既有严格的形式语法，也有相应的解释语义。语法规定哪些公式是合法的，语义则说明这些公式在具体时间模型中如何被理解和判定。
1.3.1 公式构造规则
时态逻辑通常以命题变元、逻辑联结词和时态算子为基本构件，通过递归方式生成公式。合法公式一般可以由原子命题出发，经否定、合取、析取、蕴含以及时态操作逐步构造而成。
1.3.2 时间结构的解释方式
公式的解释依赖于所采用的时间结构。时间可以被看作离散序列、连续区间，或者包含多个可能未来的分支结构。不同结构决定了“下一步”“最终”“一直”等概念的具体含义。
1.3.3 可满足性与有效性
可满足性指某个公式是否能在某个时间模型和某个时刻下为真；有效性则表示该公式在所有适用模型中都成立。二者是时态逻辑研究中的基础问题，也直接关系到推理系统的可靠性。
2 发展历史
时态逻辑并非突然出现，而是从哲学、数学逻辑与计算理论的交汇中逐步发展起来的。其形成过程与人类对“变化”这一概念的长期思考密切相关。
2.1 早期思想来源
2.1.1 哲学中的时间与变化问题
古典哲学早已关注时间、运动和变化之间的关系。关于“事物如何在变化中保持同一性”“未来是否已经确定”等问题，为后来的形式化研究提供了思想背景。
2.1.2 经典逻辑对时间表达的局限
早期逻辑体系在处理时间时往往需要借助额外的自然语言说明，难以直接表达“先后”“持续”“变化”等概念。这种局限推动研究者寻找能在公式内部直接编码时间信息的方法。
2.2 形式化阶段
2.2.1 现代时态逻辑的提出
20世纪中叶以后，研究者开始将时间作为逻辑系统中的正式对象，引入专门算子来处理时间关系。现代时态逻辑由此成型，并逐渐获得清晰的语法、语义与证明理论。
2.2.2 主要理论框架的形成
随着研究深入，不同时间观念对应的理论框架相继建立，包括线性时间、分支时间、过去时态系统以及区间时态系统等。它们共同构成了时态逻辑的核心谱系。
2.3 学科扩展
2.3.1 与计算机科学的结合
时态逻辑在计算机科学中迅速发展，特别是在程序正确性证明、并发过程建模和自动化验证方面表现突出。它使系统行为可以被精确地描述为时间序列上的性质集合。
2.3.2 与语言学和人工智能的交叉
在语言学中，时态逻辑有助于分析动词时态、体貌和句法中的时间指向；在人工智能中，它则用于表示知识随时间更新、任务执行顺序及计划推理等问题。
3 主要类型
根据对时间的理解方式不同，时态逻辑可以分为多个类型。不同类型各有适用场景，反映了时间结构在形式系统中的多样化处理。
3.1 线性时态逻辑
线性时态逻辑把时间看作单一方向上的序列，所有事件都沿着一条时间线展开。它强调“先发生什么、后发生什么”，适合描述确定性流程。
3.1.1 离散线性时间
离散线性时间把时间划分为一个个相邻时刻，常用于描述计算机程序的步骤、状态迁移和数字系统运行。此时，时间推进可以看作逐步跳转。
3.1.2 连续线性时间
连续线性时间则将时间视为无间断的整体，适合用于物理过程或连续变化现象的建模。与离散时间相比，它对瞬时变化和持续区间的刻画更细致。
3.2 分支时态逻辑
分支时态逻辑认为未来并非唯一，而是由多个可能的发展路径组成。它常用于处理非确定性系统，因为同一当前状态可能通向多种后续结果。
3.2.1 多种未来可能性的表示
在这种框架下，公式可以区分“存在某种未来会发生”与“所有未来都必须发生”两类判断。这样便能表达选择、风险和条件性演化。
3.2.2 路径与分支语义
分支时态逻辑通常以路径为基本解释单位，再由不同路径构成分支结构。路径语义使研究者能够分别考察单一路径性质与全分支性质。
3.3 过去时态逻辑
过去时态逻辑专门增强对历史信息的表达能力。它不仅关注未来预测，也重视对既往状态的回顾与追踪。
3.3.1 历史信息的表达
过去时态逻辑可以形式化“曾经发生过”“在此前一直成立”等陈述，因此适用于故障追溯、事件日志分析和行为审计等场景。
3.3.2 记忆性命题
所谓记忆性命题，是指其真值依赖于历史过程而非仅取决于当前状态。过去时态逻辑可以将这类命题纳入统一框架，使其历史依赖关系更易分析。
3.4 混合时态逻辑
混合时态逻辑综合了多种时间处理方式，通常同时引入时间点、时间区间以及其他逻辑机制，以增强表达能力。
3.4.1 时间点与时间区间
这类系统既可以讨论某一瞬间是否满足条件，也可以讨论某个时间段内是否持续成立。点与区间的并用，提升了对复杂过程的描述精度。
3.4.2 与模态逻辑的融合
混合时态逻辑常吸收模态逻辑的思想，把时间关系看成一种特殊的可达关系。这样不仅能统一多种语义，也便于借助模态方法进行推理。
4 语义理论
时态逻辑的语义理论说明公式如何在具体模型中获得解释。不同语义框架决定了系统的适用范围，也影响证明性质和算法实现。
4.1 克里普克语义
克里普克语义是时态逻辑中最常用的解释方式之一。它借助状态、关系和赋值来说明命题在不同时间点上的真值分布。
4.1.1 状态、关系与赋值
在该语义下，状态表示时间或世界中的一个位置，关系用于连接状态之间的时间推进，赋值则指定原子命题在哪些状态下成立。三者共同构成完整模型。
4.1.2 可达性结构
可达性结构描述一个状态能否通向另一个状态，以及通达顺序如何展开。对于“下一步”“最终”等时态算子，这种结构尤为关键。
4.2 时间模型
时间模型是时态逻辑语义的核心基础。不同模型对应不同的时间观，直接影响公式的解释结果。
4.2.1 离散时间模型
离散时间模型将时间组织为有序序列，适合处理一步一步演化的系统。许多计算机科学中的时态分析都以此为基础。
4.2.2 稠密时间模型
稠密时间模型假定任意两个时间点之间还存在其他时间点，因此更接近连续变化的直观。它常用于物理过程、控制系统和某些语言学分析。
4.2.3 分支结构模型
分支结构模型把未来看作树状展开的可能集合。它能自然表达非确定性、选择和多路径演化，是分支时态逻辑的重要语义基础。
4.3 语义性质
时态逻辑的语义性质关系到系统是否严密、是否可计算以及是否适合自动推理。
4.3.1 一致性
一致性指系统内部不存在明显冲突，即不会同时推出某命题及其否定。良好的语义体系应当能够避免模型层面的自相矛盾。
4.3.2 完备性
完备性表示如果某个公式在所有模型中都成立，那么它应当能够在相应证明系统中被推出。这是逻辑理论成熟的重要标志。
4.3.3 可判定性
可判定性关心是否存在算法，能在有限步骤内判断某个公式是否满足给定性质。对时态逻辑而言，这一性质对实际应用尤其重要。
5 证明系统
证明系统为时态逻辑提供形式化推导工具，使语义上的正确性可以转化为可操作的推理步骤。
5.1 公理化体系
公理化体系通过若干基础公理和推理规则来刻画时态逻辑中的合法推导。它具有结构清晰、便于分析的优点。
5.1.1 基本公理
基本公理通常包括经典逻辑公理以及反映时间关系的时态公理。例如，一些公理专门描述“总是”“最终”与逻辑联结词之间的交互。
5.1.2 时态推理规则
时态推理规则用于处理时间算子带来的特殊推导模式，如从某时刻成立推出其后继时刻的某种性质，或从全局成立推出局部成立。
5.2 序列演算
序列演算是一种结构化证明方法，强调在推导过程中保持公式集合与结论之间的关系。它适合用于元理论分析。
5.2.1 公式变换规则
公式变换规则允许将复杂时态公式拆解为更简单的部分，从而逐步归约到可处理的形式。这种方式在自动证明中较为常见。
5.2.2 证明归约方法
证明归约方法通过不断缩减待证对象，把原问题转化为更基础的子问题。对于具有递归时间结构的公式，这种方法尤其有效。
5.3 自然演绎系统
自然演绎系统以人类直观推理为风格，强调从假设出发逐步导出结论，具有较强可读性。
5.3.1 引入规则
引入规则说明如何在推理中加入某个时态算子，例如从特定条件下的成立引入“将来必然”或“曾经发生”等表达。
5.3.2 消去规则
消去规则则说明如何从包含时态算子的公式中提取有用信息，使复杂表达回到较为基础的命题层面。
6 形式性质
时态逻辑的形式性质主要包括可满足性、可判定性、复杂度与证明系统的可靠程度。这些内容直接决定其理论价值与工程可用性。
6.1 可满足性问题
可满足性问题考察一个公式是否可能在某个模型中成立。它是逻辑系统分析中的核心判定任务之一。
6.1.1 模型存在性
模型存在性意味着是否能够构造出一个时间结构，使所给公式在其中为真。若存在这样的模型，公式就具有可满足性。
6.1.2 约束满足分析
可满足性常可转化为约束满足问题，即检验各个时态条件是否能够同时实现。这在自动推理和模型检测中都有重要作用。
6.2 可判定性与复杂度
时态逻辑的可判定性与复杂度反映了其计算代价。不同子系统在时间和空间资源上的需求差异很大。
6.2.1 算法复杂度分类
一些简单时态逻辑可以在较低复杂度类中处理，而表达能力更强的系统则可能需要更高阶算法。复杂度分类有助于区分可实用与理论性的不同层次。
6.2.2 计算资源需求
在实际应用中，公式长度、模型大小和时间结构丰富程度都会影响计算资源消耗。资源需求越高，自动化分析就越依赖优化技术。
6.3 完备性与可靠性
完备性和可靠性是证明系统是否值得信赖的关键指标。它们分别从语义和推理两方面保证系统一致运行。
6.3.1 语义完备性
语义完备性表明证明系统能够覆盖全部语义上有效的结论。对于时态逻辑而言，这意味着时间语义和形式推演之间保持协调。
6.3.2 证明系统可靠性
可靠性通常指证明系统不会导出语义上错误的结论。若系统可靠，则所有可证公式都应在相应模型类中成立。
7 应用领域
时态逻辑的应用范围较广，尤其适合研究具有顺序性、持续性和状态变化的对象。其方法已渗透到多个学科领域。
7.1 计算机科学
计算机科学是时态逻辑最重要的应用领域之一。它为程序、协议和系统行为提供了精确的形式描述工具。
7.1.1 程序验证
程序验证利用时态逻辑检查程序运行过程中是否满足安全性、终止性或资源约束等性质。它能够把“程序应该如何运行”转化为逻辑公式。
7.1.2 并发系统建模
并发系统中多个组件可能同时推进，状态之间存在复杂交互。时态逻辑能够描述这些组件的先后关系和同步条件。
7.1.3 反应式系统分析
反应式系统持续对外部输入作出响应，具有明显的时间依赖特征。时态逻辑可用于分析其响应是否及时、是否稳定以及是否符合预期模式。
7.2 人工智能
在人工智能中，时态逻辑常用于知识表示和时序推理，帮助系统处理随时间更新的信息。
7.2.1 知识表示
知识并非总是静态不变的，许多事实会随着观察、执行或环境变化而改变。时态逻辑可将这些知识纳入统一表示框架。
7.2.2 时序推理
时序推理关注事件先后、计划步骤和长期目标的实现过程。时态逻辑使系统能够对“之后会怎样”进行形式化分析。
7.3 语言学
语言学中的许多现象都与时间有关，尤其是动词时态、体貌和叙述顺序。时态逻辑为这些现象提供了较为严格的分析工具。
7.3.1 时体系统分析
时体系统分析关注句子中表示过去、进行、完成和习惯性的语言形式。时态逻辑可帮助区分不同时间指向与事件内部结构。
7.3.2 句子时序解释
在叙述文本中，句子顺序不一定等同于事件发生顺序。时态逻辑有助于解释回忆、插叙和前瞻等复杂时序关系。
7.4 哲学
哲学领域对时态逻辑的兴趣主要集中在时间本体和真值随时间变化的问题上。它为相关讨论提供了更精确的分析语言。
7.4.1 时间本体论
时间本体论研究时间是否独立存在、时间点之间如何关联以及“现在”的地位等问题。时态逻辑能够将这些抽象议题转化为形式结构。
7.4.2 命题真值随时间变化
一些命题的真假显然依赖时间，例如“门是开着的”可能在不同时刻对应不同判断。时态逻辑正是用来刻画这类时间敏感命题的。
8 相关分支与扩展
时态逻辑与若干其他逻辑分支关系密切。随着研究深化，它不断吸收外部理论并发展出更多扩展形式。
8.1 动态逻辑的联系
动态逻辑关注行为或程序执行后的状态变化，与时态逻辑在描述过程方面有天然联系。二者常在系统建模中互相补充。
8.1.1 行为变化与时间表达
动态逻辑更强调动作对状态的改变，而时态逻辑更强调时间推进中的性质变化。两者结合后，可以更完整地描述“做了什么”以及“随后发生了什么”。
8.2 模态逻辑的关系
时态逻辑通常被视为模态逻辑的一个时间化分支。它继承了模态逻辑处理可能性、必然性和可达关系的基本思想。
8.2.1 可能性与必然性的时间化
在时态逻辑中，“可能”和“必然”被重新解释为未来或过去某种时间结构上的成立方式。这样便形成了具有时间方向的模态表达。
8.3 认知时态逻辑
认知时态逻辑将知识、信念等认知状态与时间因素结合，用于分析信息随时间变化的过程。
8.3.1 信念与时间信息结合
这类系统可表达“某主体在过去相信什么”“之后是否会更新信念”等问题，因此适合研究信息传播、学习和决策过程。
8.4 区间时态逻辑
区间时态逻辑不只关注单个时刻，还关注时间区间内的整体性质，因此更适合描述持续性和阶段性现象。
8.4.1 时间区间上的性质描述
它可以表达“在某段时间内始终成立”“在某个区间内至少发生过一次”等性质。与点时态逻辑相比，其表达更贴近过程本身。
9 经典问题与研究方向
时态逻辑的研究并未停留在基本体系的建立上，围绕语义、表达能力和自动推理的进一步问题仍在持续推进。
9.1 语义等价
语义等价研究不同模型、不同定义或不同形式系统之间是否在表达上保持一致。这是比较各类时态逻辑的重要手段。
9.1.1 不同模型之间的转换
不同时间模型之间可能通过转换、嵌入或近似建立联系。研究这些转换关系，有助于统一看待多种时态语义。
9.2 表达能力
表达能力考察一个时态逻辑系统究竟能描述哪些时间性质，以及哪些性质超出了其能力范围。
9.2.1 语言可表达性质
某些性质可以直接用简单算子表达，而另一些则需要更强的系统或辅助构造。表达能力研究正是为了划分这种边界。
9.3 自动推理
自动推理是时态逻辑走向实际应用的关键环节。它依赖算法来完成模型检查、公式证明和反例搜索等任务。
9.3.1 模型检测
模型检测通过枚举或搜索系统状态，判断目标性质是否在给定模型中成立。它是时态逻辑在工程领域最常见的应用方式之一。
9.3.2 定理证明
定理证明则从公理和推理规则出发，尝试证明某个时态公式必然成立。与模型检测相比，它更偏向演绎式分析。
9.4 进一步发展
时态逻辑的未来发展通常围绕更复杂的时间结构和更广泛的理论融合展开，以增强其表达与推理能力。
9.4.1 更丰富的时间结构
研究者不断探索更复杂的时间组织方式，如多线时间、混合连续离散结构等，以适应更精细的现实建模需求。
9.4.2 与其他形式系统的融合
时态逻辑也在与概率逻辑、资源逻辑、认知逻辑等系统融合。此类交叉研究有望形成更适合复杂系统分析的统一框架。