Emptiness of Büchi automata

DefinitionSymbol-forgetting transition graph of a Büchi automaton#✓fully proved

For a nondeterministic Büchi automaton, the transition graph has an edge from a state \(s\) to a state \(t\) exactly when the automaton has a transition from \(s\) to \(t\) reading some symbol.

def Step (na : Buchi State Symbol) (s t : State) : Prop :=
  ∃ x, na.Tr s x t

Used by 5

Used byReachability by words is reachability in the transition graph · Nonempty words and paths of positive length · Lasso detection by finite reachability · The lasso condition in the transition graph · Lasso states of a finite Büchi automaton

DefinitionLasso of a Büchi automaton#✓fully proved

A nondeterministic Büchi automaton has a lasso if there are a start state \(s_0\) and an accepting state \(s\) such that the automaton can move from \(s_0\) to \(s\) by reading some finite word \(u\), and from \(s\) back to \(s\) by reading some nonempty finite word \(v\).

def HasLasso (na : Buchi State Symbol) : Prop :=
  ∃ s₀ ∈ na.start, ∃ s ∈ na.accept, (∃ u, na.MTr s₀ u s) ∧ ∃ v, v ≠ [] ∧ na.MTr s v s

Used by 8

Used byFinite-model LTL satisfaction iff no counterexample lasso · Nonempty Büchi languages contain ultimately periodic words · Lasso detection by finite reachability · The lasso condition in the transition graph · An accepted word yields a lasso · Büchi emptiness test · Correctness of the Büchi emptiness test · Lasso characterization of Büchi nonemptiness

TheoremBüchi acceptance condition#✓fully proved

A nondeterministic Büchi automaton accepts an infinite word \(x = x_0 x_1 x_2 \cdots\) if and only if it has a run on \(x\), that is, a sequence of states \(s_0 s_1 s_2 \cdots\) with \(s_0\) a start state and a transition from \(s_k\) to \(s_{k+1}\) reading \(x_k\) for every \(k\), such that \(s_k\) is an accepting state for infinitely many \(k\).

theorem mem_language_iff {xs : ωSequence Symbol} :
    xs ∈ language na ↔ ∃ ss, na.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ na.accept

TheoremLassos give accepted ultimately periodic words#✓fully proved

Let \(\mathcal{A}\) be a nondeterministic Büchi automaton over a nonempty alphabet. Suppose \(s_0\) is a start state and \(s\) an accepting state of \(\mathcal{A}\), that reading the finite word \(u\) the automaton can move from \(s_0\) to \(s\), and that reading a nonempty finite word \(v\) it can move from \(s\) back to \(s\). Then \(\mathcal{A}\) accepts the infinite word \(u v^\omega = u v v v \cdots\).

theorem lasso_mem_language [Inhabited Symbol] {s₀ s : State} {u v : List Symbol}
    (h₀ : s₀ ∈ na.start) (hs : s ∈ na.accept) (hu : na.MTr s₀ u s) (hv : v ≠ [])
    (hvs : na.MTr s v s) : u ++ω (const v).flatten ∈ language na

Used by 2

Used byNonempty Büchi languages contain ultimately periodic words · Lasso characterization of Büchi nonemptiness

TheoremAn accepted word yields a lasso#✓fully proved

If a nondeterministic Büchi automaton with finitely many states accepts some infinite word, then it has a lasso: some accepting state is visited twice along an accepting run, and the run between the two visits is the cycle.

theorem hasLasso_of_mem [Finite State] {xs : ωSequence Symbol} (h : xs ∈ language na) :
    na.HasLasso

Uses 1 · Used by 1

Statement usesLasso of a Büchi automaton

Used byLasso characterization of Büchi nonemptiness

TheoremLasso characterization of Büchi nonemptiness#✓fully proved

For finitely many states, the language of a nondeterministic Büchi automaton is nonempty iff some accepting state is reachable from a start state and lies on a nonempty cycle.

