How to compare two LTLs?

问题:

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??

Thanks.

回答1:

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.)

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

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) }

(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? )

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

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).

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

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.

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.