[Spot] underlying algorithm of monitor construction

3 Mar 2017

      Hello dear spot devs,

I need to know which construction is used when I'm translating an LTL
formula into a monitor automaton. By that I mean:

    /spot::formula some_ltl;
    spot::translator trans;/
    /trans.set_type(spot::postprocessor::Monitor)
    spot::const_twa_graph_ptr aut = trans.run(some_ltl)/

I couldn't find documentation about this, besides some rather informal
description.
It would be great if you could point me to some more useful
documentation about the algorithm or even better a paper on it.

Best,
Marvin Stenger