Symbolic Solution of Emerson-Lei Games for Reactive Synthesis

Summary

This partial ingest is based on the extracted full PDF text. Hausmann, Lehaut, and Piterman give a symbolic algorithm for solving infinite-duration games with Emerson-Lei Objectives. The method uses Zielonka trees to derive a direct fixpoint characterization of winning regions, then applies it to Reactive Synthesis for specifications combining an unrestricted safety part with an Emerson-Lei liveness part.

Key Claims

• Emerson-Lei conditions are expressive regular winning conditions that can compactly represent Boolean combinations of colors occurring infinitely or finitely often.
• Existing approaches often solve Emerson-Lei games indirectly, for example by reducing to parity or Rabin games.
• Zielonka trees expose the recursive structure of an Emerson-Lei objective and can drive a direct symbolic fixpoint algorithm.
• The algorithm specializes to known fixpoint algorithms for Buchi, generalized Buchi, GR(1), parity, Streett, Rabin, and Muller conditions.
• A Safety-and-Emerson-Lei LTL fragment can be handled symbolically by translating the safety part to a deterministic symbolic safety automaton and solving the liveness part as an Emerson-Lei game.

Methods / Formalism

• An Emerson-Lei formula is a positive Boolean formula over atoms Inf c and Fin c, interpreted over the set of colors visited infinitely often by a play.
• The Zielonka tree of the condition labels tree nodes by color subsets and alternates between objective-satisfying and objective-violating maximal subsets.
• The paper reduces Emerson-Lei games through the Zielonka tree and then derives a direct fixpoint equation system for the winning region.
• For synthesis, formulas have the shape

$${\varphi }_{safety}\wedge {\varphi }_{EL},$$

where the safety component is compiled to a deterministic symbolic safety automaton and phi_EL is handled as a winning condition over the symbolic game.

• Emerson-Lei Game Solving records the reusable condition, Zielonka-tree, and fixpoint schema.

Evidence / Experiments

• The paper is primarily theoretical. It proves the game-solving and synthesis characterizations and gives worked examples of Zielonka-tree objectives and symbolic strategies.
• The authors report complexity bounds for the symbolic procedure and note that implementation and objective simplification remain future work.
• For a safety part of size n and Emerson-Lei part of size m, the stated synthesis bound is doubly exponential in the safety part and single-exponential in the liveness part, with both determinization and game solving amenable to symbolic implementation.

Connections

• Extends the symbolic safety-synthesis thread from Zhu2020 - A Symbolic Approach to Safety LTL Synthesis by adding a richer liveness condition rather than remaining purely safety-only.
• Helps place GR(1) and parity/Rabin/Streett synthesis inside a broader Emerson-Lei Objectives perspective.
• Useful for Temporal Logic and Formal Methods because it separates the automata cost of safety determinization from the game-solving cost of liveness objectives.
• Provides a conceptual bridge from Safety Games to more general infinite-duration games used in controller synthesis.

Open Questions

• Which Emerson-Lei objectives arising in robotics or AI-control specifications have small enough Zielonka trees for practical symbolic solving?
• Can the proposed Safety-and-Emerson-Lei fragment be implemented competitively against existing GR(1), Rabin, or parity synthesis workflows?
• How should these symbolic game-solving ideas connect to runtime Shielding rather than offline controller synthesis?

Citation

Hausmann, Daniel, Mathieu Lehaut, and Nir Piterman. 2024. “Symbolic Solution of Emerson-Lei Games for Reactive Synthesis.”