模型检查:使用NFA的错误前缀 [英] Model Checking : Bad Prefixes using NFA

问题描述

我们使用NFA为安全属性建模BadPrefixes.我想了解给定安全属性的NFA建模方法.

We use NFA to model BadPrefixes for the safety property.I want to understand for a given Safety property , how to model the NFA.

以下图像仅供参考.

The following images are for reference.

例如，对于安全属性P2，有人可以解释如何知道需要多少个状态(解决方案有4个)以及在边上使用哪种逻辑，在图3和图4中，边如何选择满足不良前缀P1和P2.谢谢.

For instance, for safety property P2 ,Can someone explain how to know how many states are required(solution has 4) and which logic to use on the edges, how in Fig.,3 and Fig.4 , the edges are selected to satisfy the badprefixes P1 and P2.Thanks.

推荐答案

在这里，我们有几个定义和符号，让我们首先看一下这些:

We have several definitions and notations here, let's go through these first:

• 我们获得了一组原子命题AP.这里没有明确说，但是通常这意味着我们对以AP的幂集为字母的语言感兴趣.因此，对于AP = {a，b，c}，我们的字母为Sigma = {{}，{a}，{b}，{c}，{a，b}，{a，c}，{b，c }，{a，b，c}}.

• We are given a set of atomic propositions AP. It is not said here explicitly, but usually this means we are interested in languages that have as alphabet the power set of AP. So for AP = {a,b,c}, our alphabet would be Sigma = { {}, {a}, {b}, {c}, {a,b}, {a,c}, {b,c}, {a,b,c} }.

如您所见，写出此幂集字母可能需要很多工作.因此，存在基于命题公式的替代表示法.考虑变量AP的命题公式phi.我们可以取一个来自Sigma的符号x，并在phi中将x中包含的所有原子命题设置为true，并将所有其他原子命题设置为false.然后我们评估phi，它变为true或false.我们可以理解phi指的是Sigma中所有phi评估为true的x.

As you can see, writing out this power set alphabet can be a lot of work. For this reason, there is an alternative notation based on propositional formulas. Consider a propositional formula phi over the variables AP. We can take a symbol x from Sigma and in phi set all atomic propositions contained in x to true and all other atomic propositions to false. Then we evaluate phi and it becomes true or false. We can understand phi to refer to all those x from Sigma for which phi evaluates to true.

例如，公式phi ="a and not b"表示符号{a}和{a，c}.公式phi ="a"表示符号{a}，{a，b}，{a，c}，{a，b，c}.公式phi ="not a"表示符号{}，{b}，{c}，{b，c}.公式phi ="not a a not not b and not c"仅表示符号{}.公式phi ="true"表示Sigma中的所有符号.公式phi ="false"表示没有符号(请勿与符号{}混淆).等等...

For example, the formula phi="a and not b" refers to the symbols {a} and {a,c}. The formula phi="a" refers to the symbols {a},{a,b},{a,c},{a,b,c}. The formula phi="not a" refers to the symbols {},{b},{c},{b,c}. The formula phi="not a and not b and not c" refers only to the symbol {}. The formula phi="true" refers to all symbols from Sigma. The formula phi="false" refers to no symbol (not to be confused with the symbol {}). And so on ...

此逻辑是示例中NFA边缘上使用的表示法.

This logic is the notation used on the NFA edges in your example.

如果存在接受L的NFA，我们将有限词上的语言L称为常规".

We call a language L over finite words "regular" if there is a NFA that accepts L.

如果不在L中的每条跟踪都有一个错误的前缀(即有限前缀w)，使得L中没有w的无限连续，我们将在无穷迹上的语言L称为安全属性".

We call a language L over infinite traces a "safety property" if every trace not in L has a bad prefix, meaning a finite prefix w, such that no infinite continuation of w is in L.

如果其错误前缀的语言是常规的，则我们将安全属性称为常规".请注意，我们在这里处理两种不同的常规"概念，一种是用于有限词的语言，另一种是在无限轨迹上的安全性.

We call a safety property "regular" if the language of its bad prefixes is regular. Note we are dealing with two different notions of "regular" here, one for languages of finite words and one for safety properties over infinite traces.

您正在处理从对安全性资产的非正式描述到对它的错误前缀的语言进行正式描述的问题.这样做没有一般性规则，但是请记住，在直观的水平上，安全属性表示永远不会发生某些不良事件".那么，不良前缀的语言就是那些不良事件在某个时刻发生"的有限词.因此，您的方法是分析不良事件"是什么.

You are dealing with the problem of going from an informal description of a safety property to a formal description of the language of its bad prefixes. There is no general rule for how to do this, but remember that on an intuitive level, a safety property means "some bad event never happens". The language of the bad prefixes is then exactly those finite words for which "the bad event happens at some point". Your approach would therefore be to analyze what the "bad event" is.

(当然，这是模型检查中的一个普遍问题，当从非正式描述转到正式模型时，存在无法完全捕获原始描述的风险.)

(This is a general problem in model checking of course, when going from informal descriptions to a formal model there is a risk of not perfectly capturing the original description.)

