Labelled Transition System (LTS)

A Labelled Transition System (LTS) models the observable behaviour of the possible states of a system. They are particularly popular in the fields of concurrency theory, logic, and programming languages.

Main definitions

• LTS is a structure for labelled transition systems, consisting of a labelled transition relation Tr between states. We follow the style and conventions in [Sangiorgi2011].

• LTS.MTr extends the transition relation of any LTS to a multistep transition relation, formalising the inference system and admissible rules for such relations in [Montesi2023].

• Definitions for all the common classes of LTSs: image-finite, finitely branching, finite-state, finite, and deterministic.

Main statements

• A series of results on LTS.MTr that allow for obtaining and composing multistep transitions in different ways.

• LTS.deterministic_imageFinite: every deterministic LTS is also image-finite.

• LTS.finiteState_imageFinite: every finite-state LTS is also image-finite.

• LTS.finiteState_finitelyBranching: every finite-state LTS is also finitely-branching, if the type of labels is finite.

References

• [F. Montesi, Introduction to Choreographies][Montesi2023]
• [D. Sangiorgi, Introduction to Bisimulation and Coinduction][Sangiorgi2011]

structure Cslib.LTS (State : Type u) (Label : Type v) : Type (max u v)

A Labelled Transition System (LTS) for a type of states (State) and a type of transition labels (Label) consists of a labelled transition relation (Tr).

• Tr : State → Label → State → Prop

  The transition relation.

Multistep transitions and executions with finite traces

This section treats executions with a finite number of steps.

inductive Cslib.LTS.MTr {State : Type u} {Label : Type v} (lts : LTS State Label) : State → List Label → State → Prop

Definition of a multistep transition.

(Implementation note: compared to [Montesi2023], we choose stepL instead of stepR as fundamental rule. This makes working with lists of labels more convenient, because we follow the same construction. It is also similar to what is done in the SimpleGraph library in mathlib.)

• refl {State : Type u} {Label : Type v} {lts : LTS State Label} {s : State} : lts.MTr s [] s
• stepL {State : Type u} {Label : Type v} {lts : LTS State Label} {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} : lts.Tr s1 μ s2 → lts.MTr s2 μs s3 → lts.MTr s1 (μ :: μs) s3

theorem Cslib.LTS.MTr.single {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μ : Label} {s2 : State} : lts.Tr s1 μ s2 → lts.MTr s1 [μ] s2

Any transition is also a multistep transition.

theorem Cslib.LTS.MTr.stepR {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μs : List Label} {s2 : State} {μ : Label} {s3 : State} : lts.MTr s1 μs s2 → lts.Tr s2 μ s3 → lts.MTr s1 (μs ++ [μ]) s3

Any multistep transition can be extended by adding a transition.

theorem Cslib.LTS.MTr.comp {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μs1 : List Label} {s2 : State} {μs2 : List Label} {s3 : State} : lts.MTr s1 μs1 s2 → lts.MTr s2 μs2 s3 → lts.MTr s1 (μs1 ++ μs2) s3

Multistep transitions can be composed.

theorem Cslib.LTS.MTr.single_invert {State : Type u} {Label : Type v} (lts : LTS State Label) (s1 : State) (μ : Label) (s2 : State) : lts.MTr s1 [μ] s2 → lts.Tr s1 μ s2

Any 1-sized multistep transition implies a transition with the same states and label.

theorem Cslib.LTS.MTr.nil_eq {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 s2 : State} (h : lts.MTr s1 [] s2) : s1 = s2

In any zero-steps multistep transition, the origin and the derivative are the same.

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

A state s1 can reach a state s2 if there exists a multistep transition from s1 to s2.

Equations

• lts.CanReach s1 s2 = ∃ (μs : List Label), lts.MTr s1 μs s2

