Hi Dennis, On Sat, Oct 18, 2014 at 1:07 AM, Dennis Park <emaildpark(a)gmail.com> wrote: Sure, you can even do it from the command line. % ltlfilt --nnf -f '!G(a -> b)' F(a & !b) When you know it's called "negative normal form", it's easier to find :-) But without this, you can start from http://spot.lip6.fr/refdoc/spot-latest/modules.html then click on "rewriting LTL formulae", and explore what is available (the same pages are included in doc/spot.html/ inside the tarball in case you work off line). There are basically two interfaces you may want to use, either the spot::ltl::negative_normal_form() function, or the spot::ltl::ltl_simplifier::negative_normal_form() method. The latter uses a cache to speed up the rewriting of (sub)formulae that have already been seen previously, so this is better if you have multiple formulae to process. The former function is just a wrapper around the latter: it creates a temporary spot::ltl::ltl_simplifier object just for a one-shot usage. Regarding the documentation, I should point that most of the existing transformations applicable to LTL/PSL formulae (including negative normal form) are documented in the file doc/tl/tl.pdf included in the tarball. This document is mostly concerned about detailing what rewriting rules are actually used, but it also points to the function names implementing them. -- Alexandre Duret-Lutz