《Principles of Model Checking》Chapter 5 Linear Temporal Logic

Chapter 5 Linear Temporal Logic

​ 本章介绍（命题）线性时序逻辑（LTL），这是一种适用于指定LT属性的逻辑形式。定义了线性时序逻辑的语法和语义。提供了各种示例，展示了如何使用线性时序逻辑来指定重要的系统属性。本章的第二部分涉及基于Büchi自动机的LTL模型检查算法

5.1 Linear Temporal Logic

时间逻辑中时间的本质可以是线性的，也可以是分支的。在线性视图中，每一时刻都有一个单一的后续时刻，而在分支视图中，它有一个分支的树状结构，时间可以分为不同的过程。本章讨论LTL（线性时态逻辑），一种基于线性时间视角的时态逻辑。第6章介绍了CTL（计算树逻辑），这是一种基于分支时间视图的逻辑。一些模型检查工具使用LTL（或其微小变体）作为属性规范语言。模型检查器SPIN是这种自动验证工具的一个突出例子。LTL的主要优点之一是，强加公平性假设（如强公平性和弱公平性）不需要使用任何新机制：典型的公平性假设都可以在LTL中指定。在公平性约束下验证LTL公式可以使用LTL算法完成。这不适用于CTL。

5.1.1 Syntax （语法）

Example 5.2. Properties for the Mutual Exclusion Problem

Example 5.3. Properties for the dining philosophers

Example 5.4. Properties for a Traffic Light

5.1.2 Semantics（语义）

Definition 5.6. Semantics of LTL (Interpretation over Words)

Definition 5.7. Semantics of LTL over Paths and States

Example 5.8. Semantics of LTL

5.1.3 Specifying Properties

Example 5.11. Modulo 4 Counter

Example 5.12. A Communication Channel

Example 5.13. Dynamic Leader Election

5.1.4 Equivalence of LTL Formulae