Spinroot

My initial question was: "Is it safe to use a simple DFS to check safety LTL properties?" By this I meant that the formula specified as "ltl name {formula}" in a Promela model is a safety property.

I would be very surprised if when using the '-DSAFETY' option or when referring to safety properties in the man pages, it means that the negation of the desired property is safety, because then to check invariants one would need the -a option (because their negation is not a safety, but a liveness property)!

Well, for ltl prop {p W q} (or equivalently spin -f "! ( ([] p) || (p U q))"), SPIN generates a never-claim that has non-dummy accept labels, but I believe it doesn't need -a to fully verify, because all infinite accepted traces have a finite prefix for which the never-claim finishes.

Actually my question is not whether the algorithms are correct, but rather which are the algorithms used. More precisely: never-claims are more powerful than Buchi automata, because they also accept finite traces, while Buchi automata only accept infinite traces. The papers I have seen only talk about how to generate Buchi automata, not never-claims. For instance, for ! (p W q), the Buchi automata could look (as a never-claim), like this:

never { 
T0_init :    /* init */
	if
	:: (!q) -> goto T0_init
	:: (!p && !q) -> goto accept_all
	fi;
accept_all :    /* 1 */
	if
	:: (1) -> goto accept_all
        fi
}

but SPIN generates a never-claim which looks like this:

never { /* ! ( ([] p) || (p U q)) */
T0_init :    /* init */
	if
	:: (!q) -> goto T0_init
	:: (!p && !q) -> goto accept_all
	fi;
accept_all :    /* 1 */
	skip
}

(I used here the ltl2ba tool just to keep the automaton smaller; I could have used SPIN instead to illustrate the same issue.)

Now, concerning correctness: if the only transformation from the (non-terminating) Buchi automata to (the possibly terminating) never-claims is the addition of jumps to the end of the never-claim, then I have reasons to believe that this is not sufficient: Kupferman and Vardi in "Model Checking of Safety Properties" (CAV'99) show that one needs to determinize the Buchi automaton obtained from the LTL formula, in order to obtain a finite automaton that detects all bad prefixes. (Unfortunately, they don't give the concrete LTL formula which shows this, they only give a similar one, which is complicated enough, see Theorem 3.3.) Without this determinization step, I think that there are safety LTL formulas for which SPIN's translation (and actually all translations) would generate a never-claim that never terminates and hence for which SPIN will not find errors only by doing a simple DFS.

No. But I just imagine that further transformations are needed besides the theoretical LTL to NBA translation (and the above mentioned inverse of the stutter extension rule). So I am just curious how SPIN builds the never-claim. For instance, I know that one can transform a safety NBA into an NFA that accepts all good prefixes, by applying the powerset construction. Is this what is done?

Another reason for which I asked is that, besides the match between the names (safety option and safety property), I haven't seen a place where it is said that it is safe to do so.

I refine my question: Is it safe to use a simple DFS (that is, the -DSAFETY option) to check safety LTL properties?

I think I've finally got it. Actually the same behavior is exhibited by the following program:

int x;
ltl p { <> (x == 1)}
init { 0; x = 1; }

which clearly deadlocks/blocks. As explained on page 130 of the SPIN book (Ch.6, The stutter extension rule), for finite traces, the last state is stuttered, in order to obtain an infinite trace. Then everything makes sense.

This explanation also appears at [url]http://spinroot.com/spin/Man/progress.html[/url]:
[quote]
The standard stutter-extension, to extend finite execution sequences into infinite ones by stuttering (repeating) the final state of the sequence, is applied in the detection of all standard types of acceptance properties, but it is not used for non-progress cycles.
[/quote]
But it does not appear on [url]http://spinroot.com/spin/Man/accept.html[/url] or [url]http://spinroot.com/spin/Man/ltl.html[/url]. Thus I would say that these pages are rather misleading with regard to the treatment of finite traces.