logic - 模型检查：使用 NFA 的错误前缀

Question

我们使用 NFA 为安全属性建模 BadPrefixes。我想了解给定的安全属性，如何建模 NFA。

以下图片供参考。

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

标签： logicstatenfamodel-checking

Answer 1

我们这里有几个定义和符号，让我们先来看看这些：

• 我们得到一组原子命题 AP。这里没有明确说明，但这通常意味着我们对以字母表形式具有 AP 幂集的语言感兴趣。所以对于 AP = {a,b,c}，我们的字母表将是 Sigma = { {}, {a}, {b}, {c}, {a,b}, {a,c}, {b,c }, {a,b,c} }。

• 如您所见，写出这个幂集字母表可能需要做很多工作。出于这个原因，有一个基于命题公式的替代符号。考虑一个关于变量 AP 的命题公式 phi。我们可以从 Sigma 中取出一个符号 x，并在 phi 中将 x 中包含的所有原子命题设置为真，将所有其他原子命题设置为假。然后我们评估 phi，它变成真或假。我们可以将 phi 理解为指 Sigma 中所有那些 phi 评估为真的 x。

  例如，公式 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 and not b and not c" 仅指符号 {}。公式 phi="true" 指的是来自 Sigma 的所有符号。公式 phi="false" 表示没有符号（不要与符号 {} 混淆）。等等 ...

  此逻辑是您示例中 NFA 边缘上使用的符号。

• 如果存在接受 L 的 NFA，我们将有限词上的语言 L 称为“常规”。

• 如果不在 L 中的每条迹线都有一个坏前缀，即有限前缀 w，那么我们将无限迹线上的语言 L 称为“安全属性”，这样在 L 中就没有 w 的无限延续。

• 如果它的坏前缀的语言是常规的，我们将安全属性称为“常规”。请注意，我们在这里处理“常规”的两种不同概念，一种用于有限词的语言，另一种用于无限轨迹上的安全属性。

一般的做法

您正在处理从对安全属性的非正式描述到对其坏前缀语言的正式描述的问题。没有关于如何做到这一点的一般规则，但请记住，在直观层面上，安全属性意味着“某些不良事件永远不会发生”。坏前缀的语言正是那些“坏事件发生在某个时刻”的有限词。因此，您的方法是分析“坏事件”是什么。

（当然，这是模型检查中的一个普遍问题，当从非正式描述转换为正式模型时，存在无法完美捕捉原始描述的风险。）

考虑 P1：坏事件是“a 变为有效，然后 b 仅在有限多步内有效，并且在 c 变为真之前变为假”。我们可以把它变成一个稍微冗长的描述：“a 变为有效，之后我们看到一些 b 没有 c，然后我们看到没有 b 和没有 c”。我们可以使用这个描述来推导出“坏事件发生在某个时刻”的正式定义。我个人觉得正则表达式比 NFA 更直观，所以我会先尝试构建一个正则表达式，然后再从中构建 NFA：

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

这个正则表达式描述了在某些时候发生坏事件的所有有限词。我们在开头和结尾使用 (true)*，因为我们不关心坏事件之前或之后发生的事情。在您的示例中，正则表达式已经非常接近 NFA，一般来说，从这样的正则表达式构建 NFA 应该很容易。您可以看到，与显式写出符号相比，基于命题公式的符号更紧凑，例如写“a”比写完整的正则表达式 ({a} + {a,b} + {a, c} + {a,b,c})。

这不是唯一的解决方案，而不是要求在看到（不是 b 而不是 c）之前看到（b 而不是 c）*，在看到（不是 b 而不是 c）之前要求看到（不是 c）* 也足够了）。这将导致正则表达式：

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

与第一个解决方案的唯一区别是，我们不需要匹配我们看到的第一个（不是 b 和不是 c），我们还可以跳过一些（不是 b 和不是 c），因为它们也匹配（不是 c） ，只要我们最终匹配 a（不是 b 也不是 c）。所以在某种程度上，第一个解决方案是更好的解决方案，因为由此产生的 NFA 更具确定性。

考虑 P2：坏事件是有两个 a，使得在某个点之间 b 不成立。把它变成一个稍微详细一点的描述，我们会得到“我们看到 a，然后我们看到一些 b 而没有看到 a，然后我们到达一个点，我们既看不到 b 也看不到 a，然后我们看到任何符号，直到我们到达结束 a ”。把它变成“坏事件在某个时候发生”的正则表达式给我们：

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

同样，这与您示例中的 NFA 非常相似，应该很容易看出如何从这样的表达式构造 NFA。和以前一样，我们也可以获得替代解决方案，通过将 (b and not a)* 放宽到 (not a)*，唯一的区别是这将允许跳过一些 (not b and not a)，只要因为我们最终匹配了一个。此外，我们可以将中间 (true)* 加强为 (not a)*，要求我们匹配第一个结束 a，而不是允许在匹配结束 a 之前跳过一些 a：

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

关于状态数

既然你问如何知道状态数：我会先尝试获得一些 NFA，然后检查它是否可以简化。对于您示例中的 NFA，我认为没有办法进一步减少状态数量，但总的来说，最小化 NFA 是一个难题（参考），因此没有有效的算法。当然，如果你得到一个完全确定的自动机，你可以应用标准算法来最小化 DFA。