Divergence of LTS

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