Labelled transition system

LTSstructure

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

Used by

Deterministic system
Reachability
Simulation
Trace

From Mathlib

Order.SetNotation

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

Adapted for Conjectura from cslib, `Cslib/Foundations/Semantics/Lts/Basic.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