我必须在 NuSMV 中创建 Kripke 的结构,并且我必须检查一些属性。
有人帮我吗?结构和特性(LTL、CTL 和 CTL*)在图片中。
这里有一个结构和性质:
http://cl.ly/image/1x0b1v3E0P0D/Screen%20Shot%202014-10-16%20at%2016.52.34.png
我必须在 NuSMV 中创建 Kripke 的结构,并且我必须检查一些属性。
有人帮我吗?结构和特性(LTL、CTL 和 CTL*)在图片中。
这里有一个结构和性质:
http://cl.ly/image/1x0b1v3E0P0D/Screen%20Shot%202014-10-16%20at%2016.52.34.png
我为您的 Kripke 结构找到了一个更简单且看似更可靠的 NuSMV 代码。感谢dejvuth对我的问题的回答。代码如下
MODULE main
VAR
state : {s0,s1,s2,s3,s4};
ASSIGN
init(state) := s0;
next(state):=
case
state = s0 : {s1,s2};
state = s1 : {s1,s2};
state = s2 : {s1,s2,s3};
state = s3 : {s1,s4};
state = s4 : {s4};
esac;
DEFINE
p := state = s1 | state = s2 | state = s3 | state = s4;
q := state = s1 | state = s2;
r := state = s3;
SPEC
EG p;
SPEC
AG p;
SPEC
EF (AG p);
据我所知,NuSMV 仅处理 LTL 和 CTL 公式(请参阅Wikipedia 中的 NuSMV)。问题 1-3 中的公式是 CTL 公式,因此可以通过 NuSMV 进行模型检查。然而,问题 4 和 5 中的公式是 CTL* 公式,因此我们不能直接将它们用作 NuSMV 的输入。您还需要了解所有 CTL* 公式的集合是所有 LTL 和 CTL 公式并集的正确超集。这种情况意味着某些 CTL* 公式没有等效的 LTL 或 CTL 公式(请参阅Wikipedia 中的 CTL*)。您的 Kripke 结构可以通过以下代码在 NuSMV 中定义:
MODULE main
VAR
p : boolean;
q : boolean;
r : boolean;
state : {s0,s1,s2,s3,s4};
ASSIGN
init (state) := s0;
next (state) :=
case
state = s0 : {s1, s2};
state = s1 : {s1, s2};
state = s2 : {s1, s2, s3};
state = s3 : {s1, s4};
state = s4 : {s4};
TRUE : state;
esac;
init (p) := FALSE;
init (q) := FALSE;
init (r) := FALSE;
next(p) :=
case
state = s1 | state = s2 | state = s3 | state = s4 : TRUE;
TRUE : p;
esac;
next(q) :=
case
state = s1 | state = s2 : TRUE;
state = s3 | state = s4 : FALSE;
TRUE : q;
esac;
next(r) :=
case
state = s3 : TRUE;
state = s1 | state = s2 | state = s4 : FALSE;
TRUE : r;
esac;
SPEC
EG p;
SPEC
AG p;
SPEC
EF (AG p);
当然,还有另一种方法可以在 NuSMV 中定义 Kripke 结构,但我认为这是最简单的方法之一。(无论如何,感谢您帮助我解决问题)。
至于问题 4 和 5 中的公式,这是我的答案。
公式AF [p U EG ( p -> q)]的形式为AF [\phi],其中\phi是 LTL 公式p U EG (p->q)。由于 LTL 公式\phi在 Kripke 模型中得到满足,如果对于从 s0 开始的每条路径我们都满足\phi,那么我们将AF [p U EG ( p -> q)]转换为AF A[p U EG ( p -> q)]。
通过类似的论点,我们将EG[(( p & q ) | r) U (r U AG p)]翻译成EG[A(( p & q ) | r) UA( r U AG p)]。