《Principles of Model Checking》 Chapter 3 Linear time properties （线性时间特性）

Chapter 3 Linear time properties （线性时间特性）

​ 出于验证目的，所考虑系统的过渡系统模型需要附带待验证的相关属性的规范。**本章介绍了一些重要但相对简单的属性类。对这些属性进行了形式化定义，并提出了基本的模型检查算法来自动检查这些属性。**本章重点讨论线性时间行为，并建立不同类别的属性和跟踪行为之间的关系。介绍并比较了公平的基本形式。

3.1DeadLock(死锁)

​ 不受发散影响的顺序程序（即无限循环）具有终端状态，即没有任何传出转换的状态。然而，对于并行系统，计算通常不考虑目前为止处理的互斥程序。在这样的系统中，终端状态是不可取的，并且大多表示设计错误。因此，整个系统已经停止，而至少有一个组件有可能继续运行。典型的死锁场景发生在组件相互等待进展时。

Example3.1 Deadlock for Fault Designed Traffic Lights

当第一个红绿灯等待与动作α同步时，第二个红绿灯被阻塞，因为它正在等待与动作β同步.

Example 3.2. Dining Philosophers （哲学家进餐问题）

五位哲学家坐在一张圆桌旁，在中间放着一碗米饭。对于哲学家来说（有点超凡脱俗），生活包括思考和饮食（以及等待，我们将看到）。哲学家要从碗里拿出一些米饭，需要两根筷子。

然而，在两个相邻的哲学家之间，只有一根筷子。因此，在任何时候，两个相邻的哲学家中只有一个可以吃饭。当然，筷子是专用的，禁止用手吃饭。

请注意，当所有哲学家都拥有一根筷子时，就会出现死锁场景。

解决方法：

• 允许最多 4 个哲学家同时坐在桌子上。
• 只有一个哲学家的两根筷子都可用时，他才能拿起它们（他必须在临界区内拿起两根 辕子)。
• 使用非对称解决方案。即单号的哲学家先拿起左边的筷子，接着右边的筷子；而双 号的哲学家先拿起右边的筷子，接着左边的筷子。

3.2 Linear-Time Behavior （线性时间行为）

为了分析由转换系统表示的计算机系统，可以采用基于动作或基于状态的方法。基于状态的方法从动作中提取；相反，只考虑状态序列中的标签。相反，基于动作的视图从状态中抽象出来，只引用转换的动作标签。（基于动作和状态的组合视图是可能的，但会导致更复杂的定义和概念。因此，通常从动作或状态标签中抽象出来。）大多数现有规范形式和相关验证方法可以以相应的方式为这两个角度制定。

**在本章中，我们主要关注基于状态的方法。转换的动作标签仅用于建模通信；**因此，它们与以下章节无关。相反，我们使用状态的原子命题来表述系统属性。因此，验证算法在转换系统的状态图上运行，该状态图通过从动作标签中提取而源自转换系统。

3.2.1 Paths and State Graph （路径和状态图）

3.2.2 Traces

3.2.3 Linear-Time Properties （线性时间属性）

​ 在下面，我们假设一组固定的命题AP。线性时间（属性）特性是转换系统轨迹的要求。

Definition 3.10. LT Property

Definition 3.11. Satisfaction Relation for LT Properties

3.2.4 Trace Equivalence and Linear-Time Properties (轨迹等价性和线性时间属性)

轨迹等价、轨迹包含和满足LT属性之间的精确关系是本节的主题。

跟踪包含与LT属性有什么关系？以下定理表明，轨迹包含与表示为LT属性的需求规范兼容。

Theorem 3.15. Trace Inclusion and LT Properties

如果过渡系统具有相同的轨迹集，则称其为轨迹等价：

Definition 3.17. Trace Equivalence

3.3 Safety Properties and Invariants（安全性和不变量）

