Labelled transition system

Conjectura.Defs.ComputerScience.Semantics.LabelledTransitionSystem

/-
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Fabrizio Montesi
-/
import Mathlib.Order.SetNotation

/-! # Labelled transition system

## Source

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

namespace Conjectura.Semantics

universe u v

/-- A **labelled transition system** models the observable behaviour of a system: a relation
`Tr s μ s'` saying that state `s` can perform action `μ` and become `s'`. Nearly every notion
of process equivalence is phrased over this one structure. -/
structure LTS (State : Type u) (Label : Type v) where
  /-- The labelled transition relation. -/
  Tr : State → Label → State → Prop

end Conjectura.Semantics