  We study the problem of determinizing $\omega$-automata whose acceptance
condition is defined on the transitions using Boolean formulas, also known as
transition-based Emerson-Lei automata (TELA). The standard approach to
determinize TELA first constructs an equivalent generalized B\"uchi automaton
(GBA), which is later determinized. We introduce three new ways of translating
TELA to GBA. Furthermore, we give a new determinization construction 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. We
also study limit-determinization of TELA and 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 good-for-MDP automata which can be used
for quantitative probabilistic model checking.
