Stutter bisimulation


Stutter bisimulation is defined in a coinductive manner, as bisimulation.

Let TS= be a transition system. A stutter bisimulation for TS is

a binary relation R on S such that for all which is in R:

  1. L = L.
  2. If s1' is in Post with is not in R,

then there exists a finite path fragment s2u1…uns2' with n≥0 and

is in R, and is in R.
  1. If s2' is in Post with is not in R,

then there exists a finite path fragment s1v1…vns1' with n≥0 and

is in R, and is in R.