Stutter bisimulation

In theoretical computer science, a stutter bisimulation is a relationship between two transition systems, abstract machines that model computation. 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.

Definition

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. A stutter bisimulation for ${\text{TS}}=(S,{\text{Act}},\to ,I,{\text{AP}},L)$ is a binary relation R on S such that for all (s₁,s₂) in R:

1. $s_{1},s_{2}$ have the same labels
2. If $s_{1}\to s_{1}'$ is a valid transition and $(s_{1}',s_{2})\not \in R$ then there exists a finite path fragment $s_{2}u_{1}\cdots u_{n}s_{2}'$ ($n\geq 0$) such that each pair $(s_{1},u_{i})$ is in R and $(s_{1}',s_{2}')$ is in R
3. If $s_{2}\to s_{2}'$ is a valid transition and $(s_{1},s_{2}')\not \in R$ is not then there exists a finite path fragment $s_{1}v_{1}\cdots v_{n}s_{1}'$ ($n\geq 0$) such that each pair $(v_{i},s_{2})$ is in R and $(s_{1}',s_{2}')$ is in R

Generalizations

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. A robust stutter bisimulation allows uncertainty over transitions in the system.