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.