Category of Labelled Transition Systems

This file contains the definition of the category of labelled transition systems as defined in Winskel and Nielsen's handbook chapter [WN95].

References

• N. Winskel and M. Nielsen, Models for concurrency

def Cslib.LTS.withIdle {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : LTS State (Option Label)

We first define what is denoted Tran* in [WN95]: the extension of a transition relation with idle transitions.

Equations

• lts.withIdle = { Tr := fun (s : State) (l : Option Label) (s' : State) => l.elim (s = s') fun (x : Label) => lts.Tr s x s' }

LTSs and LTS morphisms form a category

structure Cslib.LTSCat : Type ((max u v) + 1)

The definition of labelled transition system (with the type of states and the type of labels as part of the structure).

• State : Type u

  Type of states of an LTS

• Label : Type v

  Type of labels of an LTS

• lts : LTS self.State self.Label

  Transition relation of an LTS

structure Cslib.LTS.Morphism (lts₁ lts₂ : LTSCat) : Type

A morphism between two labelled transition systems consists of (1) a function on states, (2) a partial function on labels, and a proof that (1) preserves each transition along (2).

• stateMap : lts₁.State → lts₂.State

  Mapping of states of lts₁ to states of lts₂

• labelMap : lts₁.Label → Option lts₂.Label

  Mapping of labels of lts₁ to labels of lts₂

• labelMap_tr (s s' : lts₁.State) (l : lts₁.Label) : lts₁.lts.Tr s l s' → lts₂.lts.withIdle.Tr (self.stateMap s) (self.labelMap l) (self.stateMap s')

  Stipulation that stateMap preserve transitions

def Cslib.LTS.Morphism.id (lts : LTSCat) : Morphism lts lts

The identity LTS morphism.

Equations

• Cslib.LTS.Morphism.id lts = { stateMap := id, labelMap := pure, labelMap_tr := ⋯ }

def Cslib.LTS.Morphism.comp {lts₁ lts₂ lts₃ : LTSCat} (f : Morphism lts₁ lts₂) (g : Morphism lts₂ lts₃) : Morphism lts₁ lts₃

Composition of LTS morphisms.

We use Kleisli composition to define this.

Equations

• f.comp g = { stateMap := g.stateMap ∘ f.stateMap, labelMap := f.labelMap >=> g.labelMap, labelMap_tr := ⋯ }

@[implicit_reducible]

instance Cslib.instCategoryLTSCat : CategoryTheory.Category.{0, 1} LTSCat

Finally, we prove that these form a category.

Equations

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