Stuttering equivalence

{{technical|date=July 2012}}

In theoretical computer science, stuttering equivalence,{{cite book | first1 = Jan Friso | last1 = Groote | first2 = Frits W. | last2 = Vaandrager | chapter-url = https://archive.org/details/automatalanguage0000ical/page/626 | chapter = An efficient algorithm for branching bisimulation and stuttering equivalence | title = Proceedings of the 17th International Colloquium on Automata, Languages and Programming | editor1-first = Michael S. | editor1-last = Paterson | publisher = Springer-Verlag | series = Lecture Notes in Computer Science | volume = 443 | pages = [https://archive.org/details/automatalanguage0000ical/page/626 626–638] | year = 1990 | isbn = 0-387-52826-1 | doi = 10.1007/BFb0032063 | url = https://ir.cwi.nl/pub/5766 | chapter-url-access = registration }} a relation written as

Image:Stuttering Equivalence.pdf

:$\backslash pi\backslash sim\_\{st\}\backslash pi\text{'}$,

can be seen as a partitioning of paths $\backslash pi$ and $\backslash pi\text{'}$ into blocks, so that states in the $k^\{\backslash mathrm\{th\}\}$ block of one path are labeled ($L(\backslash sdot)$) the same as states in the $k^\{\backslash mathrm\{th\}\}$ block of the other path. Corresponding blocks may have different lengths.

Formally, this can be expressed as two infinite paths $\backslash pi=s\_0,\; s\_1,\; \backslash ldots$ and $\backslash pi\text{'}=r\_0,\; r\_1,\; \backslash ldots$ being stuttering equivalent ($\backslash pi\; \backslash sim\_\{st\}\; \backslash pi\text{'}$) if there are two infinite sequences of integers and such that for every block $k\; \backslash geq\; 0$ holds $L(s\_\{i\_k\})\; =\; L(s\_\{i\_k+1\})\; =\; \backslash ldots\; =\; L(s\_\{i\_\{k+1\}-1\})\; =\; L(r\_\{j\_k\})\; =\; L(r\_\{j\_k+1\})\; =\; \backslash 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.{{Citation needed|date=April 2012}}