Intersection of nondeterministic Buchi automata.

The intersection automaton consists of the product of the two automata to be intersected plus a history state which is a pointer to one of the two automata. It waits for the accepting condition of the automaton being pointed to by the history state. Once it sees that, it toggles the history state to wait for the accepting condition of the other automaton. The intersection automaton accepts iff the toggling happens infinitely many times.

The two automata to be intersected are indexed by the type Bool. We choose Bool simply because toggling can be easily modeled by the boolean operation not.

def Cslib.Automata.NA.Buchi.histStart {State : Bool → Type u_2} : ((i : Bool) → State i) → Bool

The initial history state.

Equations

• Cslib.Automata.NA.Buchi.histStart x✝ = false

def Cslib.Automata.NA.Buchi.interAcc {State : Bool → Type u_2} (j : Bool) (acc : (i : Bool) → Set (State i)) : Set (((i : Bool) → State i) × Bool)

The two accepting conditions of the intersection automaton.

Equations

• Cslib.Automata.NA.Buchi.interAcc j acc = {(s, h) : ((i : Bool) → State i) × Bool | s j ∈ acc j ∧ h = j}

noncomputable def Cslib.Automata.NA.Buchi.histTrans {Symbol : Type u_1} {State : Bool → Type u_2} (acc : (i : Bool) → Set (State i)) (s : ((i : Bool) → State i) × Bool) : Symbol → ((i : Bool) → State i) → Bool

The transition function of the history state.

Equations

• Cslib.Automata.NA.Buchi.histTrans acc s x✝¹ x✝ = if s ∈ Cslib.Automata.NA.Buchi.interAcc false acc then true else if s ∈ Cslib.Automata.NA.Buchi.interAcc true acc then false else s.2

noncomputable def Cslib.Automata.NA.Buchi.interNA {Symbol : Type u_1} {State : Bool → Type u_2} (na : (i : Bool) → NA (State i) Symbol) (acc : (i : Bool) → Set (State i)) : NA (((i : Bool) → State i) × Bool) Symbol

The intersection automaton.

Equations

• Cslib.Automata.NA.Buchi.interNA na acc = (Cslib.Automata.NA.iProd na).addHist Cslib.Automata.NA.Buchi.histStart (Cslib.Automata.NA.Buchi.histTrans acc)

def Cslib.Automata.NA.Buchi.interAccept {State : Bool → Type u_2} (acc : (i : Bool) → Set (State i)) : Set (((i : Bool) → State i) × Bool)

The overall accepting conditon of the intersection automaton.

Equations

• Cslib.Automata.NA.Buchi.interAccept acc = Cslib.Automata.NA.Buchi.interAcc false acc ∪ Cslib.Automata.NA.Buchi.interAcc true acc

theorem Cslib.Automata.NA.Buchi.inter_freq_acc_freq_acc {Symbol : Type u_1} {State : Bool → Type u_2} {na : (i : Bool) → NA (State i) Symbol} {acc : (i : Bool) → Set (State i)} {xs : ωSequence Symbol} {ss : ωSequence (((i : Bool) → State i) × Bool)} {i : Bool} (h_run : (interNA na acc).Run xs ss) (h_inf : ∃ᶠ (k : ℕ) in Filter.atTop, ss k ∈ interAcc i acc) : ∃ᶠ (k : ℕ) in Filter.atTop, ss k ∈ interAcc (!i) acc

If the intersection automaton sees one accepting condtion infinitely many times, then it sees the other accepting condition infinitely many times as well.

theorem Cslib.Automata.NA.Buchi.inter_freq_comp_acc_freq_acc {Symbol : Type u_1} {State : Bool → Type u_2} {na : (i : Bool) → NA (State i) Symbol} {acc : (i : Bool) → Set (State i)} {xs : ωSequence Symbol} {ss : ωSequence (((i : Bool) → State i) × Bool)} (h_run : (interNA na acc).Run xs ss) (h_inf_f : ∃ᶠ (k : ℕ) in Filter.atTop, ss k ∈ {s : ((i : Bool) → State i) × Bool | s.1 false ∈ acc false}) (h_inf_t : ∃ᶠ (k : ℕ) in Filter.atTop, ss k ∈ {s : ((i : Bool) → State i) × Bool | s.1 true ∈ acc true}) : ∃ᶠ (k : ℕ) in Filter.atTop, ss k ∈ interAccept acc

If the intersection automaton sees the accepting condtions of both component automata infinitely many times, then its own accepting condition also happens infinitely many times.

@[simp]

theorem Cslib.Automata.NA.Buchi.inter_language_eq {Symbol : Type u_1} {State : Bool → Type u_2} {na : (i : Bool) → NA (State i) Symbol} {acc : (i : Bool) → Set (State i)} : ωAcceptor.language { toNA := interNA na acc, accept := interAccept acc } = ⋂ (i : Bool), ωAcceptor.language { toNA := na i, accept := acc i }

The language accepted by the intersection automaton is the intersection of the languages accepted by the two component automata.