模型检查：安全和活性属性
Model Checking : Safety and Liveness properties
我知道什么是 Safety 和 Liveness 属性，以及 LT 的 Safety 和 Badprefixes 之间的关系 属性。我想了解闭包属性以及为什么安全 属性 的闭包是 属性 本身。图片仅供参考。谁能给我解释一下可以用来回答问题的概念，这真的很有帮助。
我们正在考虑无限痕迹的语言。
正如您所暗示的，语言 L 被定义为安全的 属性 如果对于不在 L 中的每条踪迹，都存在一个错误的前缀，即一个有限前缀，例如该前缀的所有无限延续不在 L 中。所以直觉上，安全 属性 是关于一些坏事件没有发生。
对于给定的语言 L，语言闭包 (L) 被定义为由所有轨迹组成，其中每个有限前缀也是 L 中轨迹的前缀。
采用闭包的标准示例是 L = a*b^omega = { bbb..., abbb..., aabbb..., aaabbb... }。语言 L 包含所有具有有限前缀 a 和无限多个 b 的迹。那么闭包(L) = a*b^omega + a^omega = L U {aaa...}。无限多个a的迹不包含在L中，但a^omega的每个有限前缀也是L中迹的前缀。因此a^omega包含在L的闭包中。
现在你的问题是为什么对于安全性属性 L，它认为L = closure(L)。
设L为安全属性。我们必须证明 L 中的每条轨迹都包含在闭包 (L) 中，反之亦然，闭包 (L) 中的每条轨迹都包含在 L 中。
L中的每条迹都包含在closure(L)中：考虑L中的迹sigma。那么sigma的每个有限前缀都是sigma的前缀。因此，sigma 的每个有限前缀都是 L 中迹的前缀。根据 closure(L) 的定义，可以得出 sigma 在 closure(L) 中。
闭包(L)中的每条轨迹都包含在L中：设sigma在闭包(L)中。假设 sigma 不在 L 中。根据安全属性的定义，sigma 有一个有限前缀 w，因此在 L 中没有 w 的无限延续。但是 w 不能是 L 中单词的前缀。但是根据闭包的定义（ L), sigma 的每个有限前缀都必须在 L 中。矛盾。由于sigma不在L中的假设导致矛盾，因此得出sigma在L中。
旁注 A：请注意，对于 1. 我们没有使用 L 是安全性 属性。 属性 L 是 closure(L) 的一个子集一般都成立，而不仅仅是为了安全属性。
旁注 B：在闭包示例中，我们注意到对于 L = a*b^omega，我们有闭包 (L) = a*b^omega + a^omega。因此L不等于closure(L)，所以L不可能是安全的属性。我们可以从迹 a^omega 看出这一点，它不在 L 中，但没有坏前缀，因为 a^omega 的每个有限前缀都是 a* 的形式，并且可以继续到形式为 a 的迹*b^欧米茄在 L.
旁注 C：我们也可以问相反的问题，当 L = closure(L) 时，L 是安全的吗 属性？答案是肯定的。令 L 为 L = closure(L) 的语言。考虑一个不在 L 中的迹 sigma。我们必须证明 sigma 有一个错误的前缀。通过 L = closure(L)，我们有 sigma 不在 closure(L) 中。根据 closure(L) 的定义，如果 sigma 的所有有限前缀都在 L 中，我们将在 closure(L) 中有 sigma。因此，根据 sigma not in closure(L)，可以得出 sigma 有一些有限前缀 w，这样 L 中的所有迹线 sigma' 都没有 w 作为前缀。换句话说，w 的每一个无限延续都不可能是 L 中的踪迹。因此 w 是一个坏前缀。总之，每个不在 L 中的迹线西格玛都有一个错误的前缀，因此 L 是安全的 属性.
旁注 D：根据您的原始问题和旁注 C，我们可以得出结论，当且仅当 L = closure(L) 时，L 是安全的 属性。这提高了我们对采用 L 的闭包意味着什么的理解：添加所有没有错误前缀的跟踪。此外，您可以验证获取闭包的闭包不会添加任何新的踪迹，因此对于任何 L，它认为 closure(L) = closure(closure(L))。因此对于任何 L，它认为 closure(L) 是安全的 属性.
旁注 E：为了回答您的评论问题，举一个等同于其闭包的语言示例：基于旁注 D，我们可以采取任何安全措施 属性：考虑字母表上的语言 L { a,b,c} 即 L = { {a,b,c}^omega 中的 sigma |西格玛没有 c }。因此，坏前缀将是所有具有 c 的有限词（如果您将跟踪视为对某些程序的执行进行建模，则 c 可能表示 "the program has a crash" 并在之后执行随机操作）。我们可以验证L = closure(L)：我们已经知道L子集closure(L)，基于上面的1.。对于另一个方向，考虑 closure(L) 中的跟踪 sigma。根据闭包 (L) 的定义，sigma 的每个有限前缀 w 必须是 L 中迹 sigma' 的前缀。由于根据 L 的定义，sigma' 不能包含 c，因此 w 不能包含 c。当 sigma 的每个有限前缀 w 都不能包含 c 时，则 sigma 不能包含 c。因此 sigma 在 L 中。我们得出 L = closure(L).
我知道什么是 Safety 和 Liveness 属性，以及 LT 的 Safety 和 Badprefixes 之间的关系 属性。我想了解闭包属性以及为什么安全 属性 的闭包是 属性 本身。图片仅供参考。谁能给我解释一下可以用来回答问题的概念，这真的很有帮助。
我们正在考虑无限痕迹的语言。
正如您所暗示的，语言 L 被定义为安全的 属性 如果对于不在 L 中的每条踪迹，都存在一个错误的前缀，即一个有限前缀，例如该前缀的所有无限延续不在 L 中。所以直觉上，安全 属性 是关于一些坏事件没有发生。
对于给定的语言 L，语言闭包 (L) 被定义为由所有轨迹组成，其中每个有限前缀也是 L 中轨迹的前缀。
采用闭包的标准示例是 L = a*b^omega = { bbb..., abbb..., aabbb..., aaabbb... }。语言 L 包含所有具有有限前缀 a 和无限多个 b 的迹。那么闭包(L) = a*b^omega + a^omega = L U {aaa...}。无限多个a的迹不包含在L中，但a^omega的每个有限前缀也是L中迹的前缀。因此a^omega包含在L的闭包中。
现在你的问题是为什么对于安全性属性 L，它认为L = closure(L)。
设L为安全属性。我们必须证明 L 中的每条轨迹都包含在闭包 (L) 中，反之亦然，闭包 (L) 中的每条轨迹都包含在 L 中。
L中的每条迹都包含在closure(L)中：考虑L中的迹sigma。那么sigma的每个有限前缀都是sigma的前缀。因此，sigma 的每个有限前缀都是 L 中迹的前缀。根据 closure(L) 的定义，可以得出 sigma 在 closure(L) 中。
闭包(L)中的每条轨迹都包含在L中：设sigma在闭包(L)中。假设 sigma 不在 L 中。根据安全属性的定义，sigma 有一个有限前缀 w，因此在 L 中没有 w 的无限延续。但是 w 不能是 L 中单词的前缀。但是根据闭包的定义（ L), sigma 的每个有限前缀都必须在 L 中。矛盾。由于sigma不在L中的假设导致矛盾，因此得出sigma在L中。
旁注 A：请注意，对于 1. 我们没有使用 L 是安全性 属性。 属性 L 是 closure(L) 的一个子集一般都成立，而不仅仅是为了安全属性。
旁注 B：在闭包示例中，我们注意到对于 L = a*b^omega，我们有闭包 (L) = a*b^omega + a^omega。因此L不等于closure(L)，所以L不可能是安全的属性。我们可以从迹 a^omega 看出这一点，它不在 L 中，但没有坏前缀，因为 a^omega 的每个有限前缀都是 a* 的形式，并且可以继续到形式为 a 的迹*b^欧米茄在 L.
旁注 C：我们也可以问相反的问题，当 L = closure(L) 时，L 是安全的吗 属性？答案是肯定的。令 L 为 L = closure(L) 的语言。考虑一个不在 L 中的迹 sigma。我们必须证明 sigma 有一个错误的前缀。通过 L = closure(L)，我们有 sigma 不在 closure(L) 中。根据 closure(L) 的定义，如果 sigma 的所有有限前缀都在 L 中，我们将在 closure(L) 中有 sigma。因此，根据 sigma not in closure(L)，可以得出 sigma 有一些有限前缀 w，这样 L 中的所有迹线 sigma' 都没有 w 作为前缀。换句话说，w 的每一个无限延续都不可能是 L 中的踪迹。因此 w 是一个坏前缀。总之，每个不在 L 中的迹线西格玛都有一个错误的前缀，因此 L 是安全的 属性.
旁注 D：根据您的原始问题和旁注 C，我们可以得出结论，当且仅当 L = closure(L) 时，L 是安全的 属性。这提高了我们对采用 L 的闭包意味着什么的理解：添加所有没有错误前缀的跟踪。此外，您可以验证获取闭包的闭包不会添加任何新的踪迹，因此对于任何 L，它认为 closure(L) = closure(closure(L))。因此对于任何 L，它认为 closure(L) 是安全的 属性.
旁注 E：为了回答您的评论问题，举一个等同于其闭包的语言示例：基于旁注 D，我们可以采取任何安全措施 属性：考虑字母表上的语言 L { a,b,c} 即 L = { {a,b,c}^omega 中的 sigma |西格玛没有 c }。因此，坏前缀将是所有具有 c 的有限词（如果您将跟踪视为对某些程序的执行进行建模，则 c 可能表示 "the program has a crash" 并在之后执行随机操作）。我们可以验证L = closure(L)：我们已经知道L子集closure(L)，基于上面的1.。对于另一个方向，考虑 closure(L) 中的跟踪 sigma。根据闭包 (L) 的定义，sigma 的每个有限前缀 w 必须是 L 中迹 sigma' 的前缀。由于根据 L 的定义，sigma' 不能包含 c，因此 w 不能包含 c。当 sigma 的每个有限前缀 w 都不能包含 c 时，则 sigma 不能包含 c。因此 sigma 在 L 中。我们得出 L = closure(L).