Bisimilarity

Conjectura.Defs.ComputerScience.Semantics.Bisimilarity

/-
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.Bisimulation

/-! # Bisimilarity

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

/-- Two states are **bisimilar** when some `IsBisimulation` relates them. Bisimilarity is the
largest bisimulation, and the standard formal meaning of "these two processes behave the
same". -/
def Bisimilarity {S₁ S₂ Label : Type*}
    (lts₁ : LTS S₁ Label) (lts₂ : LTS S₂ Label) : S₁ → S₂ → Prop :=
  fun s₁ s₂ => ∃ r, r s₁ s₂ ∧ IsBisimulation lts₁ lts₂ r

end Conjectura.Semantics