Languages determined by pairs of states

def Cslib.LTS.pairLang {Symbol : Type u_1} {State : Type} (lts : LTS State Symbol) (s t : State) : Language Symbol

LTS.pairLang s t is the language of finite words that can take the LTS from state s to state t.

Equations

• lts.pairLang s t = {xs : List Symbol | lts.MTr s xs t}

@[simp]

theorem Cslib.LTS.mem_pairLang {Symbol : Type u_1} {State : Type} {lts : LTS State Symbol} {s t : State} {xs : List Symbol} : xs ∈ lts.pairLang s t ↔ lts.MTr s xs t

@[simp]

theorem Cslib.LTS.pairLang_regular {Symbol : Type u_1} {State : Type} [Finite State] {lts : LTS State Symbol} {s t : State} : (lts.pairLang s t).IsRegular

LTS.pairLang s t is a regular language if there are only finitely many states.

def Cslib.LTS.pairViaLang {Symbol : Type u_1} {State : Type} (lts : LTS State Symbol) (via : Set State) (s t : State) : Language Symbol

LTS.pairViaLang via s t is the language of finite words that can take the LTS from state s to state t via a state in via.

Equations

• lts.pairViaLang via s t = ⨆ r ∈ via, lts.pairLang s r * lts.pairLang r t

@[simp]

theorem Cslib.LTS.mem_pairViaLang {Symbol : Type u_1} {State : Type} {lts : LTS State Symbol} {via : Set State} {s t : State} {xs : List Symbol} : xs ∈ lts.pairViaLang via s t ↔ ∃ r ∈ via, ∃ (xs1 : List Symbol) (xs2 : List Symbol), lts.MTr s xs1 r ∧ lts.MTr r xs2 t ∧ xs1 ++ xs2 = xs

@[simp]

theorem Cslib.LTS.pairViaLang_regular {Symbol : Type u_1} {State : Type} [Inhabited Symbol] [Finite State] {lts : LTS State Symbol} {via : Set State} {s t : State} : (lts.pairViaLang via s t).IsRegular

LTS.pairViaLang via s t is a regular language if there are only finitely many states.

theorem Cslib.LTS.pairLang_append {Symbol : Type u_1} {State : Type} {lts : LTS State Symbol} {s0 s1 s2 : State} {xs1 xs2 : List Symbol} (h1 : xs1 ∈ lts.pairLang s0 s1) (h2 : xs2 ∈ lts.pairLang s1 s2) : xs1 ++ xs2 ∈ lts.pairLang s0 s2

theorem Cslib.LTS.pairLang_split {Symbol : Type u_1} {State : Type} {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2 : List Symbol} (h : xs1 ++ xs2 ∈ lts.pairLang s0 s2) : ∃ (s1 : State), xs1 ∈ lts.pairLang s0 s1 ∧ xs2 ∈ lts.pairLang s1 s2

theorem Cslib.LTS.pairViaLang_append_pairLang {Symbol : Type u_1} {State : Type} {lts : LTS State Symbol} {s0 s1 s2 : State} {xs1 xs2 : List Symbol} {via : Set State} (h1 : xs1 ∈ lts.pairViaLang via s0 s1) (h2 : xs2 ∈ lts.pairLang s1 s2) : xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2

theorem Cslib.LTS.pairLang_append_pairViaLang {Symbol : Type u_1} {State : Type} {lts : LTS State Symbol} {s0 s1 s2 : State} {xs1 xs2 : List Symbol} {via : Set State} (h1 : xs1 ∈ lts.pairLang s0 s1) (h2 : xs2 ∈ lts.pairViaLang via s1 s2) : xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2

theorem Cslib.LTS.pairViaLang_split {Symbol : Type u_1} {State : Type} {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2 : List Symbol} {via : Set State} (h : xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2) : ∃ (s1 : State), xs1 ∈ lts.pairViaLang via s0 s1 ∧ xs2 ∈ lts.pairLang s1 s2 ∨ xs1 ∈ lts.pairLang s0 s1 ∧ xs2 ∈ lts.pairViaLang via s1 s2

theorem Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow {Symbol : Type u_1} {State : Type} [Inhabited Symbol] [Finite State] (na : Buchi State Symbol) : ωAcceptor.language na = ⨆ s ∈ na.start, ⨆ t ∈ na.accept, na.pairLang s t * (na.pairLang t t)^ω

The ω-language accepted by a finite-state Büchi automaton is the finite union of ω-languages of the form L * M^ω, where all Ls and Ms are regular languages.