Unified Satisfiability Checker for CTL and Related Logics

Formulas have syntax defined by the following BNF notation where p is any lowercase letter:
φ := p | (φ & φ) | -φ | (φ U φ) | Xφ | Fφ | Gφ | Aφ | Eφ | (φ | φ) | (φ = φ) | (φ > φ) | (φ < φ)

These operators are to be read as: atomic (p)ropostion, and (&), negation (-), (U)ntil, ne(X)t, (F)inally, (G)lobally/always, on (A)ll paths/futures, there (E)xists a path, or (|), equals (=), implies (>) and implied by (<).

To add a new rewrite rule of the form φ → ψ, just enter the formula "φ = ψ" and the system will add it to the list of rewrite rules used to simplify formulas once it verifies that the rule is valid (i.e. the negation is not satisfiable) in our BPATH path-variable variant of BCTL*, and that the rule has not already been added. These rules can be translated into a form readable by existing Term Rewrite Systems such as Waldmeister, see for example the following Waldmeister run. Queries are logged, and may be used for debugging and research purposes. At the moment using "simplify" may well convert CTL formulas into CTL*, and should be avoided for CTL provers (i.e. ctl-rp and anu-*)

See also: [github, Source Code, Rewrite Rules]

 AX AG ((~ AX a) & (~ EG EG a)) : bdd

~( ~( AG ~ AF a ) | a) : bdd

EF((AF ~a)&(AX EG a))' : grbj

^ hide^