Skip to content

Generalized Büchi automata

14 fully proved

Generalized Büchi automata and degeneralization

StructureGeneralized Büchi automaton#✓fully proved

A generalized Büchi automaton with states \(S\) and symbols \(\Sigma\) is a nondeterministic automaton (a labelled transition relation on \(S\) together with a set of start states) equipped with a natural number \(k\) and \(k\) acceptance sets \(F_0, \dots, F_{k-1} \subseteq S\). A run is accepting when it visits every acceptance set infinitely often.

structure GenBuchi (State Symbol : Type*) extends NA State Symbol where
  /-- The number of acceptance sets. -/
  k : ℕ
  /-- The acceptance sets. -/
  accept : Fin k → Set State
Used by 20
Used byGeneralized Büchi tableau for an LTL formula · Büchi transition test via the computable counter update · Generalized LTL tableau language equals the formula language · Büchi automaton language equals the LTL formula language · LTL tableau accepts exactly the satisfying words · Tableau acceptance via initial, local and fairness conditions · Computable counter update equals generic degeneralization · Counter sequence of a state sequence · The degeneralization counter reaches every higher value · The degeneralization counter waits for the awaited set · Recursion step of the counter sequence · The counter sequence starts at zero · The degeneralization counter crosses every value below its target · Degeneralization preserves the language · Language of a generalized Büchi automaton · Counter update for degeneralization · The degeneralization counter stays when the awaited set is missed · The degeneralization counter advances on a hit · The degeneralization counter resets at the top · Degeneralization of a generalized Büchi automaton

TheoremLanguage of a generalized Büchi automaton#✓fully proved

An infinite word \(x\) belongs to the language of a generalized Büchi automaton \(g\) with acceptance sets \(F_0, \dots, F_{k-1}\) iff there is a run \(s\) of \(g\) on \(x\) such that for every \(j < k\) there are infinitely many times \(t\) with \(s_t \in F_j\). Here a run of \(g\) on \(x\) is an infinite sequence of states \(s_0, s_1, \dots\) with \(s_0\) a start state and a transition from \(s_i\) to \(s_{i+1}\) labelled \(x_i\) for every \(i\).

theorem mem_language_iff {g : GenBuchi State Symbol} {xs : ωSequence Symbol} :
    xs ∈ language g ↔
      ∃ ss, g.Run xs ss ∧ ∀ j, ∃ᶠ k in atTop, ss k ∈ g.accept j
Uses 1 · Used by 2
Statement usesGeneralized Büchi automaton
Used byTableau acceptance via initial, local and fairness conditions · Degeneralization preserves the language

DefinitionCounter update for degeneralization#✓fully proved

Let \(g\) be a generalized Büchi automaton with acceptance sets \(F_0, \dots, F_{k-1}\). The counter update takes a counter value \(i \in \{0, \dots, k\}\) and a state \(t\) of \(g\) and returns a counter value in \(\{0, \dots, k\}\): if \(i < k\), it returns \(i + 1\) when \(t \in F_i\) and \(i\) when \(t \notin F_i\); if \(i = k\), it returns \(0\).

noncomputable def nextCount (g : GenBuchi State Symbol) (i : Fin (g.k + 1)) (t : State) :
    Fin (g.k + 1) :=
  if h : i.val < g.k then
    if t ∈ g.accept ⟨i.val, h⟩ then ⟨i.val + 1, by have := i.isLt; omega⟩ else i
  else ⟨0, Nat.zero_lt_succ _⟩
Uses 1 · Used by 12
Statement usesGeneralized Büchi automaton
Used byBüchi transition test via the computable counter update · Computable counter update equals generic degeneralization · Counter sequence of a state sequence · The degeneralization counter reaches every higher value · The degeneralization counter waits for the awaited set · Recursion step of the counter sequence · The degeneralization counter crosses every value below its target · Degeneralization preserves the language · The degeneralization counter stays when the awaited set is missed · The degeneralization counter advances on a hit · The degeneralization counter resets at the top · Degeneralization of a generalized Büchi automaton

