Stuttering equivalence explained

In theoretical computer science, stuttering equivalence,^[1] a relation written as

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

can be seen as a partitioning of paths

\pi and \pi' into blocks, so that states in the k ^{th} block of one path are labeled (L(\sdot) ) the same as states in the k ^{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.

Notes and References

1. Book: Jan Friso . Groote . Frits W. . Vaandrager . https://archive.org/details/automatalanguage0000ical/page/626 . An efficient algorithm for branching bisimulation and stuttering equivalence . Proceedings of the 17th International Colloquium on Automata, Languages and Programming . Michael S. . Paterson . . . 443 . 626–638 . 1990 . 0-387-52826-1 . 10.1007/BFb0032063 . registration .