Hi Dennis, On Sat, Oct 18, 2014 at 1:07 AM, Dennis Park <emaildpark@gmail.com> wrote:

More specifically, I would like to take an ltl formula

spot::ltl::formula* f

and propagate all negations in f so that negations only occur before atomic propositions. Does the Spot library support such a functionality?

Sure, you can even do it from the command line. % ltlfilt --nnf -f '!G(a -> b)' F(a & !b)

If so, where in the documentation could I find information on it (I tried to look for something like it in the documentation but had trouble finding anything).

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