Büchi automata for infinitely often and eventually always

DefinitionInfinitely often#✓fully proved

For a set \(p\) of symbols, the ω-language “infinitely often \(p\)” consists of the infinite words \(x_0 x_1 x_2 \ldots\) with \(x_k \in p\) for infinitely many \(k\).

def infinitelyOften (p : Set Symbol) : ωLanguage Symbol :=
  { xs : ωSequence Symbol | ∃ᶠ k in atTop, xs k ∈ p }

Used by 2

Used byThe infinitely-often automaton recognizes G F φ · Complement of “infinitely often”

DefinitionEventually always#✓fully proved

For a set \(p\) of symbols, the ω-language “eventually always \(p\)” consists of the infinite words \(x_0 x_1 x_2 \ldots\) for which there is an \(N\) with \(x_k \in p\) for all \(k \ge N\).

def eventuallyAlways (p : Set Symbol) : ωLanguage Symbol :=
  { xs : ωSequence Symbol | ∀ᶠ k in atTop, xs k ∈ p }

Used by 2

Used byThe eventually-always automaton recognizes F G φ · Complement of “infinitely often”

TheoremComplement of “infinitely often”#✓fully proved

For every set \(p\) of symbols, the complement of the ω-language of infinite words with infinitely many letters in \(p\) is the ω-language of infinite words whose letters are eventually all in the complement of \(p\).

theorem compl_infinitelyOften (p : Set Symbol) :
    (infinitelyOften p)ᶜ = eventuallyAlways pᶜ

Uses 2

Statement usesEventually always · Infinitely often

DefinitionTwo-state Büchi automaton for “infinitely often”#✓fully proved

For a set \(p\) of symbols, this is the nondeterministic Büchi automaton over the alphabet of symbols with states \(\mathsf{true}\) and \(\mathsf{false}\), single start state \(\mathsf{true}\) and single accepting state \(\mathsf{true}\), in which reading a letter \(x\) from either state leads to exactly one state: \(\mathsf{true}\) if \(x \in p\) and \(\mathsf{false}\) otherwise. So the state records whether the last letter read was in \(p\).

def infinitelyOftenNa (p : Set Symbol) : NA.Buchi Bool Symbol where
  Tr _ x s' := (s' = true ↔ x ∈ p)
  start := {true}
  accept := {true}

Used by 1

Used byThe infinitely-often automaton recognizes G F φ

DefinitionTwo-state Büchi automaton for “eventually always”#✓fully proved

For a set \(p\) of symbols, this is the nondeterministic Büchi automaton over the alphabet of symbols with states \(\mathsf{false}\) and \(\mathsf{true}\), single start state \(\mathsf{false}\) and single accepting state \(\mathsf{true}\). From \(\mathsf{false}\) it may read any letter and move to either state; from \(\mathsf{true}\) it may read only letters in \(p\), and then it stays in \(\mathsf{true}\).

def eventuallyAlwaysNa (p : Set Symbol) : NA.Buchi Bool Symbol where
  Tr s x s' := s = true → x ∈ p ∧ s' = true
  start := {false}
  accept := {true}

Used by 1

Used byThe eventually-always automaton recognizes F G φ

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.