  Emerson-Lei conditions have recently attracted attention due to their
succinctness and compositionality properties. In the current work, we show how
infinite-duration games with Emerson-Lei objectives can be analyzed in two
different ways. First, we show that the Zielonka tree of the Emerson-Lei
condition gives rise naturally to a new reduction to parity games. This
reduction, however, does not result in optimal analysis. Second, we show based
on the first reduction (and the Zielonka tree) how to provide a direct
fixpoint-based characterization of the winning region. The fixpoint-based
characterization allows for symbolic analysis. It generalizes the solutions of
games with known winning conditions such as B\"uchi, GR[1], parity, Streett,
Rabin and Muller objectives, and in the case of these conditions reproduces
previously known symbolic algorithms and complexity results.
  We also show how the capabilities of the proposed algorithm can be exploited
in reactive synthesis, suggesting a new expressive fragment of LTL that can be
handled symbolically. Our fragment combines a safety specification and a
liveness part. The safety part is unrestricted and the liveness part allows to
define Emerson-Lei conditions on occurrences of letters. The symbolic treatment
is enabled due to the simplicity of determinization in the case of safety
languages and by using our new algorithm for game solving. This approach
maximizes the number of steps solved symbolically in order to maximize the
potential for efficient symbolic implementations.
