Stuttering equivalence

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

The paths $\pi$ and $\pi '$ are stuttering equivalent.

$\pi \sim _{st}\pi '$,

can be seen as a partitioning of paths $\pi$ and $\pi '$ into blocks, so that states in the $k^{\mathrm {th} }$ block of one path are labeled ($L(\cdot )$) the same as states in the $k^{\mathrm {th} }$ 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 _{st}\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_{i_{k}})=L(s_{i_{k}+1})=\ldots =L(s_{i_{k+1}-1})=L(r_{j_{k}})=L(r_{j_{k}+1})=\ldots =L(r_{j_{k+1}-1})$.

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.