Lambda the Ultimate

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.

wiki says