模型检查：安全性和活动性

Question

我知道什么是安全性和活动性属性，以及LT属性的安全性和错误前缀之间的关系。我想了解关闭属性，以及为什么安全属性的关闭就是属性本身。该图像仅供参考。有人可以向我解释可以使用的概念，使我能够回答问题，这真的很有帮助。

Answer 1

我们正在考虑使用无限轨迹的语言。

正如您所暗示的，如果对于每个不在L中的迹线都存在一个错误的前缀（即，一个有限的前缀，使得该前缀的所有无限延续都不在L中），则将语言L定义为安全属性。 ，安全属性是指未发生的一些不良事件。

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

采用闭包的标准示例是L = a * b ^ ome​​ga = {bbb ...，abbb ...，aabbb ...，aaabbb ...}。语言L包含所有带有有限前缀a的迹线，然后无限多个b的迹线。然后闭包（L）= a * b ^ ome​​ga + a ^ ome​​ga = L U {aaa ...}。 L中不包含无限多个a的踪迹，但是a ^ ome​​ga的每个有限前缀也是L中踪迹的前缀。因此a ^ ome​​ga包含在L的闭包中。

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

让L为安全性。我们必须证明L中的每个轨迹都包含在closure（L）中，反之亦然，closure（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是closure（L）的子集所具有的属性，而不仅仅是安全属性。

边注B：在闭包的示例中，我们注意到对于L = a * b ^ ome​​ga，我们具有闭包（L）= a * b ^ ome​​ga + a ^ ome​​ga。因此，L不等于closure（L），因此L不能成为安全属性。我们可以从轨迹a ^ ome​​ga看到这一点，该轨迹不在L中，但是没有错误的前缀，因为a ^ ome​​ga的每个有限前缀都具有a *形式，并且可以延续到a形式的轨迹* L的欧米茄。

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

旁注D：从您的原始问题和旁注C，我们可以得出结论，当且仅当L =闭包（L）时，L是安全属性。这使我们更好地理解了采用L闭包的含义：添加所有没有错误前缀的跟踪。此外，您可以验证采取封闭的封闭方式不会添加任何新的痕迹，因此对于任何L而言，它都持有该封闭（L）=封闭（封闭（L））。因此，对于任何L，它都认为closure（L）是安全属性。

Sidenote E：要回答您的评论问题，以获取一种等同于其关闭语言的示例：基于Sidenote D，我们可以采用任何安全性：考虑字母{a，b，c}上的语言L是L = {{a，b，c} ^ ome​​ga中的sigma | sigma没有c}。因此，错误的前缀将是所有带有c的有限单词（如果您将跟踪视为对某个程序的执行进行建模的对象，则c可能意味着“程序崩溃”，然后在其中执行随机操作）。我们可以验证L =闭包（L）：基于以上1.，我们已经知道L个子集闭包（L）。对于另一个方向，请考虑closure（L）中的迹线sigma。根据closure（L）的定义，sigma的每个有限前缀w必须是L中的跟踪sigma'的前缀。由于根据L的定义，sigma'不能包含c，因此w不能包含c。当sigma的每个有限前缀w不能包含c时，sigma不能包含c。因此，sigma在L中。我们得出L =闭包（L）的结论。