我有一个简单的 kripke 结构，其中有 3 个状态，具有以下转换：
s1 --> s2
s2 --> s1
s1 --> s3
s3 --> s3
s1 是唯一的初始状态。我不希望循环 s1 到 s2 重复超过一定数量（比如两次）。在其他过渡系统中，我可以在过渡中添加一个守卫。
Q1：Kripke 结构可以在转换时设置守卫吗？
Q2：如果是，我如何在 NuSmv 中建模？
谢谢
【问题讨论】：
标签： verification model-checking nusmv
您在这里比较苹果和橙子。带有守卫的模型（例如在 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]
这实际上是一个不包含任何守卫的 Kripke 结构（[v=1] 作为唯一的初始状态，并且没有在节点上定义任何标签）。
更新： 每个节点的标签集的示例是所有在此处计算为 true 的布尔表达式。
总结一下你的两个问题：
【讨论】：