Generating Deterministic $ omega$-Automata for most LTL Formulas by the Breakpoint Construction. - Andreas Morgenstern; Klaus Schneider 001; Sven Lamberti (MBMV, 2008)