Buchi Congruence

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

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.