This is implementation of a NL-BCTL*/BCTL* tableau.
Currently the only way to input a formula is to manually play with the URL.
Formulas have syntax defined by the following BNF notation where p is any lowercase letter and n..m is any sequence of digits:
φ := p | (φ ^ φ) | -φ | (φ U φ) | Xφ | Fφ | Gφ | Aφ | Eφ | (φ | φ) | (φ > φ)
These operators are to be read as: atomic (p)roposition, and (^), negation (-), (U)ntil, ne(X)t, (F)inally, (G)lobally/always, on (A)ll paths/futures, there (E)xists a path, or (|), implies (>). If p is an uppercase letter: P, Q, R, then p is interpreted as a (non-local) path atom rather than a state atom.
^hide