Embedded Systems Group (ES)

LTL (Linear Temporal Logic) Tools

Using this tool, you can check the validity of a given linear temporal logic formula by translating it to equivalent omega-automata. You can also translate parts of the formula or in some cases even the entire formula to CTL (using the checkbox below). In all cases, note that the negation of the formula is translated to an omega-automaton for checking its emptiness and not the formula itself.

simplify formula first
use F-constraints instead of GF-constraints if possible
translate as much as possible to CTL
translate given LTL formula to LO1