Bisimulation
IsBisimulationdef
A relation is a bisimulation when it is a IsSimulation in both directions: the two systems mimic each other step for step, and the states they reach stay related.
def IsBisimulation {S₁ S₂ Label : Type*}
(lts₁ : LTS S₁ Label) (lts₂ : LTS S₂ Label) (r : S₁ → S₂ → Prop) : Prop :=
IsSimulation lts₁ lts₂ r ∧ IsSimulation lts₂ lts₁ (fun b a => r a b)Builds on
Used by
import Conjectura.Defs.ComputerScience.Semantics.Bisimulation · maintainer — open · raw source
Adapted for Conjectura from cslib, `Cslib/Foundations/Semantics/Lts/Bisimulation.lean`, split into one concept per module. Released by its authors under Apache 2.0.
Copyright (c) 2025 Fabrizio Montesi. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi