LTL and never-claims

eugen · 2011-12-20 18:26:32

My initial understanding was that never-claims generated from LTL formulas should never terminate as they encode Buchi automata, or equivalently, as the standard LTL semantics is on infinite words.

But for instance for pWq, the never claim can terminate. So how is a never-claim generated from an NBA? (I assume that the NBA is obtained from the LTL formula using the algorithm described in "Simple on-the-fly automatic verification of linear temporal logic".) Is it the case that all accepting "sink" states are transformed into the 'accept_all: skip' final statement of the never-claim? Or are there other transformations being done?

spinroot · 2011-12-21 07:49:20

You are correct : we use the stutter extension rule in the translations, so that finite runs can be interpreted as a special case of infinite runs

eugen · 2011-12-21 16:14:01

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

spinroot · 2011-12-21 16:17:23

yes it is

eugen · 2011-12-21 19:03:55

Why?

spinroot · 2011-12-21 19:05:26

because that's how it is designed...
do you have a specific reason to suspect that it would not work?

eugen · 2011-12-21 20:11:46

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.

spinroot · 2011-12-22 01:33:37

The algorithm built into Spin is the one from the GPVW'95 paper: http://spinroot.com/spin/Doc/ltl.pdf but there are lots of other converters by now, all with the same basic properties (e.g., they can be used for any LTL property, both expressing liveness and safety properties). Safety applies equally to finite and infinite executions (e.g., consider an invariant, which is a safety property), so there's no special treatment needed there.
In theory the size of the Buchi automaton (that's what is built in the conversion: a non-determinisitic BA, which is precisely what a never claim is) can increase exponentially with the number of temporal operators in the LTL formula. In practice this is a non-issue though. The number of temporal operators in useful formula is rarely more than 3 or 4, so the effect is very small.
You may have a different concern in mind though, but I'm not sure I understand what it is yet?

eugen · 2011-12-22 13:50:11

I try to explain my concern with some examples. Consider the model:

init {
  do
    :: (1) -> skip;
  od;
}

and the following three never-claims (N1, N2, N3):

never
{
accept_s:
  if
    :: (1) -> goto accept_s;
  fi;
}

never
{
accept_s:
  if
    :: (1) -> goto accept_s;
    :: (1) -> goto accept_all;
  fi;
accept_all:
  skip
}

never
{
accept_s1:
  if
    :: (1) -> goto accept_s2;
  fi;

accept_s2:
  if
    :: (1) -> goto accept_s1;
  fi;
}

As expected, with a simple DFS (ie. ./pan without the -a option), SPIN finds an error only for N2. With a nested DFS (./pan -a), it finds an error for all three never-claims. On infinite traces, the three never-claims are equivalent, and describe a safety property (the bad thing is the empty trace). Assume that there are 3 LTL formulas from which these never-claims are generated. (This assumption may or may not hold, I don't know.) To check them with a single DFS, the never-claims N1 and N3 would need to be further transformed into something similar to N2. To obtain N2 from N1 seems easy (for sink states, just add a goto to the end of the never-claim), but to obtain N2 from N3 seems harder.

So my question is how does SPIN make sure that never-claims like N3 are not generated from safety LTL properties?

spinroot · 2011-12-22 18:53:49

The LTL equivalent of the first claim (N1) is the invariant: [] true
for N2 it is: ([] true) || (<>[]true) which is of course equivalent to the simpler N1
for N3 it is: [] (true && X true) which again in this case is again equivalent to N1
Never claims (and non-deterministic buchi automata) can express a larger set of properties than LTL can, so it is not always possible to find an LTL formula that is equivalent to a given never claim. Technically, never claims can specify any omega-regular property, while LTL can only specify a subset of these.
The never claim is used to express undesirable behavior (things that should *never* happen) -- so the actual property you're checking with N1 through N3 would be their negation: ![] true which is the same as <> false. Clearly we can deduce that this property cannot hold, so any infinite execution at all can serve as a counter-example. Note also that although [] true is a safety property, <> false is a liveness property.
Not sure if any of this helps.
You question comes down to: are we sure that the conversion algorithm is correct. To keep it simple: check the correctness proofs in the papers on these algoritms and see if you can find a flaw.

eugen · 2011-12-22 19:45:50

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.

Last edited by eugen (2011-12-22 19:49:28)

spinroot · 2011-12-22 19:55:28

There's only a minor syntactic convenience in never claims that make reaching the end-state of the claim equivalent to reaching a dummy accepting state:
accept_all: do :: true od
This is not an extension of its expressive power though -- never claims have precisely the expressive power of Buchi automata, not more and not less.
The algorithm used in Spin is in the GPVW'95 paper, so that should be easy to look up.
I don't think there's a real issue here. Spin simply applies a short-cut/optimization for cases where it can easily tell that we're in a trivial self-accept state (a self-loop on true), as occurs at the closing brace of the never claim.

eugen · 2011-12-22 19:57:01

Said otherwise: say that I have an LTL to NBA translator that for the formula '[] true' generates the never claim N1. Then SPIN would not detect an error with a simple DFS, even though the translation is correct (the formula and the NBA/never-claim are equivalent). Hence the translation needs to have an additional property besides being correct in order to check safety LTL property with a simple DFS. And what I wonder is what is this property that makes SPIN work correctly (in case it indeed does).

spinroot · 2011-12-22 20:01:24

Any never claim that contains accept-state labels (other than the dummy accept_all label at the end) requires the -a flag (nested DFS) to fully verify.
That's the rule.
Now your question is: does the conversion algorithm always generate a never claim free of those accept labels for safety properties? I believe the answer is yes. We can almost take it as the definition of a safety property. If you disagree, show me a counter-example....

eugen · 2011-12-22 20:14:21

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.

spinroot · 2011-12-22 20:51:54

if I take this version: ! ( ([] p) || (p U q))
this can be rewritten as: (<>!p) && !(p U q)
the first half of this is a liveness property (there exists no infinite path where p remains true)
so, it's not a safety property

eugen · 2011-12-22 21:20:26

But ([] p) || (p U q) is a safety property (the bad thing is if !p holds and before that q does not hold) and this is the property that I'd like to check. A similar situation is for the invariant []p: we search for a counter-example of []p, hence for words satisfying <>!p, although incidentally this is a liveness property.

spinroot · 2011-12-22 21:28:10

I've lost track of the question. Is it ([] p) || (p U q) that you want to check or the negation, as in your earlier post?
If you want to verify F then you specify !F as a never claim to find the violations.
So if your interested in ([] p) || (p U q) then the never claim is for !([] p) || (p U q) and that never claim is not a safety property but a liveness property.

eugen · 2011-12-22 21:49:39

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

Spinroot

#1 2011-12-20 18:26:32

LTL and never-claims

#2 2011-12-21 07:49:20

Re: LTL and never-claims

#3 2011-12-21 16:14:01

Re: LTL and never-claims

#4 2011-12-21 16:17:23

Re: LTL and never-claims

#5 2011-12-21 19:03:55

Re: LTL and never-claims

#6 2011-12-21 19:05:26

Re: LTL and never-claims

#7 2011-12-21 20:11:46

Re: LTL and never-claims

#8 2011-12-22 01:33:37

Re: LTL and never-claims

#9 2011-12-22 13:50:11

Re: LTL and never-claims

#10 2011-12-22 18:53:49

Re: LTL and never-claims

#11 2011-12-22 19:45:50

Re: LTL and never-claims

#12 2011-12-22 19:55:28

Re: LTL and never-claims

#13 2011-12-22 19:57:01

Re: LTL and never-claims

#14 2011-12-22 20:01:24

Re: LTL and never-claims

#15 2011-12-22 20:14:21

Re: LTL and never-claims

#16 2011-12-22 20:51:54

Re: LTL and never-claims

#17 2011-12-22 21:20:26

Re: LTL and never-claims

#18 2011-12-22 21:28:10

Re: LTL and never-claims

#19 2011-12-22 21:49:39

Re: LTL and never-claims

Board footer