TheoremThe degeneralization counter stays when the awaited set is missed#✓fully proved

Let \(g\) be a generalized Büchi automaton with acceptance sets \(F_0, \dots, F_{k-1}\) and counter update \(\mathrm{next}\). If \(i \in \{0, \dots, k\}\) satisfies \(i < k\) and the state \(t\) is not in \(F_i\), then \(\mathrm{next}(i, t) = i\).

theorem nextCount_eq_self {g : GenBuchi State Symbol} {i : Fin (g.k + 1)} {t : State}
    (h : i.val < g.k) (ht : t ∉ g.accept ⟨i.val, h⟩) : g.nextCount i t = i
Uses 2 · Used by 2
Statement usesGeneralized Büchi automaton · Counter update for degeneralization
Used byThe degeneralization counter waits for the awaited set · The degeneralization counter crosses every value below its target

TheoremThe degeneralization counter advances on a hit#✓fully proved

Let \(g\) be a generalized Büchi automaton with acceptance sets \(F_0, \dots, F_{k-1}\), let \(i \in \{0, \dots, k\}\) be a counter value and let \(t\) be a state of \(g\). If \(i < k\) and \(t \in F_i\), then the counter update of \(i\) at \(t\) is \(i + 1\).

theorem nextCount_eq_succ {g : GenBuchi State Symbol} {i : Fin (g.k + 1)} {t : State}
    (h : i.val < g.k) (ht : t ∈ g.accept ⟨i.val, h⟩) :
    g.nextCount i t = ⟨i.val + 1, by have := i.isLt; omega⟩
Uses 2 · Used by 2
Statement usesGeneralized Büchi automaton · Counter update for degeneralization
Used byThe degeneralization counter reaches every higher value · The degeneralization counter crosses every value below its target

TheoremThe degeneralization counter resets at the top#✓fully proved

Let \(g\) be a generalized Büchi automaton with \(k\) acceptance sets and let \(i \in \{0, \dots, k\}\) be a counter value. If \(i = k\), then for every state \(t\) of \(g\) the counter update of \(i\) at \(t\) is \(0\).

theorem nextCount_eq_zero {g : GenBuchi State Symbol} {i : Fin (g.k + 1)} {t : State}
    (h : i.val = g.k) : g.nextCount i t = ⟨0, Nat.zero_lt_succ _⟩
Uses 2 · Used by 2
Statement usesGeneralized Büchi automaton · Counter update for degeneralization
Used byThe degeneralization counter crosses every value below its target · Degeneralization preserves the language

DefinitionCounter sequence of a state sequence#✓fully proved

Let \(g\) be a generalized Büchi automaton with \(k\) acceptance sets and let \(s = (s_0, s_1, \dots)\) be an infinite sequence of states. The counter sequence \(c_0, c_1, \dots\) of \(s\), with values in \(\{0, \dots, k\}\), is defined by \(c_0 = 0\) and \(c_{n+1} = \mathrm{next}(c_n, s_{n+1})\), where \(\mathrm{next}\) is the counter update of \(g\). So \(c_n\) is the counter after reading the states \(s_1, \dots, s_n\); the state \(s_0\) is not read.

noncomputable def countSeq (g : GenBuchi State Symbol) (ss : ωSequence State) : ℕ → Fin (g.k + 1)
  | 0 => ⟨0, Nat.zero_lt_succ _⟩
  | n + 1 => g.nextCount (countSeq g ss n) (ss (n + 1))
Uses 2 · Used by 5
Statement usesGeneralized Büchi automaton · Counter update for degeneralization
Used byThe degeneralization counter reaches every higher value · The degeneralization counter waits for the awaited set · Recursion step of the counter sequence · The counter sequence starts at zero · Degeneralization preserves the language

TheoremThe counter sequence starts at zero#✓fully proved