安全性能通常被描述为“没有什么不好的事情发生”。互斥性是一种典型的安全性，它最多有一个过程处于其临界段。它指出，坏事（在其关键部分同时有两个或多个进程）永远不会发生。另一个典型的安全特性是死锁自由。例如，对于进餐哲学家，这种僵局可以被描述为所有哲学家都在等待拿起第二根筷子的情况。这种糟糕的（即不想要的）情况不应该发生。

3.3.1 Invariants

事实上，上述安全属性属于一种特殊类型：它们是不变量。不变量是由状态的条件Φ给出的LT属性，要求Φ适用于所有可达状态。

​ 我们如何检查过渡系统是否满足不变量？由于检查命题公式Φ的不变量相当于检查Φ在从某个初始状态可到达的每个状态中的有效性，只要给定的转换系统TS是有限的，则对深度优先搜索（DFS）或广度优先搜索（BFS）等标准图遍历算法稍加修改即可。

3.3.2 Safety Properties

Definition 3.22. Safety Properties, Bad Prefixes

Lemma 3.25. Satisfaction Relation for Safety Properties

Definition 3.26. Prefix and Closure

3.3.3 Trace Equivalence and Safety Propertie

Example 3.32. Finite vs. Infinite Transition System

3.4 Liveness Properties

非正式地说，安全属性规定“坏事永远不会发生”。对于互斥算法，“坏”的是不止一个进程处于其关键部分，而对于红绿灯，“坏”的情况是当红灯相位之前没有黄灯相位时。算法只需不做任何事情就可以轻松实现安全属性，因为这永远不会导致“坏”情况。由于这通常是不需要的，安全特性由需要一些进展的特性来补充。

此类属性称为“活性”属性。直觉上，他们说未来会发生“好事”。虽然安全属性在有限时间内（即通过有限系统运行）受到侵犯，但活性属性在无限时间内（即通过无限系统运行）受到侵犯。

3.4.2 Safety vs. Liveness Properties

本节研究活性和安全性之间的关系。特别是，它回答了以下问题：

• 安全性和活性属性是否不相交？
• 任何线性时间属性是安全属性还是活性属性？

正如我们将看到的，第一个问题将得到肯定的回答，而第二个问题将导致否定的回答。然而，有趣的是，对于任何LT性质P等价的LT性质P？确实存在安全性和活性属性的组合（即交叉点）。总之，可以说，安全性和活性属性的识别因此提供了线性时间属性的基本特征。

第一个结果表明，安全性和活性属性实际上几乎是不相交的。更准确地说，它指出，唯一既安全又活跃的属性是非限制性的，即允许所有可能的行为。从逻辑上讲，这相当于“真”
Safety and Liveness Properties - 知乎 (zhihu.com)

3.5 Fairness

3.5.1 Fairness Constraints

• 无条件公平：例如，“每个进程都会无限频繁地执行。”

• 强公平：例如“每个被无限频繁地启用的进程都会无穷频繁地执行”。

• 弱公平：例如：“每个从某个时刻开始连续启用的进程，都会无限经常地执行。”。

Definition 3.43. Unconditional, Strong, and Weak Fairness

Definition 3.46. Fairness Assumption

Definition 3.48. Fair Satisfaction Relation for LT Properties

3.5.2 Fairness Strategies

​ 上一节中的示例表明，可能需要公平性假设来验证过渡系统TS的活性属性。为了排除“不切实际”的计算，对TS的轨迹施加公平性假设，并检查TS |=F P，而不是检查TS（无公平性）。哪些公平性假设适用于检查P？许多模型检查工具提供了使用内置公平性假设的可能性。粗略地说，目的是排除在实际实现中无法执行的执行。但这到底意味着什么？为了深入了解这一点，我们考虑了同步并发系统的几个公平性假设。目的是在所涉及的各个过程之间建立一个公平的沟通机制。经验法则是：需要强公平性来获得（进程之间）冲突的充分解决，而弱公平性足以表示独立动作（即交错）的并发执行的动作集。

concurrency = interleaving (i.e., nondeterminism) + fairness

并发性=交织（即不确定性）+公平性

3.5.3 Fairness and Safety

Theorem 3.55. Realizable Fairness is Irrelevant for Safety Properties

3.6 Summary