Beschreibung:
<jats:title>Abstract</jats:title><jats:p>The topic of this paper is the determinization problem of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\omega $$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML">
<mml:mi>ω</mml:mi>
</mml:math></jats:alternatives></jats:inline-formula>-automata under the <jats:italic>transition-based Emerson-Lei</jats:italic> acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent <jats:italic>generalized Büchi automaton</jats:italic> (GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. The second part of the paper studies limit-determinization of TELA and we show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields <jats:italic>good-for-MDP</jats:italic> automata which can be used for quantitative probabilistic model checking.
</jats:p>