For every generalized Büchi automaton \(g\) and every infinite sequence of states \(s\), the counter sequence of \(s\) has value \(0\) at time \(0\).

theorem countSeq_zero (g : GenBuchi State Symbol) (ss : ωSequence State) :
    g.countSeq ss 0 = ⟨0, Nat.zero_lt_succ _⟩
Uses 2
Statement usesGeneralized Büchi automaton · Counter sequence of a state sequence

TheoremRecursion step of the counter sequence#✓fully proved

Let \(g\) be a generalized Büchi automaton, \(s\) an infinite sequence of states, and \(c_0, c_1, \dots\) the counter sequence of \(s\). For every \(n\), \(c_{n+1} = \mathrm{next}(c_n, s_{n+1})\), where \(\mathrm{next}\) is the counter update of \(g\).

theorem countSeq_succ (g : GenBuchi State Symbol) (ss : ωSequence State) (n : ℕ) :
    g.countSeq ss (n + 1) = g.nextCount (g.countSeq ss n) (ss (n + 1))
Uses 3 · Used by 2
Statement usesGeneralized Büchi automaton · Counter sequence of a state sequence · Counter update for degeneralization
Used byThe degeneralization counter reaches every higher value · The degeneralization counter waits for the awaited set

TheoremThe degeneralization counter waits for the awaited set#✓fully proved

Let \(g\) be a generalized Büchi automaton with acceptance sets \(F_0, \dots, F_{k-1}\), let \(s\) be an infinite sequence of states with counter sequence \(c_0, c_1, \dots\), and let \(i < k\) and \(n\) satisfy \(c_n = i\). If \(m \ge n\) and \(s_{j+1} \notin F_i\) for every \(j\) with \(n \le j < m\), then \(c_m = i\).

theorem countSeq_stay {g : GenBuchi State Symbol} {ss : ωSequence State}
    {i : Fin (g.k + 1)} {n : ℕ} (hi : i.val < g.k) (hc : g.countSeq ss n = i) :
    ∀ {m}, n ≤ m → (∀ j, n ≤ j → j < m → ss (j + 1) ∉ g.accept ⟨i.val, hi⟩) →
      g.countSeq ss m = i
Uses 5 · Used by 1
Statement usesGeneralized Büchi automaton · Counter sequence of a state sequence
Proof usesRecursion step of the counter sequence · Counter update for degeneralization · The degeneralization counter stays when the awaited set is missed
Used byThe degeneralization counter reaches every higher value

TheoremThe degeneralization counter reaches every higher value#✓fully proved

Let \(g\) be a generalized Büchi automaton with acceptance sets \(F_0, \dots, F_{k-1}\), and let \(s\) be an infinite sequence of states that visits every \(F_j\) infinitely often, with counter sequence \(c_0, c_1, \dots\). Then for every time \(n\) and every \(j\) with \(c_n \le j \le k\) there is a time \(m \ge n\) with \(c_m = j\).

The distance \(d = j - c_n\) appears in the statement as a separate variable, and the proof is by induction on \(d\): the first visit to the awaited set after time \(n\) advances the counter by one (the counter stays put until then).

theorem countSeq_reach {g : GenBuchi State Symbol} {ss : ωSequence State}
    (hacc : ∀ j, ∃ᶠ t in atTop, ss t ∈ g.accept j) :
    ∀ d n j, j - (g.countSeq ss n).val = d → (g.countSeq ss n).val ≤ j → j ≤ g.k →
      ∃ m, n ≤ m ∧ (g.countSeq ss m).val = j
Uses 6 · Used by 1
Statement usesGeneralized Büchi automaton · Counter sequence of a state sequence
Proof usesThe degeneralization counter waits for the awaited set · Recursion step of the counter sequence · Counter update for degeneralization · The degeneralization counter advances on a hit
Used byDegeneralization preserves the language

TheoremThe degeneralization counter crosses every value below its target#✓fully proved

