Stutter Invariance


I'm trying to understand the stutter invariance and its application in the verification distributed systems (specified in the the SPIN model checker, primer and reference manual).

I couldn't quite understand the concept. Could anyone help me to understand it ?

Thanks in advance,

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Also confused

I'm not sure if this is on topic, but I'll put in a bit anyway.

I don't quite understand it either, but basically, the idea is that if you want to show that two automata are doing essentially the same thing, or to compose them together, you have to add "stutter" or silent steps to accomodate for the differences between them or to allow them to interleave steps.

A property is stuttering invariant if it still holds after you add stuttering steps, which seems to really just be a check that your property didn't assume too much.

Applied to model checking, I guess testing properties that are not stuttering invariant might cause problems? has a lot on stuttering invariance.

wiki says