考虑P1:不良事件是"a变为有效，然后b仅在有限的多个步骤中才有效，并且在c变为true之前变为false".我们可以将其转换为更为冗长的描述:"a变为有效，之后我们看到一些b，但是没有c，然后我们看到没有b和c".我们可以使用此描述来得出不良事件在某个时刻发生"的正式定义.我个人认为正则表达式比NFA更直观，因此我将首先尝试构建正则表达式，然后再从中构建NFA:

Consider P1: The bad event is "a becomes valid and afterwards b is valid only finitely many steps and becomes false before c becomes true". We can turn this into a slightly more verbose description: "a becomes valid, afterwards we see some b's but no c's and then we see no b and no c". We can use this description to derive a formal definition for "the bad event happens at some point". I personally find regular expressions more intuitive than NFAs, so I would first try to build a regular expression and then build the NFA from that afterwards:

(true)* a (b and not c)* (not b and not c) (true)*

此正则表达式描述了在某些情况下发生不良事件的所有有限词.我们在开始和结束时都使用(true)*，因为我们不在乎不良事件之前或之后发生的事情.在您的示例中，正则表达式已经非常接近NFA，通常应该很容易从此类正则表达式构建NFA.您可以看到，与明确地写出符号(例如，符号)相比，基于命题公式的符号使这一过程更加紧凑.写"a"比写完整的正则表达式({a} + {a，b} + {a，c} + {a，b，c})要短.

This regular expression describes all finite words where at some point the bad event happens. We use the (true)* at the beginnging and the end because we do not care what happens before or after the bad event. The regular expression is already very close the NFA in your example, in general it should be easy to build NFAs from such regular expressions. You can see that the notation based on propositional formulas makes this much more compact compared to writing out the symbols explicitly, e.g. writing "a" is shorter than writing the full regular expression ({a} + {a,b} + {a,c} + {a,b,c}).

这不是唯一的解决方案，而不是要求先看到(b和非c)*，然后再看到(不是b和非c)*，也需要先看到(非c)*，然后再看到(非b)而不是c).这将导致正则表达式:

This is not the only solution, instead of requiring to see (b and not c)* before seeing (not b and not c), it would also suffice to require to see (not c)* before seeing (not b and not c). This would result in the regular expression:

(true)* a (not c)* (not b and not c) (true)*

与第一个解决方案的唯一区别在于，我们无需跳过某些匹配的(而不是b和c)，而不是匹配我们看到的第一个(不是b和c).不是c)，只要我们最终匹配a(不是b而不是c).因此，从某种意义上说，第一种解决方案是更好的解决方案，因为生成的NFA更具确定性.

The only difference to the first solution would be that instead of requiring to match the first (not b and not c) we see, we could also skip over some (not b and not c)'s because they also match (not c), as long as we match a (not b and not c) eventually. So in a way the first solution is the better one because the resulting NFA is more deterministic.

考虑P2:不好的事件是有两个a，使得在某个点之间的b不成立.将其变成稍微冗长的描述，我们将得到我们看到一个a，之后我们看到一些b而没有看到a，然后我们到达一个既看不到b也不看到a的点，之后我们看到了任何符号，直到到达结尾a ".将其转换为不良事件在某个时刻发生"的正则表达式可以使我们:

Consider P2: The bad event would be having two a's such that in between at some point b does not hold. Turning this into a slightly more verbose description, we would get "we see a, afterwards we see some b's without seeing a, then we reach a point where we see neither b nor a, afterwards we see any symbols until we reach the closing a". Turning this into a regular expression for "the bad event happens at some point" gives us:

(true)* a (b and not a)* (not b and not a) (true)* a (true)*

同样，这与您的示例中的NFA非常相似，应该很容易看出如何从这样的表达式构造NFA.与以前一样，我们也可以通过将(b和非a)*放宽到(非a)*，获得唯一的解决方案，唯一的区别是，只要允许跳过某些(非b和非a)，就可以当我们最终匹配一个.另外，我们可以将中间(true)*增强为(不是a)*，这要求我们匹配第一个闭合a，而不是允许在匹配闭合a之前跳过一些a:

Again this is very similar to the NFA in your example, it should be easy to see how to construct an NFA from such an expression. As before we could also obtain an alternative solution, by relaxing the (b and not a)* to (not a)*, the only difference would be that this would allow to skip over some (not b and not a), as long as we match one eventually. Also, we could strengthen the middle (true)* to (not a)*, requiring us to match the first closing a instead of allowing to skip over some a's before matching the closing a:

(true)* a (not a)* (not b and not a) (not a)* a (true)*

关于国家数量

由于您询问了如何知道状态数:我将首先尝试获取一些NFA，然后检查它是否可以简化.对于您示例中的NFA，我看不到进一步减少状态数量的方法，但是总的来说，最小化NFA是一个难题(

Regarding the number of states

Since you asked about how to know the number of states: I would first try to obtain some NFA and then check if it can be simplified. For the NFAs in your example, I see no way to further reduce the number of states, but in general minimizing NFAs is a hard problem (reference), so there is no efficient algorithm for that. Of course, if you obtain a fully deterministic automaton, you can apply the standard algorithm for minimizing DFAs.

这篇关于模型检查:使用NFA的错误前缀的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！