verification - Kripke 结构可以有守卫吗？

Question

我有一个简单的 kripke 结构，其中有 3 个状态，具有以下转换：

s1 --> s2
s2 --> s1
s1 --> s3
s3 --> s3

s1 是唯一的初始状态。我不希望循环 s1 到 s2 重复超过一定数量（比如两次）。在其他过渡系统中，我可以在过渡中添加一个守卫。

Q1：Kripke 结构可以在转换时设置守卫吗？

Q2：如果是，我如何在 NuSmv 中建模？

谢谢

Answer 1

你在这里比较苹果和橘子。带有守卫的模型（例如在 NuSMV 中）定义了一个状态空间，它又可以被视为 Kripke 结构（让我们在这里忽略像死锁这样的问题）。

守卫是建模方法的一个元素，而 Kripke 结构是用于描述状态空间的基本理论概念。

举个例子：我们有一个模型，它有一个变量v，可以取两个值 1 和 2，初始值为 1，还有两个带保护的转换：

a == WHEN v=1 THEN v:=2
b == WHEN v=2 THEN v:=1

结果状态空间将是：

[v=1] --> [v=2]
[v=2] --> [v=1]

这实际上是一个[v=1]不包含任何守卫的 Kripke 结构（作为唯一的初始状态并且没有在节点上定义任何标签）。

更新：每个节点的标签集的示例是所有在此处计算为 true 的布尔表达式。

总结一下你的两个问题：

1. 不，Kripke 结构本身没有警卫。
2. 尽管如此（正如所解释的，Kripke 结构中没有守卫并不意味着模型中一定没有守卫），我认为您可以将 case 语句中的条件视为冒号行动权的守卫。或者使用 TRANS，您可以在表达式中隐含防护。