2

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

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

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

Q1:Kripke 结构可以在转换时设置守卫吗?

Q2:如果是,我如何在 NuSmv 中建模?

谢谢

4

1 回答 1

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,您可以在表达式中隐含防护。
于 2019-04-08T07:43:06.097 回答