Stuttering equivalence

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

:$pisim\_\{st\}pi\text{'}$,

can be seen as a partitioning of path $pi$ and $pi\text{'}$ into blocks, so that states in the $k^\{mathrm\{th$ block of one path are labeled ($L(sdot)$) 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\text{'}=r\_0,\; r\_1,\; ldots$ which are stuttering equivalent ($pi\; sim\_\{st\}\; pi\text{'}$) if there are two infinite sequences of integers and 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/branching time logic (modal logic). So-called branching bisimulation has to be used.