LTS with a special "internal" transition τ.

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

def Cslib.LTS.τSTr {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : State → State → Prop

Saturated τ-transition relation.

Equations

• lts.τSTr = Relation.ReflTransGen (Cslib.LTS.Tr.toRelation lts Cslib.HasTau.τ)

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 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 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.

theorem Cslib.LTS.sTr_τSTr {Label : Type u_1} {State : Type u_2} {s s' : State} [HasTau Label] (lts : LTS State Label) : lts.STr s HasTau.τ s' ↔ lts.τSTr s s'

STr transitions labeled by HasTau.τ are exactly the τSTr transitions.

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

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

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.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_tr_saturate_sTr {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.τ