Stuttering equivalence

In theoretical computer science, stuttering equivalence, a relation written as In theoretical computer science, stuttering equivalence, a relation written as can be seen as a partitioning of path π {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 } which are 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 kgeq 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.