automata - 如何比较两个 LTL？

Question

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

谢谢。

Answer 1

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

我们要检查是否 [] <> 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 中创建一个未初始化的变量？ ）

然后把它放在一个文件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查找最短示例），但它给出了警告。它确实找到了一个更短的周期。