A detailed presentation on how to switch from a formula expressed in Linear Temporal Logic to a BüchI automata.
This transformation is useful for model checking, we can check if a
given model respect a property expressed in LTL. The
transformation isn't polynomial, but usually the property to
verify are small and the shown algorithm can be further optimized.