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

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.

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

• Cslib.LTS.Tr.toRelation lts μ s1 s2 = lts.Tr s1 μ s2

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

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

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 [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 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.IsExecution {State : Type u} {Label : Type v} (lts : LTS State Label) (s1 : State) (μs : List Label) (s2 : State) (ss : List State) : Prop

A finite execution, or sequence of transitions.

Equations

• lts.IsExecution s1 μs s2 ss = ∃ (x : ss.length = μs.length + 1), ss[0] = s1 ∧ ss[ss.length - 1] = s2 ∧ ∀ (k : ℕ) {x_1 : k < μs.length}, lts.Tr ss[k] μs[k] ss[k + 1]

theorem Cslib.LTS.isExecution_nonEmpty_states {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μs : List Label} {s2 : State} {ss : List State} (h : lts.IsExecution s1 μs s2 ss) : ss ≠ []

Every execution has a start state.

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

Every state has an execution of zero steps terminating in itself.

theorem Cslib.LTS.IsExecution.stepL {State : Type u} {Label : Type v} {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} {ss : List State} {lts : LTS State Label} (htr : lts.Tr s1 μ s2) (hexec : lts.IsExecution s2 μs s3 ss) : lts.IsExecution s1 (μ :: μs) s3 (s1 :: ss)

Equivalent of MTr.stepL for executions.

theorem Cslib.LTS.isExecution_cons_invert {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μ : Label} {μs : List Label} {s2 : State} {ss : List State} (h : lts.IsExecution s1 (μ :: μs) s2 (s1 :: ss)) : lts.IsExecution ss[0] μs s2 ss

Deconstruction of executions with List.cons.

theorem Cslib.LTS.mTr_isExecution {State : Type u} {Label : Type v} {lts : LTS State Label} {s1 : State} {μs : List Label} {s2 : State} (h : lts.MTr s1 μs s2) : ∃ (ss : List State), lts.IsExecution s1 μs s2 ss

A multistep transition implies the existence of an execution.

theorem Cslib.LTS.isExecution_mTr {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μs : List Label} {s2 : State} {ss : List State} (hexec : lts.IsExecution s1 μs s2 ss) : lts.MTr s1 μs s2

Converts an execution into a multistep transition.

theorem Cslib.LTS.mTr_isExecution_iff {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μs : List Label} {s2 : State} : lts.MTr s1 μs s2 ↔ ∃ (ss : List State), lts.IsExecution s1 μs s2 ss

Correspondence of multistep transitions and executions.

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.MTr.toRelation {State : Type u} {Label : Type v} (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

• Cslib.LTS.MTr.toRelation lts μs s1 s2 = lts.MTr s1 μs s2

Calc tactic support for MTr

instance Cslib.instTransToRelationToRelationConsNil {State : Type u} {Label : Type v} {μ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

• Cslib.instTransToRelationToRelationConsNil lts = { trans := ⋯ }

instance Cslib.instTransToRelationToRelationCons {State : Type u} {Label : Type v} {μ : 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

• Cslib.instTransToRelationToRelationCons lts = { trans := ⋯ }

instance Cslib.instTransToRelationToRelationHAppendListConsNil {State : Type u} {Label : Type v} {μ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

• Cslib.instTransToRelationToRelationHAppendListConsNil lts = { trans := ⋯ }

instance Cslib.instTransToRelationHAppendList {State : Type u} {Label : Type v} {μ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

• Cslib.instTransToRelationHAppendList lts = { trans := ⋯ }

Infinite sequences of transitions

This section treats infinite executions as ω-sequences of transitions.

def Cslib.LTS.ωTr {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (ss : ωSequence State) (μs : ωSequence Label) : Prop

Definition of an infinite execution, or ω-sequence of transitions.

Equations

• lts.ωTr ss μs = ∀ (i : ℕ), lts.Tr (ss i) (μs i) (ss (i + 1))

@[irreducible]

theorem Cslib.LTS.ωTr_mTr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {ss : ωSequence State} {μs : ωSequence Label} (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) : lts.MTr (ss n) (μs.extract n m) (ss m)

Any finite execution extracted from an infinite execution is valid.

theorem Cslib.LTS.ωTr.cons {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {μ : Label} {t : State} {ss : ωSequence State} {μs : ωSequence Label} (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) : lts.ωTr (ωSequence.cons s ss) (ωSequence.cons μ μs)

Prepends an infinite execution with a transition.

theorem Cslib.LTS.ωTr.append {State : Type u_2} {Label : Type u_1} {lts : LTS State Label} {s : State} {μl : List Label} {t : State} {ss : ωSequence State} {μs : ωSequence Label} (hmtr : lts.MTr s μl t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) : ∃ (ss' : ωSequence State), lts.ωTr ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t

Prepends an infinite execution with a finite execution.

Total LTS

class Cslib.LTS.Total {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : Prop

An LTS is total iff every state has a μ-derivative for every label μ.

• total (s : State) (μ : Label) : ∃ (s' : State), lts.Tr s μ s'

  The condition of being total.

noncomputable def Cslib.LTS.chooseFLTS {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) [h : lts.Total] : FLTS State Label

Choose an FLTS that is a "sub-LTS" of a total LTS.

Equations

• lts.chooseFLTS = { tr := fun (s : State) (μ : Label) => Classical.choose ⋯ }

theorem Cslib.LTS.chooseFLTS.total {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) [h : lts.Total] (s : State) (μ : Label) : lts.Tr s μ (lts.chooseFLTS.tr s μ)

The FLTS chosen by LTS.chooseFLTS always provides legal transitions.

noncomputable def Cslib.LTS.chooseωTr {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) [lts.Total] (s : State) (μs : ωSequence Label) : ℕ → State

LTS.chooseωTr builds an infinite execution of a total LTS from any starting state and over any infinite sequence of labels.

Equations

• lts.chooseωTr s μs 0 = s
• lts.chooseωTr s μs n.succ = lts.chooseFLTS.tr (lts.chooseωTr s μs n) (μs n)

theorem Cslib.LTS.Total.ωTr_exists {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} [h : lts.Total] (s : State) (μs : ωSequence Label) : ∃ (ss : ωSequence State), lts.ωTr ss μs ∧ ss 0 = s

If a LTS is total, then there exists an infinite execution from any starting state and over any infinite sequence of labels.

theorem Cslib.LTS.Total.mTr_ωTr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} [Inhabited Label] [ht : lts.Total] {μl : List Label} {s t : State} (hm : lts.MTr s μl t) : ∃ (μs : ωSequence Label) (ss : ωSequence State), lts.ωTr ss (μl ++ω μs) ∧ ss 0 = s ∧ ss μl.length = t

If a LTS is total, then any finite execution can be extended to an infinite execution, provided that the label type is inbabited.

def Cslib.LTS.totalize {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : LTS (State ⊕ Unit) Label

LTS.totalize constructs a total LTS from any given LTS by adding a sink state.

Equations

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

instance Cslib.instTotalSumUnitTotalize {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : lts.totalize.Total

The LTS constructed by LTS.totalize is indeed total.

theorem Cslib.LTS.totalize.not_right_left {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {μs : List Label} {t : State} : ¬lts.totalize.MTr (Sum.inr ()) μs (Sum.inl t)

In LTS.totalize, there is no finite execution from the sink state to any non-sink state.

@[simp]

theorem Cslib.LTS.totalize.tr_left_iff {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {μ : Label} {s t : State} : lts.totalize.Tr (Sum.inl s) μ (Sum.inl t) ↔ lts.Tr s μ t

In LTS.totalize, the transitions between non-sink states correspond exactly to the transitions in the original LTS.

@[simp]

theorem Cslib.LTS.totalize.mtr_left_iff {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {μs : List Label} {s t : State} : lts.totalize.MTr (Sum.inl s) μs (Sum.inl t) ↔ lts.MTr s μs t

In LTS.totalize, the multistep transitions between non-sink states correspond exactly to the multistep transitions in the original LTS.

Definitions about termination

def Cslib.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 Cslib.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 Cslib.LTS.union {State : Type u} {Label : Type v} (lts1 lts2 : LTS State Label) : LTS State Label

The union of two LTSs defined on the same types.

Equations

• lts1.union lts2 = { Tr := lts1.Tr ⊔ lts2.Tr }

def Cslib.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 Cslib.LTS.inl {State : Type u} {Label : Type v} {State' : Type u_1} (lts : LTS State Label) : LTS { x : State ⊕ State' // x.isLeft = true } { _label : 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 Cslib.LTS.inr {State : Type u} {Label : Type v} {State' : Type u_1} (lts : LTS State Label) : LTS { x : State' ⊕ State // x.isRight = true } { _label : 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 Cslib.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

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 LTS.setImageMultistep as List.foldl on LTS.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.

class Cslib.LTS.ImageFinite {State : Type u} {Label : Type v} (lts : LTS State Label) [image_finite : ∀ (s : State) (μ : Label), Finite ↑(lts.image s μ)] : Type

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

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

Equations

• lts.deterministic_imageFinite = { }

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.

Equations

• lts.finiteState_imageFinite = { }

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) [image_finite : ∀ (s : State) (μ : Label), Finite ↑(lts.image s μ)] [finite_state : ∀ (s : State), Finite ↑(lts.outgoingLabels s)] : Type

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

instance Cslib.LTS.finiteState_finitelyBranching {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.

Equations

• lts.finiteState_finitelyBranching = { }

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

Weak transitions (single- and multistep)

class Cslib.HasTau (Label : Type v) : Type v

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

• τ : Label

  The internal transition label, also known as τ.

inductive Cslib.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 Cslib.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 Cslib.LTS.saturate_tr_sTr {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} : lts.saturate.Tr = lts.STr

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

theorem Cslib.LTS.saturate_sTr_tr {Label : Type u_1} {State : Type u_2} {μ : Label} {s : State} [hHasTau : HasTau Label] (lts : LTS State Label) (hμ : μ = HasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ

In a saturated LTS, the transition and saturated transition relations are the same.

theorem Cslib.LTS.mem_saturate_image_τ {Label : Type u_1} {State : Type u_2} {s : State} [HasTau Label] (lts : LTS State Label) : s ∈ lts.saturate.image s HasTau.τ

In a saturated LTS, every state is in its τ-image.

def Cslib.LTS.τClosure {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State

The τ-closure of a set of states S is the set of states reachable by any state in S by performing only τ-transitions.

Equations

• lts.τClosure S = lts.saturate.setImage S Cslib.HasTau.τ

Divergence

def Cslib.LTS.DivergentTrace {Label : Type u_1} [HasTau Label] (μs : ωSequence Label) : Prop

An infinite trace is divergent if every label within it is τ.

Equations

• Cslib.LTS.DivergentTrace μs = ∀ (i : ℕ), μs i = Cslib.HasTau.τ

def Cslib.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 = ∃ (ss : Cslib.ωSequence State) (μs : Cslib.ωSequence Label), lts.ωTr ss μs ∧ ss 0 = s ∧ Cslib.LTS.DivergentTrace μs

theorem Cslib.LTS.divergentTrace_drop {Label : Type u_1} [HasTau Label] {μs : ωSequence Label} (h : DivergentTrace μs) (n : ℕ) : DivergentTrace (ωSequence.drop n μs)

If a trace is divergent, then any 'suffix' is also divergent.

class Cslib.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.

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

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