Stutter bisimulation

Short description: Relationship between transition systems

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}^{\prime }$ is a valid transition and $({s_1}^{\prime },s_2)\in ̸R$ then there exists a finite path fragment $s_2{u}_1\cdots u_n{s_2}^{\prime }$ ($n\ge 0$) such that each pair $(s_1,u_i)$ is in R and $({s_1}^{\prime },{s_2}^{\prime })$ is in R
3. If $s_2\to {s_2}^{\prime }$ is a valid transition and $(s_1,{s_2}^{\prime })\in ̸R$ is not then there exists a finite path fragment $s_1{v}_1\cdots v_n{s_1}^{\prime }$ ($n\ge 0$) such that each pair $(v_i,s_2)$ is in R and $({s_1}^{\prime },{s_2}^{\prime })$ 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.