Emerson-Lei Objectives

Definition

Emerson-Lei objectives are regular infinite-duration winning conditions expressed as positive Boolean combinations of colors that occur infinitely often or only finitely often along a play.

Why It Matters

They provide a compact umbrella for many game objectives used in reactive synthesis, including Buchi, Rabin, Streett, Muller, parity, and GR(1)-style conditions. That makes them useful when a temporal specification is richer than pure safety but still should be solved symbolically.

Formalism / Key Objects

• Fix a finite color set C. An Emerson-Lei formula is a positive Boolean formula over atoms Inf c and Fin c for c in C.
• Given D subseteq C, interpreted as the set of colors visited infinitely often:

$$D\models Infc⟺c\in D,D\models Finc⟺c\notin D.$$

• A play wins when the set of colors seen infinitely often satisfies the Emerson-Lei formula.
• A Zielonka tree compactly represents the recursive structure of the objective and can drive game-solving algorithms.
• Emerson-Lei Game Solving records the Zielonka-tree and fixpoint machinery.

Connections

• Reactive Synthesis can combine a deterministic safety automaton with an Emerson-Lei liveness objective.
• Safety Games are the pure safety case; Emerson-Lei games cover more general infinite-duration objectives.
• Linear Temporal Logic specifications can sometimes be compiled into safety plus Emerson-Lei structure.
• EXPTIME and higher complexity classes matter because exact realizability can remain expensive even for useful fragments.

Common Confusions

• Emerson-Lei objectives are game objectives, not a separate temporal logic syntax for writing end-user specifications.
• Fin c does not mean the color occurs finitely many times in a finite trace; it means only finitely often along an infinite play.
• Compact objective syntax does not guarantee small strategy memory or a small Zielonka tree.

Key Sources

• Hausmann2024 - Symbolic Solution of Emerson-Lei Games for Reactive Synthesis