We suggest an expressive fragment of LTL for which reactive synthesis can be performed by symbolically analyzing games. For general LTL, this kind of analysis is impossible due to the complexity of determinization. Bypasses are either by enumerative handling of determinization or by restricting attention to fragments of the language. Here, we take the second approach and suggest a fragment combining a safety specification and a liveness part. The safety part is unrestricted but allows symbolic treatment due to the simplicity of determinization in the case of safety languages. The liveness part is very general, allowing to define Emerson-Lei conditions on occurrences of letters. We elaborate the construction of an Emerson-Lei game that captures the synthesis problem. We also show how Emerson-Lei games can be analyzed symbolically by providing a fixpoint-based characterization of the winning region, which is obtained from an analysis of the Zielonka tree of the winning condition. Our algorithm 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 algorithms and complexity results; the algorithm solves unrestricted Emerson-Lei games with $n$ nodes, $m$ edges and $k$ colors in time $\mathcal{O}(k!\cdot m\cdot n^k)$ and yields winning strategies with memory $\mathcal{O}(k!)$. The runtime of the resulting overall synthesis algorithm is single-exponential in the size of the liveness part and doubly-exponential in the size of the safety part, as it is for (safety) LTL. However, the trade-off between enumerative and symbolic aspects is maximized by enumeratively analyzing the liveness condition and generating from it a symbolic game analysis algorithm.

翻译：我们提出一种具有表达力的线性时态逻辑(LTL)片段，可通过符号化分析博弈实现其反应式综合。对于通用LTL，由于确定化过程的复杂性，此类分析难以实现。现有解决方案要么采用枚举方式处理确定化，要么限制语言片段。本文采用后一种方案，提出结合安全性规范与活性部分的片段。安全性部分不受限制，但因其语言在确定化上的简洁性而允许符号化处理。活性部分具有高度通用性，可定义字母出现上的Emerson-Lei条件。我们详细阐述了捕捉综合问题的Emerson-Lei博弈构造过程。同时，通过提供基于不动点的获胜区域特征化方法（该方法通过对获胜条件的Zielonka树分析获得），展示了如何符号化分析Emerson-Lei博弈。我们的算法统一处理了Büchi、GR[1]、Parity、Streett、Rabin及Muller等已知获胜条件的博弈解，并在这些条件下复现已有算法与复杂度结果。该算法可在时间$\mathcal{O}(k!\cdot m\cdot n^k)$内求解具有$n$个节点、$m$条边及$k$种颜色的无限制Emerson-Lei博弈，并生成存储量为$\mathcal{O}(k!)$的获胜策略。由此产生的综合算法整体运行时，在活性部分规模上呈单指数复杂度，在安全性部分规模上呈双指数复杂度——这与（安全性）LTL的复杂度一致。但通过枚举分析活性条件并生成符号化博弈分析算法，本方法在枚举与符号化方面实现了最优化权衡。