Add other logics to Spot
Spot currently supports LTL and PSL. It would be nice to be able to read/write other logics of equivalent expressive power. Especially, first-order logic (FO) is equivalent to LTL, and monadic second-order logic (MSO) is equivalent to omega-automata. The translation between FO and LTL is easier when using past operators, which are not supported yet.
-
Add support for past operators in LTL. This may require to update translation algorithms. -
Add support for mu-calculus: input/output, transformations to/from PSL/automata -
Add support for FO: input/output, transformation to/from LTL -
Add support for MSO: input/output, transformation to/from PSL/automata