A forum for Spin users

You are not logged in.

#1 2011-06-21 12:41:24

Registered: 2011-06-21
Posts: 2

Finite counterexamples for this desired LTL property ([] <> dl)


I tried to verify this LTL property ([]<>dl) on a model in SPIN. SPIN generated a never claim for the negation of this property which is ![]<>dl. I set parameters in SPIN to generate all the possible counterexamples up to the depth of 10,000. I expected to see only infinite counterexamples but to my surprise a large number of the generated counterexamples to this LTL property are finite. I can’t explain how these finite traces are generated.


#2 2011-06-22 15:04:52

Registered: 2010-11-18
Posts: 691

Re: Finite counterexamples for this desired LTL property ([] <> dl)

the finite traces are considered a special case of infinite traces, using the so-called 'stutter-extension rule' (this is fairly standard when dealing with omega-automata theory).  basically, the final state is assumed to repeat forever on a 'stutter' step (a no-op), thus allowing us to treat it as a special 'infinite' trace.
in your case ![]<>dl is the same as <>[]!dl, so if dl is false in the final state, the negated property holds on that trace


Board footer

Powered by FluxBB