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 TS = ( S , Act , → , I , AP , L ) {\displaystyle {\text{TS}}=(S,{\text{Act}},\to ,I,{\text{AP}},L)} is a binary relation R on S such that for all (s1,s2) in R:
s 1 , s 2 {\displaystyle s_{1},s_{2}} have the same labels If s 1 → s 1 ′ {\displaystyle s_{1}\to s_{1}'} is a valid transition and ( s 1 ′ , s 2 ) ∉ R {\displaystyle (s_{1}',s_{2})\not \in R} then there exists a finite path fragment s 2 u 1 ⋯ u n s 2 ′ {\displaystyle s_{2}u_{1}\cdots u_{n}s_{2}'} ( n ≥ 0 {\displaystyle n\geq 0} ) such that each pair ( s 1 , u i ) {\displaystyle (s_{1},u_{i})} is in R and ( s 1 ′ , s 2 ′ ) {\displaystyle (s_{1}',s_{2}')} is in R If s 2 → s 2 ′ {\displaystyle s_{2}\to s_{2}'} is a valid transition and ( s 1 , s 2 ′ ) ∉ R {\displaystyle (s_{1},s_{2}')\not \in R} is not then there exists a finite path fragment s 1 v 1 ⋯ v n s 1 ′ {\displaystyle s_{1}v_{1}\cdots v_{n}s_{1}'} ( n ≥ 0 {\displaystyle n\geq 0} ) such that each pair ( v i , s 2 ) {\displaystyle (v_{i},s_{2})} is in R and ( s 1 ′ , s 2 ′ ) {\displaystyle (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.
References