Stutter bisimulation explained

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.^[1]

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 , \to, I, AP , L) is a binary relation R on S such that for all (s₁,s₂) in R:s _{1,} s _{2} have the same labels

1. 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 _{2u} _{1 …} u _{n} s _{2'} (n\ge 0 ) such that each pair (s _{1,} u _{i)} is in R and (s _{1',s} _{2')} is in R

1. 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 _{1v} _{1 …} v _{n} s _{1'} (n\ge 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.^[2] A robust stutter bisimulation allows uncertainty over transitions in the system.^[3]

Notes and References

1. Principles of Model Checking (pages 536–580), by Christel Baier and Joost-Pieter Katoen, The MIT Press, Cambridge, Massachusetts.
2. Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications. Automatica. 130. 2021. 10.1016/j.automatica.2021.109723. 10289/14366. free.
3. Robust stutter bisimulation for abstraction and controller synthesis with disturbance. Automatica. 160. 2024. 10.1016/j.automatica.2023.111394. free.