From alternating to nondeterministic Büchi automata

For every alternating Büchi automaton (ABW) over a finite state space we build a nondeterministic Büchi automaton (NBW) accepting the same language, via the Miyano–Hayashi breakpoint construction (ABW.toNBW), and prove ABW.toNBW.lang_eq.

def LeanModelChecking.ABW.toNBW {S Q : Type} (A : ABW S Q) : NBW S

The nondeterministic Büchi automaton obtained from an alternating one A by the Miyano–Hayashi breakpoint construction: states are pairs (X, W) of a current set X and an "obligation" set W of states still owing a visit to A.F.

Equations

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

theorem LeanModelChecking.ABW.toNBW.lang_sub {S Q : Type} {A : ABW S Q} {w : ℕ → S} : A.toNBW.language w → A.language w

theorem LeanModelChecking.lemma1 {α : Type} {a b c : Set α} {h : Disjoint a b} : a = (a ∪ b ∩ c) \ b

def LeanModelChecking.level {S Q : Type} {A : ABW S Q} {w : ℕ → S} {G : RunDAG A w} (i : ℕ) : Set Q

The set of states occupying level i of the run DAG G.

Equations

• LeanModelChecking.level i = {q : Q | (q, i) ∈ G.V}

structure LeanModelChecking.LevelGraph : Type 1

An abstract, finitely-branching levelled graph: each level carries a finite, nonempty type of vertices, and every vertex on level i + 1 has a parent on level i. König's lemma then yields an infinite path.

• level : ℕ → Type

  The type of vertices on each level.

• E (i : ℕ) : self.level i → self.level (i + 1) → Prop

  The edge relation between consecutive levels.

• ex_parent (i : ℕ) (v : self.level (i + 1)) : ∃ (v' : self.level i), self.E i v' v

  Every vertex on level i + 1 has a predecessor on level i.

• fin (i : ℕ) : Finite (self.level i)

  Each level is finite.

• nonempty (i : ℕ) : Nonempty (self.level i)

  Each level is nonempty.

structure LeanModelChecking.LevelGraph.Path (G : LevelGraph) : Type

An infinite path through a LevelGraph: a choice of vertex on each level together with a proof that consecutive choices are connected by an edge.

• f (i : ℕ) : G.level i

  The vertex chosen on each level.

• p (i : ℕ) : G.E i (self.f i) (self.f (i + 1))

  Consecutive chosen vertices are connected by an edge.

@[irreducible]

noncomputable def LeanModelChecking.LevelGraph.ancestor {G : LevelGraph} {i j : ℕ} (hij : i ≤ j) (v : G.level j) : G.level i

The ancestor on level i of a vertex on level j ≥ i, obtained by repeatedly choosing a parent.

Equations

• LeanModelChecking.LevelGraph.ancestor hij v = if eq : i = j then ⋯ ▸ v else LeanModelChecking.LevelGraph.ancestor ⋯ ⋯.choose

theorem LeanModelChecking.LevelGraph.ancestor_refl {G : LevelGraph} {i : ℕ} (v : G.level i) : ancestor ⋯ v = v

theorem LeanModelChecking.LevelGraph.ancestor_1 {G : LevelGraph} {i j : ℕ} (hij : i ≤ j) (v : G.level (j + 1)) : ancestor hij ⋯.choose = ancestor ⋯ v

theorem LeanModelChecking.LevelGraph.ancestor_trans {G : LevelGraph} {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) (v : G.level k) : ancestor hij (ancestor hjk v) = ancestor ⋯ v

theorem LeanModelChecking.LevelGraph.choose_eq {α : Sort u_1} {p : α → Prop} (P : ∃ (a : α), p a) {a : α} (eq : P.choose = a) : p a

theorem LeanModelChecking.LevelGraph.ex_path (G : LevelGraph) : Nonempty G.Path

def LeanModelChecking.helper.p {S Q : Type} {A : ABW S Q} {w : ℕ → S} {G : RunDAG A w} : ℕ → Set Q × Set Q

The canonical run of ABW.toNBW A extracted from a run DAG G of A: at each level it records the set of live states together with the breakpoint obligation set.

Equations

• One or more equations did not get rendered due to their size.
• LeanModelChecking.helper.p 0 = ({A.q₀}, ∅)

theorem LeanModelChecking.ABW.toNBW.lang_sup {S Q : Type} {A : ABW S Q} [Finite Q] {w : ℕ → S} : A.language w → A.toNBW.language w

theorem LeanModelChecking.ABW.toNBW.lang_eq {S Q : Type} (A : ABW S Q) [Finite Q] : A.language = A.toNBW.language