Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Bisimulation

Conjectura.Defs.ComputerScience.Semantics.Bisimulation

/-
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Fabrizio Montesi
-/
import Conjectura.Defs.ComputerScience.Semantics.Simulation

/-! # Bisimulation

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), `Cslib/Foundations/Semantics/Lts/Bisimulation.lean`, split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Semantics

/-- 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)

end Conjectura.Semantics