Trace Equivalence

Definitions and results on trace equivalence for LTSs.

Main definitions

• LTS.traces: the set of traces of a state.
• TraceEq s1 s2: s1 and s2 are trace equivalent, i.e., they have the same sets of traces.

Notations

• s1 ~tr[lts] s2: the states s1 and s2 are trace equivalent in lts.

Main statements

• TraceEq.eqv: trace equivalence is an equivalence relation (see Equivalence).
• TraceEq.deterministic_sim: in any deterministic LTS, trace equivalence is a simulation.

def Cslib.LTS.traces {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : Set (List Label)

The traces of a state s is the set of all lists of labels μs such that there is a multi-step transition labelled by μs originating from s.

Equations

• lts.traces s = {μs : List Label | ∃ (s' : State), lts.MTr s μs s'}

theorem Cslib.LTS.traces_in {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) (μs : List Label) (s' : State) (h : lts.MTr s μs s') : μs ∈ lts.traces s

If there is a multi-step transition from s labelled by μs, then μs is in the traces of s.

def Cslib.TraceEq {State : Type u} {Label : Type v} (lts : LTS State Label) (s1 s2 : State) : Prop

Two states are trace equivalent if they have the same set of traces.

Equations

• (s1 ~tr[lts] s2) = (lts.traces s1 = lts.traces s2)

def Cslib.«term_~tr[_]_» : Lean.TrailingParserDescr

Notation for trace equivalence.

Differently from standard pen-and-paper presentations, we require the lts to be mentioned explicitly.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.TraceEq.refl {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : s ~tr[lts] s

Trace equivalence is reflexive.

theorem Cslib.TraceEq.symm {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 s2 : State} (h : s1 ~tr[lts] s2) : s2 ~tr[lts] s1

Trace equivalence is symmetric.

theorem Cslib.TraceEq.trans {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 s2 s3 : State} (h1 : s1 ~tr[lts] s2) (h2 : s2 ~tr[lts] s3) : s1 ~tr[lts] s3

Trace equivalence is transitive.

theorem Cslib.TraceEq.eqv {State : Type u} {Label : Type v} (lts : LTS State Label) : Equivalence (TraceEq lts)

Trace equivalence is an equivalence relation.

instance Cslib.instTransTraceEq {State : Type u} {Label : Type v} (lts : LTS State Label) : Trans (TraceEq lts) (TraceEq lts) (TraceEq lts)

calc support for simulation equivalence.

Equations

• Cslib.instTransTraceEq lts = { trans := ⋯ }

theorem Cslib.TraceEq.deterministic_sim {State : Type u} {Label : Type v} (lts : LTS State Label) [hdet : lts.Deterministic] (s1 s2 : State) (h : s1 ~tr[lts] s2) (μ : Label) (s1' : State) : lts.Tr s1 μ s1' → ∃ (s2' : State), lts.Tr s2 μ s2' ∧ s1' ~tr[lts] s2'

In a deterministic LTS, trace equivalence is a simulation.