Every LTL formula has an equivalent finite-state Büchi automaton #
We assemble the translations LTL → NNF → ABW → NBW to conclude that for any
linear temporal logic formula there is an equivalent finite-state
nondeterministic Büchi automaton accepting the same language. Finiteness comes
from the construction: the alternating automaton's states are subformulas of
the (negation normal form of the) input formula, and the Miyano–Hayashi
breakpoint construction squares that state space to pairs of subsets.