verification - Kripke 结构可以有守卫吗?
问题描述
我有一个简单的 kripke 结构,其中有 3 个状态,具有以下转换:
s1 --> s2
s2 --> s1
s1 --> s3
s3 --> s3
s1 是唯一的初始状态。我不希望循环 s1 到 s2 重复超过一定数量(比如两次)。在其他过渡系统中,我可以在过渡中添加一个守卫。
Q1:Kripke 结构可以在转换时设置守卫吗?
Q2:如果是,我如何在 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]
这实际上是一个[v=1]
不包含任何守卫的 Kripke 结构(作为唯一的初始状态并且没有在节点上定义任何标签)。
更新:每个节点的标签集的示例是所有在此处计算为 true 的布尔表达式。
总结一下你的两个问题:
- 不,Kripke 结构本身没有警卫。
- 尽管如此(正如所解释的,Kripke 结构中没有守卫并不意味着模型中一定没有守卫),我认为您可以将 case 语句中的条件视为冒号行动权的守卫。或者使用 TRANS,您可以在表达式中隐含防护。
推荐阅读
- python - 使用 spyder 4 在不同笔记本电脑上运行相同代码的问题
- css - 当内容较大时,垂直居中 div 而不会溢出
- firebase - 调度时间少于 1 分钟的 Firebase 计划函数
- android - Mockito 3.4.0 静态模拟异常
- python - Python Celery 自动缩放 Kubernetes
- mysql - 拉拉维尔。无法将带空格的数据插入数据库。语法错误 1064
- abap - FOR ALL ENTRIES 通过空的 itab 选择数据库中的所有记录
- visual-studio - 在winform图表y系列中使用表达式
- java - HAProxy1.7 转发客户端IP到后端
- sql - 选择某些元组列表中出现 2 列值的行