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 →

Bisimilarity

Bisimilaritydef

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

Builds on

import Conjectura.Defs.ComputerScience.Semantics.Bisimilarity · 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

Full credits