Documentation

Cslib.Semantics.LTS.TraceEq

Trace Equivalence #

Definitions and results on trace equivalence for LTSs.

Main definitions #

Notations #

Main statements #

def 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
Instances For
    theorem 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 TraceEq {State : Type u} {Label : Type v} (lts : LTS State Label) (s1 s2 : State) :

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

    Equations
    Instances For

      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.
      Instances For
        theorem TraceEq.refl {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) :
        s ~tr[lts] s

        Trace equivalence is reflexive.

        theorem 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 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 TraceEq.eqv {State : Type u} {Label : Type v} (lts : LTS State Label) :

        Bisimilarity is an equivalence relation.

        theorem 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.