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

• LTS.BoundedUpTo records an explicit global execution-length bound. LTS.Bounded, LTS.Terminating, and LTS.Acyclic distinguish globally bounded execution length, absence of infinite executions, and absence of nonempty cycles.

• Definitions for all the common classes of LTSs: image-finite, finitely branching, finite-state, 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.

theorem Cslib.LTS.ext_iff {State : Type u} {Label : Type v} {x y : LTS State Label} : x = y ↔ x.Tr = y.Tr

theorem Cslib.LTS.ext {State : Type u} {Label : Type v} {x y : LTS State Label} (Tr : x.Tr = y.Tr) : x = y

def Cslib.LTS.UnlabelledTr {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : State → State → Prop

The unlabelled transition relation underlying an LTS.

Equations

• lts.UnlabelledTr s₁ s₂ = ∃ (μ : Label), lts.Tr s₁ μ s₂

def Cslib.LTS.IsTerminal {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (s : State) : Prop

A state is terminal if it has no outgoing transitions.

Equations

• lts.IsTerminal s = ∀ (μ : Label) (s' : State), ¬lts.Tr s μ s'

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_iff {State : Type u} {Label : Type v} (lts : LTS State Label) (a✝ : State) (a✝¹ : List Label) (a✝² : State) : lts.MTr a✝ a✝¹ a✝² ↔ a✝¹ = [] ∧ a✝² = a✝ ∨ ∃ (μ : Label) (s2 : State) (μs : List Label), lts.Tr a✝ μ s2 ∧ lts.MTr s2 μs a✝² ∧ a✝¹ = μ :: μs

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.

@[simp]

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

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.cons_iff {State : Type u} {Label : Type v} {s1 : State} {μ : Label} {μs : List Label} {s2 : State} {lts : LTS State Label} : lts.MTr s1 (μ :: μs) s2 ↔ ∃ (s : State), lts.Tr s1 μ s ∧ lts.MTr s μs s2

A multistep transition along μ :: μs is a transition labelled by μ plus a multistep transition labelled by μs.

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.

@[simp]

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

A 1-sized multistep transition is exactly a single transition with the given label.

theorem Cslib.LTS.MTr.split {State : Type u} {Label : Type v} {s1 : State} {μs μs' : List Label} {s2 : State} {lts : LTS State Label} (h : lts.MTr s1 (μs ++ μs') s2) : ∃ (s : State), lts.MTr s1 μs s ∧ lts.MTr s μs' s2

A multistep transition over a concatenation can be split into two multistep transitions.

theorem Cslib.LTS.MTr.append_iff {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μs μs' : List Label} {s2 : State} : lts.MTr s1 (μs ++ μs') s2 ↔ ∃ (s : State), lts.MTr s1 μs s ∧ lts.MTr s μs' s2

Multistep-transitions over μs ++ μs' are exactly multistep transitions over μs and μs' with a common end & start state (respectively).

def Cslib.LTS.TrInv {State : Type u} {Label : Type v} (lts : LTS State Label) (p : State → Prop) : Prop

Single-step invariant.

Equations

• lts.TrInv p = ∀ (s1 : State) (μ : Label) (s2 : State), lts.Tr s1 μ s2 → p s1 → p s2

def Cslib.LTS.MTrInv {State : Type u} {Label : Type v} (lts : LTS State Label) (p : State → Prop) : Prop

Multistep invariant.

Equations

• lts.MTrInv p = ∀ (s1 : State) (μs : List Label) (s2 : State), lts.MTr s1 μs s2 → p s1 → p s2

theorem Cslib.LTS.mtrInv_of_trInv {State : Type u} {Label : Type v} {lts : LTS State Label} {p : State → Prop} (htr : lts.TrInv p) : lts.MTrInv p

Any single-step invariant is also a multistep invariant.

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.

def Cslib.LTS.traces {State : Type u_1} {Label : Type u_2} {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

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

def Cslib.LTS.completeTraces {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} (s : State) : Set (List Label)

The complete 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 from s to a state with no outgoing transitions.

Equations

• Cslib.LTS.completeTraces s = {μs : List Label | ∃ (s' : State), lts.IsTerminal s' ∧ lts.MTr s μs s'}

theorem Cslib.LTS.mem_traces_iff {State : Type u_1} {Label : Type u_2} {s : State} {lts : LTS State Label} (μs : List Label) : μs ∈ traces s ↔ ∃ (s' : State), lts.MTr s μs s'

Definition of LTS.traces for general label sequences, ...

theorem Cslib.LTS.mem_traces_singleton_iff {State : Type u_1} {Label : Type u_2} {s : State} {lts : LTS State Label} (μ : Label) : [μ] ∈ traces s ↔ ∃ (s' : State), lts.Tr s μ s'

... singleton sequences, ...

theorem Cslib.LTS.mem_traces_cons_iff {State : Type u_1} {Label : Type u_2} {s : State} {lts : LTS State Label} (μ : Label) (μs : List Label) : μ :: μs ∈ traces s ↔ ∃ (s' : State), lts.Tr s μ s' ∧ μs ∈ traces s'

... and sequences extended with a single transition.

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

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

Classes of LTSs

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

A state s is deterministic for a label μ if s has at most one μ-derivative.

Equations

• lts.DeterministicStateLabel s μ = ∀ (s₁ s₂ : State), lts.Tr s μ s₁ → lts.Tr s μ s₂ → s₁ = s₂

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

A state s is deterministic if it is deterministic for all labels.

Equations

• lts.DeterministicState s = ∀ (μ : Label), lts.DeterministicStateLabel s μ

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

An lts is deterministic if it is deterministic at every state.

• deterministic (s : State) : lts.DeterministicState s

  For all states and labels, there is at most one state reachable from a given state with a given label.

theorem Cslib.LTS.Deterministic.eq_of_tr {State : Type u} {Label : Type v} {s1 : State} {μ : Label} {s2 s2' : State} {lts : LTS State Label} [h : lts.Deterministic] (htr : lts.Tr s1 μ s2) (htr' : lts.Tr s1 μ s2') : s2 = s2'

theorem Cslib.LTS.Deterministic.eq_of_mTr {State : Type u} {Label : Type v} {s1 : State} {μs : List Label} {s2 s2' : State} {lts : LTS State Label} [lts.Deterministic] (hmtr : lts.MTr s1 μs s2) (hmtr' : lts.MTr s1 μs s2') : s2 = s2'

In a deterministic lts, multistep transitions with a given start state and trace reach a unique end state.

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.DeterministicStateLabel.not_tr_of_ne {State : Type u} {Label : Type v} (lts : LTS State Label) {s : State} {μ : Label} {s₁ s₂ : State} (hdet : lts.DeterministicStateLabel s μ) (hne : s₁ ≠ s₂) (htr₁ : 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.DeterministicStateLabel.image_singleton_iff_tr {State : Type u} {Label : Type v} (lts : LTS State Label) {s : State} {μ : Label} {s' : State} (h : lts.DeterministicStateLabel s μ) : lts.image s μ = {s'} ↔ lts.Tr s μ s'

theorem Cslib.LTS.DeterministicStateLabel.image_char {State : Type u} {Label : Type v} (lts : LTS State Label) {s : State} {μ : Label} (h : lts.DeterministicStateLabel s μ) : (∃ (s' : State), lts.image s μ = {s'}) ∨ lts.image s μ = ∅

If s is deterministic for μ, then the μ-image of s is either a singleton or the empty set.

theorem Cslib.LTS.DeterministicStateLabel.finite_image {State : Type u} {Label : Type v} (lts : LTS State Label) {s : State} {μ : Label} (h : lts.DeterministicStateLabel s μ) : Finite ↑(lts.image s μ)

If s is deterministic at μ, then the μ-image of s is finite.

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

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.

def Cslib.LTS.BoundedUpTo {State : Type u} {Label : Type v} (lts : LTS State Label) (n : ℕ) : Prop

An LTS is bounded up to n if every finite execution has length strictly less than n.

Equations

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

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

An LTS is bounded if there is a global bound on the length of all of its finite executions.

• bounded : ∃ (n : ℕ), lts.BoundedUpTo n

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

An LTS is terminating if its underlying unlabelled transition relation is terminating, equivalently if it admits no infinite execution.

• terminating : Relation.Terminating lts.UnlabelledTr

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

An LTS is acyclic if its underlying unlabelled transition relation contains no nonempty cycle.

• acyclic : Relation.Acyclic lts.UnlabelledTr

theorem Cslib.LTS.Deterministic.traces_of_tr {State : Type u} {Label : Type v} {s : State} {μ : Label} {s' : State} {lts : LTS State Label} [lts.Deterministic] (h : lts.Tr s μ s') : traces s' = {μs : List Label | μ :: μs ∈ traces s}

In a deterministic lts, a state's traces are determined by any of its predecessors.

theorem Cslib.LTS.Deterministic.traces_of_mTr {State : Type u} {Label : Type v} {s : State} {μs : List Label} {s' : State} {lts : LTS State Label} [lts.Deterministic] (h : lts.MTr s μs s') : traces s' = {μs' : List Label | μs ++ μs' ∈ traces s}

In a deterministic lts, a state's traces are determined by any of its multi-step predecessors.