theorem language_nonempty_iff_hasLasso [Finite State] :
    (∃ xs, xs ∈ language na) ↔ na.HasLasso

Uses 3 · Used by 3

Statement usesLasso of a Büchi automaton

Proof usesAn accepted word yields a lasso · Lassos give accepted ultimately periodic words

Used byFinite-model LTL satisfaction iff no counterexample lasso · Nonempty Büchi languages contain ultimately periodic words · Correctness of the Büchi emptiness test

TheoremNonempty Büchi languages contain ultimately periodic words#✓fully proved

Let \(A\) be a nondeterministic Büchi automaton with finitely many states over a nonempty alphabet. If \(A\) accepts some infinite word, then there are finite words \(u\) and \(v\) with \(v\) nonempty such that \(A\) accepts the ultimately periodic word \(u v^\omega = u v v v \cdots\).

theorem exists_lasso_word_of_nonempty [Finite State] [Inhabited Symbol]
    (h : ∃ xs, xs ∈ language na) :
    ∃ u v : List Symbol, v ≠ [] ∧ u ++ω (const v).flatten ∈ language na

Uses 3

Proof usesLasso of a Büchi automaton · Lasso characterization of Büchi nonemptiness · Lassos give accepted ultimately periodic words

15 fully proved

Reduction to graph reachability

TheoremReachability by words is reachability in the transition graph#✓fully proved

For states \(s\) and \(t\) of a nondeterministic Büchi automaton, the automaton can move from \(s\) to \(t\) by reading some finite word (possibly empty) if and only if \(t\) is reachable from \(s\) in zero or more steps of the transition graph, which has an edge from \(p\) to \(q\) when some symbol takes \(p\) to \(q\).

theorem exists_mTr_iff_reflTransGen {s t : State} :
    (∃ u, na.MTr s u t) ↔ ReflTransGen na.Step s t

Uses 1 · Used by 2

Statement usesSymbol-forgetting transition graph of a Büchi automaton

Used byNonempty words and paths of positive length · The lasso condition in the transition graph

TheoremNonempty words and paths of positive length#✓fully proved

For states \(s\) and \(t\) of a nondeterministic Büchi automaton, the automaton can move from \(s\) to \(t\) by reading some nonempty finite word if and only if \(t\) is reachable from \(s\) in one or more steps of the transition graph, which has an edge from \(p\) to \(q\) when some symbol takes \(p\) to \(q\).

theorem exists_ne_nil_mTr_iff_transGen {s t : State} :
    (∃ v, v ≠ [] ∧ na.MTr s v t) ↔ TransGen na.Step s t

Uses 2 · Used by 1

Statement usesSymbol-forgetting transition graph of a Büchi automaton

Proof usesReachability by words is reachability in the transition graph

Used byThe lasso condition in the transition graph

TheoremThe lasso condition in the transition graph#✓fully proved

A nondeterministic Büchi automaton has a lasso if and only if there are a start state \(s_0\) and an accepting state \(s\) such that \(s\) is reachable from \(s_0\) in zero or more steps of the transition graph and \(s\) is reachable from itself in one or more steps; the transition graph has an edge from \(p\) to \(q\) when some symbol takes \(p\) to \(q\).

theorem hasLasso_iff_reachable :
    na.HasLasso ↔ ∃ s₀ ∈ na.start, ∃ s ∈ na.accept,
      ReflTransGen na.Step s₀ s ∧ TransGen na.Step s s

Uses 4 · Used by 1

Statement usesLasso of a Büchi automaton · Symbol-forgetting transition graph of a Büchi automaton

Proof usesReachability by words is reachability in the transition graph · Nonempty words and paths of positive length

Used byLasso detection by finite reachability

Decision procedure

DefinitionFinite set of start states#✓fully proved

For a nondeterministic Büchi automaton with finitely many states and a decidable start set, this is the set of its start states, viewed as a finite set.

def startFin (na : Buchi State Symbol) [DecidablePred (· ∈ na.start)] : Finset State :=
  Finset.univ.filter (· ∈ na.start)

