如何比较两个LTL？

如何比较两个LTL以查看是否可以相互抵触？我问这是因为我有一个分层状态机和描述每个状态行为的LTL。我需要知道本地零担可以抵制全球零担。我在文章'Feature Specification and Automated Conflict Detection'中看到，如果L（f）交点L（g）为空，则两个LTL属性f和g不一致。这正是用f作为程序和作为属性的模型检查问题。谁能帮我这个？如何将LTL f转换为SPIN/Promela中的程序？如何比较两个LTL？

谢谢。

来源

2015-11-02 Georgia

以下适用于我。（警告：我在官方文档中没有看到这一点，这可能意味着还有其他更好的方法可以做到这一点，或者说我看起来不够硬。）

我们想检查是否[] <> 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找到一个最短的例子），但它会给出警告。它确实找到了更短的周期。

来源

2015-11-05 19:26:13 d8d0d65b3f7cf42

非常感谢您的帮助。我测试了索赔（[]（p && q））&&（<>！（p）），其中f是[]（p && q），g是<>！（p）。对我来说，这两个LTL是矛盾的，因为！p会与[p]相矛盾。当我测试自旋向我显示消息：“错误：断言违反旋转：断言失败的文本：assert（！（！（（p && q））））”并没有向我展示反例。我做错了什么？ – Georgia

你是从命令行（正如我写的）运行它，还是在ispin或其他一些GUI中运行？ – d8d0d65b3f7cf42

我从ispin图形用户界面运行... – Georgia

如何比较两个LTL？

回答

相关问题