Stutter bisimulation

Stutter bisimulation[1] is defined in a coinductive manner, as 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 (s₁,s₂) which is in R:

1. L(s₁) = L(s₂).
2. If s₁^' is in Post(s1) with (s₁^',s₂) is not in R,
   

then there exists a finite path fragment s₂u₁…u_ns₂^' with n≥0 and
(s₁,u_i) is in R, and (s₁^',s₂^') is in R.

1. If s₂^' is in Post(s2) with (s₁,s₂^') is not in R,
   

then there exists a finite path fragment s₁v₁…v_ns₁^' with n≥0 and
(v_i,s₂)is in R, and (s₁^',s₂^') is in R.

References

1. Principles of Model Checking , by Christel Baier and Joost-Pieter Katoen, The MIT Press, Cambridge, Massachusetts.