Trace equivalence

Conjectura.Defs.ComputerScience.Semantics.TraceEquivalence

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

/-! # Trace equivalence

## Source

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

namespace Conjectura.Semantics

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

end Conjectura.Semantics