Converting from LTS to FLTS

def Cslib.LTS.toFLTS {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : FLTS (Set State) Label

Converts an LTS into an FLTS using the subset construction.

Equations

• lts.toFLTS = { tr := lts.setImage }

theorem Cslib.LTS.toFLTS_mem_tr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {S : Set State} {s' : State} {μ : Label} : s' ∈ lts.toFLTS.tr S μ ↔ ∃ s ∈ S, lts.Tr s μ s'

Characterisation of transitions in LTS.toFLTS wrt transitions in the original LTS.

theorem Cslib.LTS.toFLTS_mem_mtr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {S : Set State} {s' : State} {μs : List Label} : s' ∈ lts.toFLTS.mtr S μs ↔ ∃ s ∈ S, lts.MTr s μs s'

Characterisation of multistep transitions in LTS.toFLTS wrt multistep transitions in the original LTS.

theorem Cslib.LTS.toFLTS_mtr_setImageMultistep {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} : lts.toFLTS.mtr = lts.setImageMultistep

Characterisation of multistep transitions in LTS.toFLTS as image transitions in LTS.