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.
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 propertyA
.(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
, andshows a model of the negation of the claim (an ultimately periodic trail where
p
andq
are true infinitely often, butp && 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.