如何比较两个LTL?
问题描述:
如何比较两个LTL以查看是否可以相互抵触?我问这是因为我有一个分层状态机和描述每个状态行为的LTL。我需要知道本地零担可以抵制全球零担。我在文章'Feature Specification and Automated Conflict Detection'中看到,如果L(f)交点L(g)为空,则两个LTL属性f和g不一致。这正是用f作为程序和作为属性的模型检查问题。谁能帮我这个?如何将LTL f转换为SPIN/Promela中的程序?如何比较两个LTL?
谢谢。
答
以下适用于我。 (警告:我在官方文档中没有看到这一点,这可能意味着还有其他更好的方法可以做到这一点,或者说我看起来不够硬。)
我们想检查是否[] <> p && [] <> q
意味着<> (p && q)
。 (不。)
写一个简单的过程P
可以做所有转换,并将该索赔编写为LTL属性A
。
bool p; bool q;
active proctype P() {
do :: d_step { p = false; q = false }
:: d_step { p = false; q = true }
:: d_step { p = true; q = false }
:: d_step { p = true; q = true }
od
}
ltl A { (([] <> p) && ([] <> q)) -> <> (p && q) }
(编辑1 - 11月 - 2016年这可能是不正确的,因为我们可能会因为缺少一个隐藏的初始状态的一些转变,看到how to make a non-initialised variable in Spin?)
然后把这个文件check.pml
,并
spin -a check.pml
cc pan.c -o pan
./pan -a -n
./pan -r check.pml.trail -v
示出了权利要求的否定的模型(一个最终周期性线索其中p
和q
为真无限频繁,但p && q
是从不)。
仔细检查:将索赔中的结论更改为<> (p || q)
,则不存在反证,证明其含义是有效的。
在你的情况下,索赔是! (f && g)
(他们不应该在同一时间)。
可能有一些聪明的方法可以使得平凡过程的代码变小。
此外,第三个命令实际上是./pan -a -i -n
(-i
找到一个最短的例子),但它会给出警告。它确实找到了更短的周期。
非常感谢您的帮助。我测试了索赔([](p && q))&&(!(p)),其中f是[](p && q),g是!(p)。对我来说,这两个LTL是矛盾的,因为!p会与[p]相矛盾。当我测试自旋向我显示消息:“错误:断言违反 旋转:断言失败的文本:assert(!(!((p && q))))”并没有向我展示反例。我做错了什么? – Georgia
你是从命令行(正如我写的)运行它,还是在ispin或其他一些GUI中运行? – d8d0d65b3f7cf42
我从ispin图形用户界面运行... – Georgia