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.

翻译：Emerson-Lei条件因其简洁性和组合性质而受到近期关注。本研究展示了如何以两种不同方式分析带有Emerson-Lei目标的无限时长博弈。首先，我们表明Emerson-Lei条件的Zielonka树自然引出了向奇偶博弈的一种新归约方法，但该归约无法实现最优分析。其次，基于第一种归约（及Zielonka树），我们提出了获胜区域的直接不动点特征刻画。该不动点特征刻画支持符号分析，它泛化了已知获胜条件（如Büchi、GR[1]、奇偶、Streett、Rabin和Muller目标）下的博弈求解方案，并在处理这些条件时复现了既有符号算法与复杂度结果。我们还展示了所提算法在反应式综合中的应用潜力，提出一种可符号化处理的新型LTL表达片段。该片段融合了安全规范与活性部分：安全部分无限制，活性部分允许在字母出现上定义Emerson-Lei条件。符号化处理的可行性源于安全语言环境下确定化的简洁性，以及我们提出的新博弈求解算法。该方法最大限度地扩展了符号化求解的步骤范围，以增强高效符号实现的潜力。