2023/05/04 by Daniel Hausmann, Hausmann, Daniel, Mathieu Lehaut +3 · 1 citation
Computer Science · #Artificial Intelligence in Games #Computer Science and Game Theory (cs.GT) #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2305.02793
openalex publication_date 2023/05/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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üchi, 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.