计算中的时态逻辑与模态逻辑
时态逻辑和模态逻辑通过引入时间算子和可能性算子来扩展经典逻辑，提供了精确的语言来描述程序或反应系统在其整个执行过程中必须如何行为。
用 PaperMind 寻找选题即将推出Find papers & topics
Tools & resources
Learn & explore
视频即将推出
Definition
时态逻辑通过增加算子来增强命题逻辑或一阶逻辑，这些算子描述了属性在计算过程中何时成立，例如“总是”、“最终”和“直到”；模态逻辑通过在状态和转换结构上使用必然性和可能性算子来概括这一点。
Scope
本主题涵盖线性时态逻辑和分支时态逻辑，如LTL和CTL；模态逻辑，包括动态逻辑和模态μ-演算；安全性和活性属性的表达；以及模型检验和可满足性等算法问题，这些问题使这些逻辑成为自动化验证的核心。
Core questions
- 逻辑如何表达“好事最终会发生”或“坏事永远不会发生”？
- 对单一执行路径进行推理与对所有可能未来进行推理之间有什么区别？
- 如何将检查系统是否满足时态属性的过程算法化？
- 哪些时态逻辑在表达能力和高效验证之间取得了平衡？
Key theories
- 用于程序规范的时态逻辑
- Pnueli表明，时态逻辑通过表达程序执行过程中的属性，捕获了反应式和并发程序的正确性，为安全性和活性要求提供了统一的语言。
- 分支时态逻辑的模型检验
- Clarke和Emerson引入了计算树逻辑和一种自动验证有限状态模型的算法，从而开创了模型检验领域。
Clinical relevance
时态逻辑是模型检验器的规范语言，这些检验器常用于验证硬件设计、通信协议和并发软件，在部署前捕获死锁和违反安全性和活性的情况；这项技术为其创始人赢得了图灵奖，并且是芯片设计中的标准技术。
History
Pnueli于1977年提出时态逻辑用于程序推理，Clarke和Emerson与Queille和Sifakis独立地在大约1981年开发了模型检验。通过1990年代早期的符号方法，该方法扩展到工业系统，其创建者因此技术获得了图灵奖。
Key figures
- Amir Pnueli
- Edmund Clarke
- E. Allen Emerson
- Joseph Sifakis
Related topics
Seminal works
- clarkeEmerson1981
- huthRyan2004
Frequently asked questions
- 线性时态逻辑和分支时态逻辑有什么区别？
- 线性时态逻辑（如LTL）描述单个（可能是无限的）执行路径的属性。分支时态逻辑（如CTL）量化每个状态的所有可能未来的树，允许表达在某些路径或所有路径上某个属性成立。它们具有不同的表达能力和验证算法。
- 模型检验如何使用这些逻辑？
- 系统被表示为有限状态模型，期望的属性被表示为时态逻辑公式。模型检验器穷尽地探索状态以确定公式是否成立，如果失败，它会生成一个反例轨迹，使验证既自动化又具有诊断性。