Stutter bisimulation

Summary

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

edit

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   is a binary relation R on S such that for all (s1,s2) in R:

  1.   have the same labels
  2. If   is a valid transition and   then there exists a finite path fragment   ( ) such that each pair   is in R and   is in R
  3. If   is a valid transition and   is not then there exists a finite path fragment   ( ) such that each pair   is in R and   is in R

Generalizations

edit

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]

References

edit
  1. ^ Principles of Model Checking (pages 536–580), by Christel Baier and Joost-Pieter Katoen, The MIT Press, Cambridge, Massachusetts.
  2. ^ Mohajerani, Sahar; Malik, Robi; Wintenberg, Andrew; Lafortune, Stéphane; Ozay, Necmiye (2021). "Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications". Automatica. 130. doi:10.1016/j.automatica.2021.109723. hdl:10289/14366.
  3. ^ Krook, Jonas; Malik, Robi; Mohajerani, Sahar; Fabian, Martin (2024). "Robust stutter bisimulation for abstraction and controller synthesis with disturbance". Automatica. 160. doi:10.1016/j.automatica.2023.111394.