Used by 1

Used byLasso states of a finite Büchi automaton

DefinitionLasso states of a finite Büchi automaton#✓fully proved

For a nondeterministic Büchi automaton with finitely many states, decidable equality of states, a finite alphabet, and decidable transitions, start set and accepting set, the lasso states form the finite set of accepting states \(s\) that are reachable from some start state in zero or more transitions and lie on a nonempty cycle, that is, \(s\) is reachable from itself in one or more transitions.

The set is computed by one reachability closure from all start states, then one cycle closure for each reachable accepting state; each closure takes as many rounds as there are states.

def lassoStates (na : Buchi State Symbol) [∀ s x t, Decidable (na.Tr s x t)]
    [DecidablePred (· ∈ na.start)] [DecidablePred (· ∈ na.accept)] : Finset State :=
  (na.startFin ∪ Relation.transGenFinFrom na.Step na.startFin).filter fun s =>
    s ∈ na.accept ∧ s ∈ Relation.transGenFin na.Step s

Uses 4 · Used by 3

Statement usesSymbol-forgetting transition graph of a Büchi automaton · Finite set of start states · Elements reachable from a point · Elements reachable from a finite set of sources

Used byLasso detection by finite reachability · Büchi emptiness test · Correctness of the Büchi emptiness test

TheoremLasso detection by finite reachability#✓fully proved

Let \(A\) be a nondeterministic Büchi automaton with finitely many states and finitely many symbols, with decidable equality of states, and whose transitions, start states and accepting states are decidable. Then \(A\) has a lasso if and only if its set of lasso states, computed by finite reachability closures as the accepting states that are reachable from a start state and lie on a nonempty cycle, is nonempty.

theorem hasLasso_iff_lassoStates_nonempty : na.HasLasso ↔ na.lassoStates.Nonempty

Uses 8 · Used by 2

Statement usesLasso of a Büchi automaton · Lasso states of a finite Büchi automaton

Proof usesSymbol-forgetting transition graph of a Büchi automaton · The lasso condition in the transition graph · Membership in the set reachable from a point · Membership in the set reachable from finitely many sources · Elements reachable from a point · Elements reachable from a finite set of sources

Used byBüchi emptiness test · Correctness of the Büchi emptiness test

DefinitionBüchi emptiness test#✓fully proved

For a nondeterministic Büchi automaton with finitely many states and finitely many symbols, with decidable equality of states, and whose transitions, start states and accepting states are decidable, the emptiness test returns true exactly when the automaton has no lasso. It decides this by computing the set of lasso states; by the lasso characterization, it returns true iff no infinite word is accepted.

With \(n\) states, \(f\) reachable accepting states and \(k\) symbols, the computation performs at most \(f + 1\) reachability closures of \(O(n^3 k)\) transition tests each.

def isEmptyB (na : Buchi State Symbol) [∀ s x t, Decidable (na.Tr s x t)]
    [DecidablePred (· ∈ na.start)] [DecidablePred (· ∈ na.accept)] : Bool :=
  !decide na.HasLasso

Uses 3 · Used by 3

Statement usesLasso of a Büchi automaton · Lasso detection by finite reachability · Lasso states of a finite Büchi automaton

Used byExecutable full-LTL model checker · Correctness of the executable LTL model checker · Correctness of the Büchi emptiness test

TheoremCorrectness of the Büchi emptiness test#✓fully proved

For a nondeterministic Büchi automaton with finitely many states and finitely many symbols, with decidable equality of states, and whose transitions, start states and accepting states are decidable, the emptiness test returns true if and only if the automaton accepts no infinite word.

theorem isEmptyB_iff : na.isEmptyB = true ↔ language na = ⊥

Uses 5 · Used by 1

Statement usesBüchi emptiness test

Proof usesLasso of a Büchi automaton · Lasso detection by finite reachability · Lasso characterization of Büchi nonemptiness · Lasso states of a finite Büchi automaton

Used byCorrectness of the executable LTL model checker

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.