Does spin reduce redundancies in LTL claims internally?

awesan · 2012-04-15 00:49:43

The following two claims are the same as (p -> !q) and its contrapositive (q -> !p) are equivalent in the propositional logic.

ltl p0a  { [] ((p -> !q) && (q -> !p)) }
ltl p0b  { [] (p -> !q) }

However, when I see the "never" claim (using spin -f), I do not see the simplified claim for "p0a". I am curious whether SPIN internally simplifies p0a to p0b before verification or it is user's responsibility to simplify claims?

spinroot · 2012-04-15 07:28:14

Spin will do some simplifications, but definitely not all possible ones....

awesan · 2012-04-15 08:00:26

Got it. Thanks. Just curious. In this particular example, is there a way to find out whether SPIN has done simplification of "p0a"? If the number of states stored, matched, transitions, memory usage, etc info reported by SPIN are exactly identical for both "p0a" and "p0b", does that indicate SPIN has reduced "p0a" to "p0b"?

spinroot · 2012-04-15 22:29:24

easy enough to check with spin -- just use spin -f 'formula' for each of these two ltl formula
and you'll see that the resulting never claim is identical

awesan · 2012-04-16 00:29:10

Nope. I tried that first; they are different for "spin -f". That's why I had to verify both claims to look at the output statistics. However, the never claims are same for "ltl2ba". Here is the output for both converters:

user : spin -f '!([] ((p -> !q) && (q -> !p)))'
never  {    /* !([] ((p -> !q) && (q -> !p))) */
T0_init:
	if
	:: (! (((p -> !q) && (q -> !p)))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

user : spin -f '!([] (p -> !q))'
never  {    /* !([] (p -> !q)) */
T0_init:
	if
	:: (! ((p -> !q))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

user : ltl2ba -f '!([] ((p -> !q) && (q -> !p)))'
never { /* !([] ((p -> !q) && (q -> !p))) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (p && q) -> goto accept_all
	fi;
accept_all:
	skip
}

user : ltl2ba -f '!([] (p -> !q))'
never { /* !([] (p -> !q)) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (p && q) -> goto accept_all
	fi;
accept_all:
	skip
}

Well, they are the same if the formula inside the "if" condition is expanded. It is just not obvious symbolically.

Last edited by awesan (2012-04-16 00:43:13)

spinroot · 2012-04-16 02:30:52

it may depend on the version of Spin -- with my version (6.1) I do get the same result in both cases:

$ spin -f '!([] ((p -> !q) && (q -> !p)))'
never { /* !([] ((p -> !q) && (q -> !p))) */
T0_init:
if
:: ((p) && (q)) -> goto accept_all
:: (1) -> goto T0_init
fi;
accept_all:
skip
}

awesan · 2012-04-16 04:00:10

hmmm. This is mysterious. I do have the same version. Here is the output of "spin -V" : Spin Version 6.1.0 -- 2 May 2011. I use http://spinroot.com/spin/Bin/spin610_linux on "Linux 3.0.0-12-generic-pae #20-Ubuntu SMP Fri Oct 7 16:37:17 UTC 2011 i686 i686 i386 GNU/Linux". I don't have a 64-bit machine to try it, but I would expect 64-bit to behave the same way as 32-bit. I am not sure whether building spin from sources using any special configuration parameters is required to get the simplification on LTL formula.

Spinroot

#1 2012-04-15 00:49:43

Does spin reduce redundancies in LTL claims internally?

#2 2012-04-15 07:28:14

Re: Does spin reduce redundancies in LTL claims internally?

#3 2012-04-15 08:00:26

Re: Does spin reduce redundancies in LTL claims internally?

#4 2012-04-15 22:29:24

Re: Does spin reduce redundancies in LTL claims internally?

#5 2012-04-16 00:29:10

Re: Does spin reduce redundancies in LTL claims internally?

#6 2012-04-16 02:30:52

Re: Does spin reduce redundancies in LTL claims internally?

#7 2012-04-16 04:00:10

Re: Does spin reduce redundancies in LTL claims internally?

Board footer