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