In theoretical computer science, stuttering equivalence, a relation written as
π ∼ s t π ′ {\displaystyle \pi \sim _{st}\pi '} , can be seen as a partitioning of paths π {\displaystyle \pi } and π ′ {\displaystyle \pi '} into blocks, so that states in the k t h {\displaystyle k^{\mathrm {th} }} block of one path are labeled ( L ( ⋅ ) {\displaystyle L(\cdot )} ) the same as states in the k t h {\displaystyle k^{\mathrm {th} }} block of the other path. Corresponding blocks may have different lengths. Formally, this can be expressed as two infinite paths π = s 0 , s 1 , … {\displaystyle \pi =s_{0},s_{1},\ldots } and π ′ = r 0 , r 1 , … {\displaystyle \pi '=r_{0},r_{1},\ldots } being stuttering equivalent ( π ∼ s t π ′ {\displaystyle \pi \sim _{st}\pi '} ) if there are two infinite sequences of integers 0 = i 0 < i 1 < i 2 < … {\displaystyle 0=i_{0}<i_{1}<i_{2}<\ldots } and 0 = j 0 < j 1 < j 2 < … {\displaystyle 0=j_{0}<j_{1}<j_{2}<\ldots } such that for every block k ≥ 0 {\displaystyle k\geq 0} holds L ( s i k ) = L ( s i k + 1 ) = … = L ( s i k + 1 − 1 ) = L ( r j k ) = L ( r j k + 1 ) = … = L ( r j k + 1 − 1 ) {\displaystyle 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.
References
