Alternating Büchi automata

We define positive Boolean formulas (PositiveBool), alternating Büchi automata (ABW), their run DAGs (RunDAG), and the language they accept.

inductive LeanModelChecking.PositiveBool (Q : Type) : Type

A positive Boolean formula over a set of atoms Q: a formula built from atoms, true, false, conjunction, and disjunction (no negation).

• atom {Q : Type} (q : Q) : PositiveBool Q
• true {Q : Type} : PositiveBool Q
• false {Q : Type} : PositiveBool Q
• and {Q : Type} (ψ₁ ψ₂ : PositiveBool Q) : PositiveBool Q
• or {Q : Type} (ψ₁ ψ₂ : PositiveBool Q) : PositiveBool Q

def LeanModelChecking.PositiveBool.Sat {Q : Type} (Y : Set Q) : PositiveBool Q → Prop

PositiveBool.Sat Y f holds when the set Y of atoms satisfies the positive Boolean formula f (reading atoms as "is a member of Y").

Equations

• LeanModelChecking.PositiveBool.Sat Y (LeanModelChecking.PositiveBool.atom q) = (q ∈ Y)
• LeanModelChecking.PositiveBool.Sat Y LeanModelChecking.PositiveBool.true = True
• LeanModelChecking.PositiveBool.Sat Y LeanModelChecking.PositiveBool.false = False
• LeanModelChecking.PositiveBool.Sat Y (ψ₁.and ψ₂) = (LeanModelChecking.PositiveBool.Sat Y ψ₁ ∧ LeanModelChecking.PositiveBool.Sat Y ψ₂)
• LeanModelChecking.PositiveBool.Sat Y (ψ₁.or ψ₂) = (LeanModelChecking.PositiveBool.Sat Y ψ₁ ∨ LeanModelChecking.PositiveBool.Sat Y ψ₂)

theorem LeanModelChecking.PositiveBool.Sat.monotone {Q : Type} {f : PositiveBool Q} {A B : Set Q} : A ⊆ B → Sat A f → Sat B f

structure LeanModelChecking.ABW (S Q : Type) : Type

An alternating Büchi automaton over input alphabet S and state space Q.

• q₀ : Q

  The initial state.

• δ : Q → S → PositiveBool Q

  The transition function, mapping a state and a letter to a positive Boolean formula over the successor states.

• F : Set Q

  The set of accepting (final) states.

structure LeanModelChecking.DAG.Base (Q : Type u_1) : Type u_1

The underlying data of a directed acyclic graph whose vertices are state/level pairs: a vertex set V and an edge set E.

• V : Set (Q × ℕ)

  The set of vertices, each a state paired with a level.

• E : Set ((Q × ℕ) × Q)

  The set of edges, each from a state/level pair to a successor state.

structure LeanModelChecking.DAG (Q : Type u_1) extends LeanModelChecking.DAG.Base Q : Type u_1

A directed acyclic graph of state/level pairs in which every edge connects a vertex on level i to a vertex on level i + 1.

• V : Set (Q × ℕ)
• E : Set ((Q × ℕ) × Q)
• edge_closure (e : (Q × ℕ) × Q) : e ∈ self.E → e.fst ∈ self.V ∧ (e.snd, e.fst.snd + 1) ∈ self.V

  Every edge starts at a vertex of V and ends at a vertex on the next level.

def LeanModelChecking.DAG.path {Q : Type u_1} (G : DAG Q) (p : ℕ → Q) : Prop

Infinite path, with an arbitrary starting level.

Equations

• G.path p = ∃ (n : ℕ), ∀ (i : ℕ), ((p i, n + i), p (i + 1)) ∈ G.E

structure LeanModelChecking.RunDAG {S Q : Type} (A : ABW S Q) (w : ℕ → S) extends LeanModelChecking.DAG Q : Type

A run DAG of the automaton A on the word w: a DAG rooted at the initial state in which every vertex's successors satisfy the relevant transition formula.

• V : Set (Q × ℕ)
• E : Set ((Q × ℕ) × Q)
• edge_closure (e : (Q × ℕ) × Q) : e ∈ self.E → e.fst ∈ self.V ∧ (e.snd, e.fst.snd + 1) ∈ self.V
• p_root : (A.q₀, 0) ∈ self.V

  The initial state sits at the root (level 0).

• p_sat (v : Q × ℕ) : v ∈ self.V → match v with | (q, i) => ∃ (Y : Set Q), PositiveBool.Sat Y (A.δ q (w i)) ∧ {(q, i)} ×ˢ Y ⊆ self.E

  Each vertex has a set of successors satisfying its transition formula.

def LeanModelChecking.RunDAG.accepting {S Q : Type} {A : ABW S Q} {w : ℕ → S} (G : RunDAG A w) : Prop

A run DAG is accepting when every infinite path through it visits an accepting state infinitely often.

Equations

• G.accepting = ∀ (p : ℕ → Q), G.path p → ∀ (i : ℕ), ∃ (j : ℕ), j ≥ i ∧ p j ∈ A.F

def LeanModelChecking.ABW.language {S Q : Type} (A : ABW S Q) (w : ℕ → S) : Prop

The automaton A accepts the word w when it admits an accepting run DAG.

Equations

• A.language w = ∃ (G : LeanModelChecking.RunDAG A w), G.accepting