logic - 模型检查：安全性和活性属性

Question

我知道什么是 Safety 和 Liveness 属性，以及 LT 属性的 Safety 和 Badprefixes 之间的关系。我想了解闭包属性以及为什么安全属性的闭包就是属性本身。图片仅供参考。有人可以向我解释可以使用的概念，使我能够回答问题，这将非常有帮助。

标签： logicformal-languagestemporalmodel-checking

Answer 1

我们正在考虑无限痕迹的语言。

正如您所暗示的那样，如果对于不在 L 中的每个跟踪都存在一个错误前缀，则语言 L 被定义为安全属性，也就是说，一个有限前缀，这样前缀的所有无限延续都不在 L 中。所以直观地说，a安全属性是关于一些没有发生的坏事件。

对于给定的语言 L，语言闭包（L）被定义为由所有迹线组成，其中每个有限前缀也是 L 中迹线的前缀。

采用闭包的标准示例是 L = a*b^omega = { bbb..., abbb..., aabbb..., aaabbb... }。语言 L 包含所有带有有限前缀 a 和无限多个 b 的迹线。然后闭包(L) = a*b^omega + a^omega = LU {aaa...}。无限多个a的迹不包含在L中，但a^omega的每个有限前缀也是L中迹的前缀。因此a^omega包含在L的闭包中。

现在你的问题是为什么对于安全属性 L，它认为 L = 闭包（L）。

令 L 为安全属性。我们必须证明 L 中的每一条迹线都包含在闭包（L）中，反之亦然，闭包（L）中的每条迹线都包含在 L 中。

1. L 中的每条迹线都包含在闭包（L）中：考虑 L 中的迹线 sigma。那么 sigma 的每个有限前缀都是 sigma 的前缀。因此，sigma 的每个有限前缀都是 L 中迹线的前缀。根据closure(L) 的定义，sigma 在closure(L) 中。

2. 闭包（L）中的每条迹线都包含在L中：让sigma在闭包（L）中。假设 sigma 不在 L 中。根据安全属性的定义，sigma 有一个有限前缀 w，因此在 L 中没有 w 的无限延续。但是 w 不能是 L 中单词的前缀。但是根据闭包的定义（ L)，sigma 的每个有限前缀都必须在 L. 矛盾中。由于 sigma 不在 L 中的假设导致矛盾，因此 sigma 在 L 中。

旁注 A：请注意，对于 1. 我们没有使用 L 是安全属性。L 是闭包 (L) 的子集的属性通常具有，而不仅仅是安全属性。

旁注 B：在闭包的示例中，我们注意到对于 L = a*b^omega，我们有闭包（L）=a*b^omega + a^omega。因此 L 不等于闭包（L），因此 L 不能是安全属性。我们可以从迹线 a^omega 中看到这一点，它不在 L 中，但没有坏前缀，因为 a^omega 的每个有限前缀都是 a* 形式，并且可以继续到形式 a 的迹线*b^omega 在 L 中。

旁注 C：我们也可以问相反的问题，当 L = 闭包（L）时，L 是安全属性吗？答案是肯定的。令 L 为 L = 闭包(L) 的语言。考虑一个不在 L 中的迹 sigma。我们必须证明 sigma 有一个错误的前缀。通过 L = 闭包（L），我们有 sigma 不在闭包（L）中。根据闭包（L）的定义，如果 sigma 的所有有限前缀都在 L 中，我们将在闭包（L）中有 sigma。因此，从不在闭包（L）中的 sigma 可以得出，存在 sigma 的某个有限前缀 w，使得 L 中的所有迹线 sigma' 都没有 w 作为前缀。换句话说，w 的每一个无限延续都不能成为 L 中的一个踪迹。因此 w 是一个坏前缀。总之，每个不在 L 中的迹 sigma 都有一个坏前缀，因此 L 是一个安全属性。

旁注 D：从您最初的问题和旁注 C，我们可以得出结论，当且仅当 L = 闭包（L）时，L 是安全属性。这提高了我们对关闭 L 的含义的理解：添加所有没有错误前缀的跟踪。此外，您可以验证采用闭包的闭包不会添加任何新的痕迹，因此对于任何 L，它都认为闭包（L）=闭包（闭包（L））。因此对于任何 L，它认为闭包（L）是一个安全属性。

旁注 E：要回答您对等于其闭包的语言示例的评论问题：基于旁注 D，我们可以采用任何安全属性：考虑字母表 {a,b,c} 上的语言 L，即 L = { {a,b,c} 中的 sigma ^omega | sigma 没有 c }。因此，坏前缀将是所有具有 ac 的有限词（如果您将跟踪视为对某个程序的执行进行建模，那么 c 可能意味着“程序发生崩溃”并在此之后执行随机操作）。我们可以验证 L =closure(L)：我们已经知道 L 子集closure(L)，基于上面的 1.。对于另一个方向，考虑闭包（L）中的迹线 sigma。根据闭包（L）的定义，sigma 的每个有限前缀 w 必须是 L 中的迹 sigma' 的前缀。由于根据 L 的定义，sigma' 不能包含 ac，因此 w 不能包含 c。当 sigma 的每个有限前缀 w 不能包含 c 时，sigma 不能包含 c。因此 sigma 在 L 中。我们得出结论 L =closure(L)。