Total LTS

This file defines, and proves some theorems about, the notion of an LTS being "total" and a "totalize" construction that converts any LTS into a 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.Total.chooseFLTS {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 chooseFLTS always provides legal transitions.

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

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

Equations

• lts.chooseOmegaExecution s μs 0 = s
• lts.chooseOmegaExecution s μs n.succ = lts.chooseFLTS.tr (lts.chooseOmegaExecution s μs n) (μs n)

theorem Cslib.LTS.Total.omegaExecution_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.OmegaExecution 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.extend_omegaExecution {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.OmegaExecution 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

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.LTS.instTotalSumUnitTotalize {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : lts.totalize.Total

The LTS constructed by totalize is indeed total.

theorem Cslib.LTS.totalize.no_sink_to_nonsink {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 totalize, there is no finite execution from the sink state to any non-sink state.

@[simp]

theorem Cslib.LTS.totalize.nonsink_tr_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 totalize, the transitions between non-sink states correspond exactly to the transitions in the original LTS.

@[simp]

theorem Cslib.LTS.totalize.nonsink_mtr_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 totalize, the multistep transitions between non-sink states correspond exactly to the multistep transitions in the original LTS.