Stuttering Equivalence

In theoretical computer science, stuttering equivalence, a relation written as

:$\pi\sim_\pi'$,

can be seen as a partitioning of paths $\pi$ and $\pi'$ into blocks, so that states in the $k^$ block of one path are labeled ($L(\sdot)$) the same as states in the $k^$ block of the other path. Corresponding blocks may have different lengths.

Formally, this can be expressed as two infinite paths $\pi=s_0, s_1, \ldots$ and $\pi'=r_0, r_1, \ldots$ being stuttering equivalent ($\pi \sim_ \pi'$) if there are two infinite sequences of integers $0 = i_0 < i_1 < i_2 < \ldots$ and $0 = j_0 < j_1 < j_2 < \ldots$ such that for every block $k \geq 0$ holds $L(s_) = L(s_) = \ldots = L(s_) = L(r_) = L(r_) = \ldots = L(r_)$.

Stuttering equivalence is not the same as bisimulation, since bisimulation cannot capture the semantics of the 'eventually' (or 'finally') operator found in linear temporal/ computation tree logic (branching time logic)(modal logic). So-called ''branching bisimulation'' has to be used.

References

Formal methods
Logic in computer science
{{Comp-sci-theory-stub