如何比较两个 LTL？

如何比较两个 LTL 以确定其中一个是否可以相互矛盾？我问这个问题是因为我有一个分层状态机和描述每个状态下行为的 LTL。我需要知道本地零担是否可以与全局零担相矛盾。我在“功能规范和自动冲突检测”一文中看到，如果 L(f) 交集 L(g) 为空，则两个 LTL 属性 f 和 g 不一致。这正是以 f 为程序、 Øg 为属性的模型检验问题。谁能帮我这个？如何将 LTL f 转换为 SPIN/Promela 中的程序？

Thanks.

以下内容对我有用。 （警告：我没有在官方文档中看到这一点。这可能意味着还有其他更好的方法可以做到这一点。或者我没有仔细寻找。）

我们想检查是否[] <> 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) }

（编辑 2016 年 11 月 1 日：这可能不正确，因为由于隐藏的初始状态，我们可能会丢失一些转换，请参阅如何在 Spin 中创建未初始化的变量？ https://stackoverflow.com/questions/40358915/how-to-make-a-non-initialised-variable-in-spin )

然后将其放入文件中check.pml, and

spin -a check.pml
cc     pan.c   -o pan
./pan -a -n
./pan -r check.pml.trail -v

显示了否定声明的模型（最终的周期性轨迹，其中p and q无限频繁地为真，但是p && q是从来没有）。

仔细检查：将权利要求中的结论更改为<> (p || q)，则不存在反例，证明蕴涵成立。

就您而言，索赔是! (f && g)（它们永远不应该同时为真）。

可能有一些聪明的方法可以使琐碎过程的代码更小。

另外，第三个命令实际上是./pan -a -i -n (the -i找到一个最短的例子）但它给出了一个警告。而且它确实找到了更短的周期。