It is defined coinductively and generalizes the idea of bisimulations.
A bisimulation matches up the states of a machine such that transitions correspond; a stutter bisimulation allows transitions to be matched to finite path fragments.
[1] In Principles of Model Checking, Baier and Katoen define a stutter bisimulation for a single transition system and later adapt it to a relation on two transition systems.
is a binary relation R on S such that for all (s1,s2) in R: A generalization, the divergent stutter bisimulation, can be used to simplify the state space of a system with the tradeoff that statements using the linear temporal logic operator "next" may change truth value.
[2] A robust stutter bisimulation allows uncertainty over transitions in the system.