This tool allows you to check the validity of a given linear temporal logic (LTL) formula by translating it into equivalent omega-automata. The translation to omega-automata takes into account positive/negative occurrences of weak/strong operators to avoid constraints, and will use FG constraints instead of GF constraints if possible and if the corresponding option is selected. You can also translate parts of the formula (or in some cases the whole formula) to CTL using the appropriate option below. In all cases, note that the negation of the formula is translated to an omega-automaton to check its emptiness instead of the formula itself.