Stuttering equivalence 1554504 161261576 2007-09-30T05:55:37Z David Eppstein 2051880 stub sorting In [[theoretical computer science]], '''stuttering equivalence''', a relation written as :<math>\pi\sim_{st}\pi'</math>, can be seen as a partitioning of path <math>\pi</math> and <math>\pi'</math> into blocks, so that states in the <math>k^{\mathrm{th}}</math> block of one path are labeled (<math>L(\sdot)</math>) the same as states in the <math>k^{\mathrm{th}}</math> block of the other path. Corresponding blocks may have different lengths. Formally, this can be expressed as two infinite paths <math>\pi=s_0, s_1, \ldots</math> and <math>\pi'=r_0, r_1, \ldots</math> which are stuttering equivalent (<math>\pi \sim_{st} \pi'</math>) if there are two infinite sequences of integers <math>0 = i_0 < i_1 < i_2 < \ldots</math> and <math>0 = j_0 < j_1 < j_2 < \ldots</math> such that for every block <math>k \geq 0</math> holds <math>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})</math>. Stuttering equivalence is '''not the same''' as [[bisimulation]], since bisimulation cannot capture the semantics of the 'eventually' (or 'finally') operator found in [[Linear temporal logic|linear temporal]]/[[branching time logic]] ([[modal logic]]). So-called '''branching bisimulation''' has to be used. [[Category:Theoretical computer science]] {{mathlogic-stub}}