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

• Lts.MTr extends the transition relation of any Lts to a multi-step transition relation, formalising the inference system and admissible rules for such relations in [Mon23].

• 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 multi-step 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
• D. Sangiorgi, Introduction to Bisimulation and Coinduction

structure Lts (State : Type u) (Label : Type v) : Type (max u v)

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

• Tr : State → Label → State → Prop

  The transition relation.

Multi-step transitions

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

Definition of a multi-step transition.

(Implementation note: compared to [Mon23], 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 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 multi-step transition.

theorem 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 multi-step transition can be extended by adding a transition.

theorem 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

Multi-step transitions can be composed.

theorem 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 multi-step transition implies a transition with the same states and label.

theorem 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 multi-step transition, the origin and the derivative are the same.

def 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 multi-step transition from s1 to s2.

Equations

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

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

Definitions about termination

def Lts.MayTerminate {State : Type u_1} {Label : Type u_2} (lts : Lts State Label) {Terminated : State → Prop} (s : State) : Prop

A state 'may terminate' if it can reach a terminated state. The definition of Terminated is a parameter.

Equations

• lts.MayTerminate s = ∃ (s' : State), Terminated s' ∧ lts.CanReach s s'

def Lts.Stuck {State : Type u_1} {Label : Type u_2} (lts : Lts State Label) {Terminated : State → Prop} (s : State) : Prop

A state 'is stuck' if it is not terminated and cannot go forward. The definition of Terminated is a parameter.

Equations

• lts.Stuck s = (¬Terminated s ∧ ¬∃ (μ : Label) (s' : State), lts.Tr s μ s')

Definitions for the unions of Ltss

Note: there is a nontrivial balance between ergonomics and generality here. These definitions might change in the future.

def Lts.unionSubtype {State : Type u} {Label : Type v} {S1 : State → Prop} {L1 : Label → Prop} {S2 : State → Prop} {L2 : Label → Prop} [DecidablePred S1] [DecidablePred L1] [DecidablePred S2] [DecidablePred L2] (lts1 : Lts (Subtype S1) (Subtype L1)) (lts2 : Lts (Subtype S2) (Subtype L2)) : Lts State Label

The union of two Ltss that have common supertypes for states and labels.

Equations

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

def Sum.isLeftP {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : Prop

TODO: move this to Sum?

Equations

• x.isLeftP = (x.isLeft = true)

def Sum.isRightP {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : Prop

TODO: move this to Sum?

Equations

• x.isRightP = (x.isRight = true)

def Lts.inl {State : Type u} {Label : Type v} {State' : Type u_1} (lts : Lts State Label) : Lts (Subtype Sum.isLeftP) (Subtype (Function.const Label True))

Lifting of an Lts State Label to Lts (State ⊕ State') Label.

Equations

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

def Lts.inr {State : Type u} {Label : Type v} {State' : Type u_1} (lts : Lts State Label) : Lts (Subtype Sum.isRightP) (Subtype (Function.const Label True))

Lifting of an Lts State Label to Lts (State' ⊕ State) Label.

Equations

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

def Lts.unionSum {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} (lts1 : Lts State1 Label) (lts2 : Lts State2 Label) : Lts (State1 ⊕ State2) Label

Union of two Ltss with the same Label type. The result combines the original respective state types State1 and State2 into (State1 ⊕ State2).

Equations

• lts1.unionSum lts2 = lts1.inl.unionSubtype lts2.inr

Classes of Ltss

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

Equations

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

def 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 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 Lts.deterministic_not_lto {State : Type u} {Label : Type v} (lts : Lts State Label) (hDet : 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 Lts.deterministic_image_char {State : Type u} {Label : Type v} (lts : Lts State Label) (hDet : 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.

theorem Lts.deterministic_imageFinite {State : Type u} {Label : Type v} (lts : Lts State Label) : lts.Deterministic → lts.ImageFinite

Every deterministic Lts is also image-finite.

def 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 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 μ}

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

Equations

• lts.FinitelyBranching = (lts.ImageFinite ∧ ∀ (s : State), Finite ↑(lts.OutgoingLabels s))

def Lts.FiniteState {State : Type u} {Label : Type v} : Lts State Label → Prop

An Lts is finite-state if it has a finite State type.

Equations

• x✝.FiniteState = Finite State

theorem Lts.finiteState_imageFinite {State : Type u} {Label : Type v} (lts : Lts State Label) (hFinite : lts.FiniteState) : lts.ImageFinite

Every finite-state Lts is also image-finite.

theorem Lts.finiteState_finitelyBranching {State : Type u} {Label : Type v} (lts : Lts State Label) (hFiniteLabel : _root_.Finite Label) (hFiniteState : lts.FiniteState) : lts.FinitelyBranching

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

def Lts.Acyclic {State : Type u} {Label : Type v} (lts : Lts State Label) : Prop

An Lts is acyclic if there are no infinite multi-step transitions.

Equations

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

def Lts.Finite {State : Type u} {Label : Type v} (lts : Lts State Label) : Prop

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

Equations

• lts.Finite = (lts.FiniteState ∧ lts.Acyclic)

Weak transitions (single- and multi-step)

class HasTau (Label : Type v) : Type v

A type of transition labels that includes a special 'internal' transition τ.

• τ : Label

inductive Lts.STr {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : Lts State Label) : State → Label → State → Prop

Saturated transition relation.

• refl {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : Lts State Label} {s : State} : lts.STr s HasTau.τ s
• tr {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : Lts State Label} {s1 s2 : State} {μ : Label} {s3 s4 : State} : lts.STr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.STr s3 HasTau.τ s4 → lts.STr s1 μ s4

def Lts.saturate {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : Lts State Label) : Lts State Label

The Lts obtained by saturating the transition relation in lts.

Equations

• lts.saturate = { Tr := lts.STr }

theorem Lts.STr.single {Label : Type u_1} {State : Type u_2} {s : State} {μ : Label} {s' : State} [HasTau Label] (lts : Lts State Label) : lts.Tr s μ s' → lts.STr s μ s'

Any transition is also a saturated transition.

inductive Lts.strN {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : Lts State Label) : ℕ → State → Label → State → Prop

As Lts.str, but counts the number of τ-transitions. This is convenient as induction metric.

• refl {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : Lts State Label} {s : State} : lts.strN 0 s HasTau.τ s
• tr {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : Lts State Label} {n : ℕ} {s1 s2 : State} {μ : Label} {s3 : State} {m : ℕ} {s4 : State} : lts.strN n s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.strN m s3 HasTau.τ s4 → lts.strN (n + m + 1) s1 μ s4

theorem Lts.str_strN {Label : Type u_1} {State : Type u_2} {s1 : State} {μ : Label} {s2 : State} [HasTau Label] (lts : Lts State Label) : lts.STr s1 μ s2 ↔ ∃ (n : ℕ), lts.strN n s1 μ s2

Lts.str and Lts.strN are equivalent.

@[irreducible]

theorem Lts.strN.trans_τ {Label : Type u_1} {State : Type u_2} {n : ℕ} {s1 s2 : State} {m : ℕ} {s3 : State} [HasTau Label] (lts : Lts State Label) (h1 : lts.strN n s1 HasTau.τ s2) (h2 : lts.strN m s2 HasTau.τ s3) : lts.strN (n + m) s1 HasTau.τ s3

Saturated transitions labelled by τ can be composed (weighted version).

theorem Lts.STr.trans_τ {Label : Type u_1} {State : Type u_2} {s1 s2 s3 : State} [HasTau Label] (lts : Lts State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) : lts.STr s1 HasTau.τ s3

Saturated transitions labelled by τ can be composed.

theorem Lts.strN.append {Label : Type u_1} {State : Type u_2} {n1 : ℕ} {s1 : State} {μ : Label} {s2 : State} {n2 : ℕ} {s3 : State} [HasTau Label] (lts : Lts State Label) (h1 : lts.strN n1 s1 μ s2) (h2 : lts.strN n2 s2 HasTau.τ s3) : lts.strN (n1 + n2) s1 μ s3

Saturated transitions can be appended with τ-transitions (weighted version).

theorem Lts.strN.comp {Label : Type u_1} {State : Type u_2} {n1 : ℕ} {s1 s2 : State} {n2 : ℕ} {μ : Label} {s3 : State} {n3 : ℕ} {s4 : State} [HasTau Label] (lts : Lts State Label) (h1 : lts.strN n1 s1 HasTau.τ s2) (h2 : lts.strN n2 s2 μ s3) (h3 : lts.strN n3 s3 HasTau.τ s4) : lts.strN (n1 + n2 + n3) s1 μ s4

Saturated transitions can be composed (weighted version).

theorem Lts.STr.comp {Label : Type u_1} {State : Type u_2} {s1 s2 : State} {μ : Label} {s3 s4 : State} [HasTau Label] (lts : Lts State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 μ s3) (h3 : lts.STr s3 HasTau.τ s4) : lts.STr s1 μ s4

Saturated transitions can be composed.

Divergence

def Lts.DivergentExecution {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : Lts State Label) (stream : Stream' State) : Prop

A divergent execution is a stream of states where each state is the anti-τ-derivative of the next.

Equations

• lts.DivergentExecution stream = ∀ (n : ℕ), lts.Tr (stream n) HasTau.τ (stream n.succ)

def Lts.Divergent {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : Lts State Label) (s : State) : Prop

A state is divergent if there is a divergent execution from it.

Equations

• lts.Divergent s = ∃ (stream : Stream' State), stream 0 = s ∧ lts.DivergentExecution stream

theorem Lts.divergent_drop {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : Lts State Label) (stream : Stream' State) (h : lts.DivergentExecution stream) (n : ℕ) : lts.DivergentExecution (Stream'.drop n stream)

If a stream is a divergent execution, then any 'suffix' is also a divergent execution.

def Lts.DivergenceFree {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : Lts State Label) : Prop

An Lts is divergence-free if it has no divergent state.

Equations

• lts.DivergenceFree = ¬∃ (s : State), lts.Divergent s

def Lts.Tr.toRelation {State : Type u_1} {Label : Type u_2} (lts : Lts State Label) (μ : Label) : State → State → Prop

Returns the relation that relates all states s1 and s2 via a fixed transition label μ.

Equations

• Lts.Tr.toRelation lts μ s1 s2 = lts.Tr s1 μ s2

def Lts.MTr.toRelation {State : Type u_1} {Label : Type u_2} (lts : Lts State Label) (μs : List Label) : State → State → Prop

Returns the relation that relates all states s1 and s2 via a fixed list of transition labels μs.

Equations

• Lts.MTr.toRelation lts μs s1 s2 = lts.MTr s1 μs s2

def Relation.toLts {Label : Type u_1} {State : Type u_2} [DecidableEq Label] (r : State → State → Prop) (μ : Label) : Lts State Label

Any homogeneous relation can be seen as an Lts where all transitions have the same label.

Equations

• Relation.toLts r μ = { Tr := fun (s1 : State) (μ' : Label) (s2 : State) => if μ' = μ then r s1 s2 else False }

Support for the calc tactic

instance instTransToRelationToRelationConsNil {State : Type u_1} {Label : Type u_2} {μ1 μ2 : Label} (lts : Lts State Label) : Trans (Lts.Tr.toRelation lts μ1) (Lts.Tr.toRelation lts μ2) (Lts.MTr.toRelation lts [μ1, μ2])

Transitions can be chained.

Equations

• instTransToRelationToRelationConsNil lts = { trans := ⋯ }

instance instTransToRelationToRelationCons {State : Type u_1} {Label : Type u_2} {μ : Label} {μs : List Label} (lts : Lts State Label) : Trans (Lts.Tr.toRelation lts μ) (Lts.MTr.toRelation lts μs) (Lts.MTr.toRelation lts (μ :: μs))

Transitions can be chained with multi-step transitions.

Equations

• instTransToRelationToRelationCons lts = { trans := ⋯ }

instance instTransToRelationToRelationHAppendListConsNil {State : Type u_1} {Label : Type u_2} {μs : List Label} {μ : Label} (lts : Lts State Label) : Trans (Lts.MTr.toRelation lts μs) (Lts.Tr.toRelation lts μ) (Lts.MTr.toRelation lts (μs ++ [μ]))

Multi-step transitions can be chained with transitions.

Equations

• instTransToRelationToRelationHAppendListConsNil lts = { trans := ⋯ }

instance instTransToRelationHAppendList {State : Type u_1} {Label : Type u_2} {μs1 μs2 : List Label} (lts : Lts State Label) : Trans (Lts.MTr.toRelation lts μs1) (Lts.MTr.toRelation lts μs2) (Lts.MTr.toRelation lts (μs1 ++ μs2))

Multi-step transitions can be chained.

Equations

• instTransToRelationHAppendList lts = { trans := ⋯ }

def commandCreate_lts__ : Lean.ParserDescr

A command to create an Lts from a labelled transition α → β → α → Prop, robust to use of variable

Equations

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

def commandLts_transition_notation__ : Lean.ParserDescr

This command adds transition notations for an Lts. This should not usually be called directly, but from the lts attribute.

As an example lts_transition_notation foo "β" will add the notations "[⬝]⭢β" and "[⬝]↠β"

Note that the string used will afterwards be registered as a notation. This means that if you have also used this as a constructor name, you will need quotes to access corresponding cases, e.g. «β» in the above example.

Equations

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

def lts_attr : Lean.ParserDescr

This attribute calls the lts_transition_notation command for the annotated declaration.

Equations

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