Home » forums » LtU Forum

Stutter Invariance

Hi,

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,
Mohan...

By mohan_vbh at 2007-09-14 10:43 | LtU Forum | previous forum topic | next forum topic | other blogs | 7508 reads

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?

http://research.microsoft.com/users/lamport/pubs/pubs.html has a lot on stuttering invariance.

By stevechy at Fri, 2007-09-14 18:13 | login or register to post comments

wiki says

wiki says

By Hank Thediek at Sat, 2007-09-15 11:01 | login or register to post comments