[Spot] underlying algorithm of monitor construction

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