Trace

HasTracedef

A trace of a state is a finite list of labels it can perform in order. Traces record what a system can do, but not when it committed to doing it.

def LTS.HasTrace {State Label : Type*}
    (lts : LTS State Label) : State → List Label → Prop
  | _, [] => True
  | s, μ :: μs => ∃ t, lts.Tr s μ t ∧ lts.HasTrace t μs

Builds on

Labelled transition system

Used by

Trace equivalence

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