Spinroot

m_tabaei

Member

Registered: 2011-06-21

Posts: 2

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

Hi,

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.

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

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