Stutter bisimulation
In theoretical computer science, a stutter bisimulation is defined in a coinductive manner, as is bisimulation. Let TS=(S,Act,→,I,AP,L) be a transition system. A stutter bisimulation for TS is 
a binary relation R on S such that for all (s1,s2) which is in R:
 L(s1) = L(s2). If s1' is in Post(s1) with (s1',s2) is not in R,
then there exists a finite path fragment s2u1…uns2' with n≥0 and 
(s1,ui) is in R, and (s1',s2') is in R.
 If s2' is in Post(s2) with (s1,s2') is not in R,
then there exists a finite path fragment s1v1…vns1' with n≥0 and 
(vi,s2) is in R, and (s1',s2') is in R.

References

Transition systems