Trace equivalence

TraceEquivalentdef

Two states are trace equivalent when they admit exactly the same traces. Strictly weaker than Bisimilarity; the gap between them is the classical illustration of why branching structure matters.

def TraceEquivalent {S₁ S₂ Label : Type*}
    (lts₁ : LTS S₁ Label) (lts₂ : LTS S₂ Label) (s₁ : S₁) (s₂ : S₂) : Prop :=
  ∀ μs : List Label, lts₁.HasTrace s₁ μs ↔ lts₂.HasTrace s₂ μs

Builds on

Trace

import Conjectura.Defs.ComputerScience.Semantics.TraceEquivalence · maintainer — open · raw source

Adapted for Conjectura from cslib, 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