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