Let \(g\) be a generalized Büchi automaton with acceptance sets \(F_0, \dots, F_{k-1}\) and counter update \(\mathrm{next}\), let \(s\) be an infinite sequence of states, and let \(c_0, c_1, \dots\) be any sequence in \(\{0, \dots, k\}\) with \(c_{n+1} = \mathrm{next}(c_n, s_{n+1})\) for every \(n\). Let \(a \le b\) be times with \(c_a = 0\) and \(c_b = d \le k\), and suppose \(c_t \ne k\) for every \(t\) with \(a < t < b\). Then for every \(j < d\) there is a time \(t\) with \(a \le t < b\) such that \(c_t = j\), \(c_{t+1} = j + 1\) and \(s_{t+1} \in F_j\).

The proof is by induction on \(b\), case-splitting the last counter step into stay, advance, or the impossible reset.

theorem counter_cross {g : GenBuchi State Symbol} {cc : ℕ → Fin (g.k + 1)}
    {ss : ωSequence State}
    (hstep : ∀ n, cc (n + 1) = g.nextCount (cc n) (ss (n + 1))) :
    ∀ b a d, a ≤ b → (cc a).val = 0 → (cc b).val = d → ∀ (hd : d ≤ g.k),
      (∀ s, a < s → s < b → (cc s).val ≠ g.k) → ∀ (j : ℕ) (hj : j < d),
      ∃ s, a ≤ s ∧ s < b ∧ (cc s).val = j ∧ (cc (s + 1)).val = j + 1 ∧
        ss (s + 1) ∈ g.accept ⟨j, Nat.lt_of_lt_of_le hj hd⟩
Uses 5 · Used by 1
Statement usesGeneralized Büchi automaton · Counter update for degeneralization
Proof usesThe degeneralization counter stays when the awaited set is missed · The degeneralization counter advances on a hit · The degeneralization counter resets at the top
Used byDegeneralization preserves the language

DefinitionDegeneralization of a generalized Büchi automaton#✓fully proved

Let \(g\) be a generalized Büchi automaton with \(k\) acceptance sets. Its degeneralization is the Büchi automaton over the same alphabet whose states are the pairs \((s, i)\) of a state \(s\) of \(g\) and a counter value \(i \in \{0, \dots, k\}\). On a symbol \(x\) there is a transition from \((s, i)\) to \((s', i')\) iff \(g\) has a transition from \(s\) to \(s'\) on \(x\) and \(i'\) is the counter update of \(i\) at the state \(s'\). The start states are the pairs \((s, 0)\) with \(s\) a start state of \(g\), and the accepting states are the pairs \((s, k)\).

def toBuchi (g : GenBuchi State Symbol) : Buchi (State × Fin (g.k + 1)) Symbol where
  Tr p x q := g.Tr p.1 x q.1 ∧ q.2 = g.nextCount p.2 q.1
  start := {p | p.1 ∈ g.start ∧ p.2 = ⟨0, Nat.zero_lt_succ _⟩}
  accept := {p | p.2.val = g.k}
Uses 2 · Used by 3
Statement usesGeneralized Büchi automaton · Counter update for degeneralization
Used byBüchi automaton for an LTL formula · Büchi automaton language equals the LTL formula language · Degeneralization preserves the language

TheoremDegeneralization preserves the language#✓fully proved

A word is accepted by the degeneralized Büchi automaton iff it is accepted by the generalized Büchi automaton.

theorem language_toBuchi (g : GenBuchi State Symbol) :
    language g.toBuchi = language g
Uses 8 · Used by 1
Statement usesGeneralized Büchi automaton · Degeneralization of a generalized Büchi automaton
Proof usesCounter sequence of a state sequence · The degeneralization counter reaches every higher value · The degeneralization counter crosses every value below its target · Language of a generalized Büchi automaton · Counter update for degeneralization · The degeneralization counter resets at the top
Used byBüchi automaton language equals the LTL formula language

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.