Stuttering Equivalence

Stephan Merz 🌐

May 7, 2012

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

Two omega-sequences are stuttering equivalent if they differ only by finite repetitions of elements. Stuttering equivalence is a fundamental concept in the theory of concurrent and distributed systems. Notably, Lamport argues that refinement notions for such systems should be insensitive to finite stuttering. Peled and Wilke showed that all PLTL (propositional linear-time temporal logic) properties that are insensitive to stuttering equivalence can be expressed without the next-time operator. Stuttering equivalence is also important for certain verification techniques such as partial-order reduction for model checking.

We formalize stuttering equivalence in Isabelle/HOL. Our development relies on the notion of stuttering sampling functions that may skip blocks of identical sequence elements. We also encode PLTL and prove the theorem due to Peled and Wilke.

License

BSD License

History

January 31, 2013
Added encoding of PLTL and proved Peled and Wilke's theorem. Adjusted abstract accordingly.

Topics

Session Stuttering_Equivalence