---
title: "Stutter bisimulation"
chunk: 1/1
source: "https://en.wikipedia.org/wiki/Stutter_bisimulation"
category: "reference"
tags: "science, encyclopedia"
date_saved: "2026-05-05T11:39:24.407314+00:00"
instance: "kb-cron"
---

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 ==