Buchi Congruence

A special type of right congruences used by J.R. Büchi to prove the closure of ω-regular languages under complementation.

@[implicit_reducible]

def Cslib.Automata.NA.Buchi.BuchiCongruence {Symbol : Type u_1} {State : Type} (na : Buchi State Symbol) : RightCongruence Symbol

Given a Buchi automaton na, two finite words u and v are Buchi-congruent according to na iff for every pair of states s and t of na, both of the following two conditions hold: (1) u can move na from s to t iff v can move na from s to t; (2) u can move na from s to t via an acceptingg states iff v can move na from s to t via an acceptingg states.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Cslib.Automata.NA.Buchi.BuchiCongrParam {Symbol : Type u_1} {State : Type} (na : Buchi State Symbol) (f : State → State → Prop × Prop) : Quotient na.BuchiCongruence.eq

BuchiCongrParam is a parameterization of the equivalence classes of na.BuchiCongruence using the type State → State → Prop × Prop, which is finite if State is.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Automata.NA.Buchi.buchiCongrParam_surjective {Symbol : Type u_1} {State : Type} {na : Buchi State Symbol} : Function.Surjective na.BuchiCongrParam

BuchiCongrParam is surjective.

theorem Cslib.Automata.NA.Buchi.buchiCongruence_fin_index {Symbol : Type u_1} {State : Type} {na : Buchi State Symbol} [Finite State] : Finite (Quotient na.BuchiCongruence.eq)

na.BuchiCongruence is of finite index if na has only finitely many states.

theorem Cslib.Automata.NA.Buchi.buchiCongruence_transfer {Symbol : Type u_1} {State : Type} {na : Buchi State Symbol} {a : Quotient na.BuchiCongruence.eq} {xl yl : List Symbol} {s t : State} (hc : xl ∈ RightCongruence.eqvCls a) (hc' : yl ∈ RightCongruence.eqvCls a) (hp : xl ∈ na.pairLang s t) : ∃ (sl : List State), na.Execution s yl t sl ∧ (xl ∈ na.pairViaLang na.accept s t → ∃ r ∈ na.accept, r ∈ sl)

If xl and yl belong to the same equivalence class of na.BuchiCongruence and xl can move na from state s to state t, then so can yl and, furthermore, if xl makes na go through an accepting state of na, then so can yl.

def Cslib.Automata.NA.Buchi.buchiFamily {Symbol : Type u_1} {State : Type} [Inhabited Symbol] (na : Buchi State Symbol) : Quotient na.BuchiCongruence.eq × Quotient na.BuchiCongruence.eq → ωLanguage Symbol

na.buchiFamily is a family of ω-languages indexed by a pair of equivalence classes of na.BuchiCongruence which will turn out to saturate the ω-language accepted by na and cover all possible ω-sequences.

Equations

• na.buchiFamily (a, b) = Cslib.RightCongruence.eqvCls a * (Cslib.RightCongruence.eqvCls b)^ω

theorem Cslib.Automata.NA.Buchi.mem_buchiFamily {Symbol : Type u_1} {State : Type} {na : Buchi State Symbol} [Inhabited Symbol] {xs : ωSequence Symbol} {a b : Quotient na.BuchiCongruence.eq} : xs ∈ na.buchiFamily (a, b) ↔ ∃ (xl : List Symbol) (xls : ωSequence (List Symbol)), xl ∈ RightCongruence.eqvCls a ∧ (∀ (k : ℕ), xls k ∈ RightCongruence.eqvCls b - 1) ∧ xl ++ω xls.flatten = xs

theorem Cslib.Automata.NA.Buchi.buchiFamily_cover {Symbol : Type u_1} {State : Type} {na : Buchi State Symbol} [Inhabited Symbol] [Finite State] : ⨆ (i : Quotient na.BuchiCongruence.eq × Quotient na.BuchiCongruence.eq), na.buchiFamily i = ⊤

na.buchiFamily is a cover if na has only finitely many states. This theorem uses the Ramsey theorem for infinite graphs and does not depend on any details of na.BuchiCongruence other than that it is of finite index.

theorem Cslib.Automata.NA.Buchi.buchiFamily_saturation {Symbol : Type u_1} {State : Type} {na : Buchi State Symbol} [Inhabited Symbol] : Set.Saturates na.buchiFamily (ωAcceptor.language na)

na.buchiFamily saturates the ω-language accepted by na.