go back Home
go back Home
# LTL formula to Büchi automata

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.

Contact me at lucareccia@hotmail.it