如何比较两个零担? [英] How to compare two LTLs?

问题描述

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

How can I compare two LTLs to see if one can contradict each other? I ask this because I have a hierarchical state machine and LTLs describing the behavior in each state. I need to know if a local LTL can contradict a global LTL. I saw in the Article 'Feature Specification and Automated Conflict Detection' that two LTLs properties f and g are inconsistent iff L(f) intersection L(g) is empty. And this is exactly the model checking question with f as the program and ¬g as the property. Can anyone help me with this? How can I transform an LTL f into a program in SPIN/Promela??

谢谢.

推荐答案

以下内容对我有用. (警告:我尚未在官方文档中看到此信息.这可能意味着还有其他更好的方法可以做到这一点.或者我看上去不够努力.)

The following works for me. (Warning: I've not seen this in official documentation. This could mean that there are other, better ways to do this. Or that I didn't look hard enough.)

我们要检查[] <> p && [] <> q是否暗含<> (p && q). (不是).

We want to check whether [] <> p && [] <> q implies <> (p && q). (It does not.)

编写一个可以进行所有转换的琐碎流程P，并将声明写为LTL属性A.

Write a trivial process P that can do all transitions, and write the claim as an LTL property 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日:这可能是不正确的，因为我们可能由于隐藏的初始状态而缺少某些过渡，请参见

(EDIT 1-Nov-2016: this may be incorrect because we might be missing some transitions because of a hidden initial state, see how to make a non-initialised variable in Spin? )

然后将其放入文件check.pml，然后

Then put this in a file check.pml, and

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

展示了一个否定索赔的模型(最终周期性的踪迹，其中p和q经常无限地成立，而p && q从未如此).

shows a model of the negation of the claim (an ultimately periodic trail where p and q are true infinitely often, but p && q is never).

仔细检查:将权利要求中的结论更改为<> (p || q)，然后没有反例，证明该暗示是有效的.

Double-check: change the conclusion in the claim to <> (p || q), then there is no counter-examle, proving that the implication is valid.

在您的情况下，声明为! (f && g)(它们永远不应同时为真).

In your case, the claim is ! (f && g) (they should never be true at the same time).

可能有一些巧妙的方法可以使琐碎过程的代码更小.

There probably is some clever way to make the code for the trivial process smaller.

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

Also, the third command is actually ./pan -a -i -n (the -i to find a shortest example) but it gives a warning. And it does find a shorter cycle.

这篇关于如何比较两个零担?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！