问模型检验:安全性和活性特性

EN

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

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

对于给定的语言L，语言闭包( L )被定义为由所有的跟踪组成，其中每个有限前缀也是L中一个跟踪的前缀。

取闭包的标准示例是L= a*b^omega ={bbb.，abbb.，aabbb.，aabbb.}。语言L包含具有有限前缀a's然后无限多b's的所有迹，然后闭包(L)= a*b^omega + a^omega =L U{aaa.}。无限多a的迹不包含在L中，而a^omega的每一个有限前缀在L中也是迹的前缀，因此a^omega包含在L的闭包中。

现在你的问题是为什么对于一个安全性质L，它认为L=闭包(L)。

让我成为一个安全的财产。我们必须证明L中的每一条迹都包含在闭包(L)中，反之亦然，闭包(L)中的每一条迹都包含在L中。

1. L中的每一个迹都包含在闭包(L)中:考虑L中的一个迹σ，则σ的每个有限前缀都是σ的前缀。因此，σ的每一个有限前缀都是L中迹的前缀。根据闭包(L)的定义，σ在闭包(L)中的closure(L).
2. Every迹包含在L中:设σ在闭包(L)中。假设σ不存在于L中，根据安全性质的定义，σ有一个有限的前缀w，使得w在L中没有无限连续，但w不能是L中一个词的前缀，但是根据闭包( L )的定义，σ的每一个有限前缀都必须处于L的矛盾中。由于西格玛不在L中的假设导致矛盾，因此西格玛在L.

中。

Sidenote :请注意，对于1.我们没有使用L是一个安全属性。一般情况下，L是闭包(L)的子集，而不仅仅是为了安全属性。

Sidenote :在闭包的例子中，我们注意到对于L= a*b^omega，我们有闭包(L)= a*b^omega + a^omega。因此L不等于闭包(L)，所以L不能是一个安全属性。我们可以从跟踪a^omega中看出这一点，它不在L中，但没有坏前缀，因为a^omega的每个有限前缀都是a*，并且可以继续跟踪a*b^omega在L中的形式。

Sidenote :我们也可以问相反的问题，当L=闭包(L)时，L是安全属性吗？答案是肯定的。设L是L=闭包(L)的语言。考虑不在L中的跟踪西格玛，我们必须证明sigma有一个糟糕的前缀。按L=闭包(L)，则σ不处于闭包(L)。根据闭包( L )的定义，如果σ的所有有限前缀都在L中，则闭包(L)中有σ。因此，从无闭包(L)的σ开始，可以得到σ的某些有限前缀w，使得L中的所有迹σ‘都没有w作为前缀。换句话说，w的每一个无限连续在L中都不可能是一个迹，因此w是一个坏前缀。总之，每个不在L中的跟踪σ都有一个不好的前缀，因此L是一个安全属性。

D:从你最初的问题和赛德诺特C，我们可以得出结论，L是一个安全属性当且仅当L=闭包(L)。这提高了我们对L的闭包含义的理解:添加所有没有坏前缀的跟踪。此外，您可以验证闭包没有添加任何新的跟踪，因此对于任何L，它都认为闭包(L)=闭包(闭包(L))。因此，对于任何L，它认为闭包(L)是一个安全属性。

Sidenote :要回答与其闭包相等的语言示例的注释问题:基于Sidenote，我们可以采取任何安全属性:考虑字母表{a，b，c}上的语言L，即L= {a，b，c }中的{ sigma，在{a，b，c}^omega =c}中没有c}。因此，糟糕的前缀都是带有c的有限单词(如果您将跟踪看作是对某个程序的执行进行建模，那么c可能意味着“程序崩溃了”，然后做一些随机的事情)。我们可以验证L=闭包(L)：我们已经知道L子集闭包(L)是基于上面的1。对于另一个方向，考虑闭包中的跟踪西格玛(L)。根据闭包( L )的定义，σ的每个有限前缀w都必须是L中迹σ‘的前缀，因为根据L的定义，σ’不能包含c，所以w不能包含c，当σ的每一个有限前缀w不能包含c时，σ不包含c，因此σ在L中，我们得出L=闭包(L)。