theorem Cslib.LTS.CanReach.refl {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : lts.CanReach s s

Any state can reach itself.

def Cslib.LTS.generatedBy {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : LTS { s' : State // lts.CanReach s s' } Label

The LTS generated by a state s is the LTS given by all the states reachable from s.

Equations

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

Classes of LTSs

class Cslib.LTS.Deterministic {State : Type u} {Label : Type v} (lts : LTS State Label) : Prop

An lts is deterministic if a state cannot reach different states with the same transition label.

• deterministic (s1 : State) (μ : Label) (s2 s3 : State) : lts.Tr s1 μ s2 → lts.Tr s1 μ s3 → s2 = s3

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

The μ-image of a state s is the set of all μ-derivatives of s.

Equations

• lts.image s μ = {s' : State | lts.Tr s μ s'}

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

The μs-image of a state s, where μs is a list of labels, is the set of all μs-derivatives of s.

Equations

• lts.imageMultistep s μs = {s' : State | lts.MTr s μs s'}

def Cslib.LTS.setImage {State : Type u} {Label : Type v} (lts : LTS State Label) (S : Set State) (μ : Label) : Set State

The μ-image of a set of states S is the union of all μ-images of the states in S.

Equations

• lts.setImage S μ = ⋃ s ∈ S, lts.image s μ

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

The μs-image of a set of states S, where μs is a list of labels, is the union of all μs-images of the states in S.

Equations

• lts.setImageMultistep S μs = ⋃ s ∈ S, lts.imageMultistep s μs

theorem Cslib.LTS.mem_setImage {State : Type u} {Label : Type v} {S : Set State} {μ : Label} {s' : State} {lts : LTS State Label} : s' ∈ lts.setImage S μ ↔ ∃ s ∈ S, lts.Tr s μ s'

Characterisation of setImage wrt Tr.

theorem Cslib.LTS.tr_setImage {State : Type u} {Label : Type v} {S : Set State} {s : State} {μ : Label} {s' : State} {lts : LTS State Label} (hs : s ∈ S) (htr : lts.Tr s μ s') : s' ∈ lts.setImage S μ

theorem Cslib.LTS.mem_setImageMultistep {State : Type u} {Label : Type v} {S : Set State} {μs : List Label} {s' : State} {lts : LTS State Label} : s' ∈ lts.setImageMultistep S μs ↔ ∃ s ∈ S, lts.MTr s μs s'

Characterisation of setImageMultistep with MTr.

theorem Cslib.LTS.mTr_setImage {State : Type u} {Label : Type v} {S : Set State} {s : State} {μs : List Label} {s' : State} {lts : LTS State Label} (hs : s ∈ S) (htr : lts.MTr s μs s') : s' ∈ lts.setImageMultistep S μs

theorem Cslib.LTS.setImage_empty {State : Type u} {Label : Type v} {μ : Label} (lts : LTS State Label) : lts.setImage ∅ μ = ∅

The image of the empty set is always the empty set.

theorem Cslib.LTS.setImageMultistep_setImage_head {State : Type u} {Label : Type v} {S : Set State} {μ : Label} {μs : List Label} (lts : LTS State Label) : lts.setImageMultistep S (μ :: μs) = lts.setImageMultistep (lts.setImage S μ) μs

theorem Cslib.LTS.setImageMultistep_foldl_setImage {State : Type u} {Label : Type v} (lts : LTS State Label) : lts.setImageMultistep = List.foldl lts.setImage

Characterisation of setImageMultistep as List.foldl on setImage.

theorem Cslib.LTS.mem_foldl_setImage {State : Type u} {Label : Type v} {S : Set State} {μs : List Label} {s' : State} (lts : LTS State Label) : s' ∈ List.foldl lts.setImage S μs ↔ ∃ s ∈ S, lts.MTr s μs s'

Characterisation of membership in List.foldl lts.setImage with MTr.

@[reducible, inline]

abbrev Cslib.LTS.ImageFinite {State : Type u} {Label : Type v} (lts : LTS State Label) : Prop

An lts is image-finite if all images of its states are finite.

Equations

• lts.ImageFinite = ∀ (s : State) (μ : Label), Finite ↑(lts.image s μ)

theorem Cslib.LTS.deterministic_not_lto {State : Type u} {Label : Type v} (lts : LTS State Label) [h : lts.Deterministic] (s : State) (μ : Label) (s' s'' : State) : s' ≠ s'' → lts.Tr s μ s' → ¬lts.Tr s μ s''

In a deterministic LTS, if a state has a μ-derivative, then it can have no other μ-derivative.

theorem Cslib.LTS.deterministic_tr_image_singleton {State : Type u} {Label : Type v} (lts : LTS State Label) {s : State} {μ : Label} {s' : State} [lts.Deterministic] : lts.image s μ = {s'} ↔ lts.Tr s μ s'

theorem Cslib.LTS.deterministic_image_char {State : Type u} {Label : Type v} (lts : LTS State Label) [lts.Deterministic] (s : State) (μ : Label) : (∃ (s' : State), lts.image s μ = {s'}) ∨ lts.image s μ = ∅

In a deterministic LTS, any image is either a singleton or the empty set.

instance Cslib.LTS.instFiniteElemImageOfDeterministic {State : Type u} {Label : Type v} (lts : LTS State Label) [lts.Deterministic] (s : State) (μ : Label) : Finite ↑(lts.image s μ)

In a deterministic LTS, the image of any state-label combination is finite.

instance Cslib.LTS.deterministic_imageFinite {State : Type u} {Label : Type v} (lts : LTS State Label) [lts.Deterministic] : lts.ImageFinite

Every deterministic LTS is also image-finite.

instance Cslib.LTS.finiteState_imageFinite {State : Type u} {Label : Type v} (lts : LTS State Label) [Finite State] : lts.ImageFinite

Every finite-state LTS is also image-finite.

def Cslib.LTS.HasOutLabel {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) (μ : Label) : Prop

A state has an outgoing label μ if it has a μ-derivative.

Equations

• lts.HasOutLabel s μ = ∃ (s' : State), lts.Tr s μ s'

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

The set of outgoing labels of a state.

Equations

• lts.outgoingLabels s = {μ : Label | lts.HasOutLabel s μ}

class Cslib.LTS.FinitelyBranching {State : Type u} {Label : Type v} (lts : LTS State Label) : Prop

An LTS is finitely branching if it is image-finite and all states have finite sets of outgoing labels.

• image_finite : lts.ImageFinite
• finite_state (s : State) : Finite ↑(lts.outgoingLabels s)

instance Cslib.LTS.FinitelyBranching.of_finite {State : Type u} {Label : Type v} (lts : LTS State Label) [Finite State] [Finite Label] : lts.FinitelyBranching

Every LTS with finite types for states and labels is also finitely branching.

class Cslib.LTS.Acyclic {State : Type u} {Label : Type v} (lts : LTS State Label) : Prop

An LTS is acyclic if there are no infinite multistep transitions.

• acyclic : ∃ (n : ℕ), ∀ (s1 : State) (μs : List Label) (s2 : State), lts.MTr s1 μs s2 → μs.length < n

class Cslib.LTS.FiniteLTS {State : Type u} {Label : Type v} [Finite State] (lts : LTS State Label) extends lts.Acyclic : Prop

An LTS is finite if it is finite-state and acyclic.

We call this FiniteLTS instead of just Finite to avoid confusion with the standard Finite class.

• acyclic : ∃ (n : ℕ), ∀ (s1 : State) (μs : List Label) (s2 : State), lts.MTr s1 μs s2 → μs.length < n