### 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

- Computer science/Automata and formal languages

### Session Stuttering_Equivalence

- Samplers
- StutterEquivalence
- PLTL

### Depends on

- Linear Temporal Logic

### Used by

- Partial Order Reduction
- Consensus Refined
- A Fully Verified Executable LTL Model Checker
- Converting Linear-Time Temporal Logic to Generalized Büchi Automata
- Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model

## Cite

×

Stuttering_Equivalence-AFP

    @article{Stuttering_Equivalence-AFP,
      author  = {Stephan Merz},
      title   = {Stuttering Equivalence},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Stuttering_Equivalence.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- Feb 2, 2013 : Isabelle2012
- May 24, 2012 : Isabelle2012
- May 8, 2012 : Isabelle2011-1