Email Gateway (Aug 18 2022 at 20:06): Email Gateway (Aug 18 2022 at 20:06):From: Tobias Nipkow <nipkow@in.tum.de>
Stuttering Equivalence
Stephan Merz
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 show that all LTL (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 a stuttering sampling function that identifies blocks of identical
sequence elements.
http://afp.sourceforge.net/entries/Stuttering_Equivalence.shtml
[An eminently reusable contribution, thanks Stephan.]
Last updated: Apr 16 2024 at 16:19 UTC