[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