wiki

Emerson-Lei Game Solving

2 min read

Emerson-Lei Game Solving

Context

Hausmann2024 - Symbolic Solution of Emerson-Lei Games for Reactive Synthesis uses Emerson-Lei objectives and Zielonka trees to solve richer infinite-duration games symbolically, then applies that machinery to synthesis formulas with a safety part and an Emerson-Lei liveness part.

Formal Statement

Let C be a finite color set. An Emerson-Lei formula is a positive Boolean formula over atoms Inf c and Fin c. For a play, let D subseteq C be the set of colors that occur infinitely often. Satisfaction of atoms is:

The play is winning for the existential player when D satisfies the Emerson-Lei formula. A Zielonka tree Z_phi recursively labels nodes by color subsets and exposes the alternation between objective-satisfying and objective-violating maximal subsets.

Derivation / Construction

  • Build the Zielonka tree for the Emerson-Lei formula.
  • Use the tree to reduce the Emerson-Lei game to a parity-game-like structure, or directly derive a fixpoint equation system.
  • Solve the fixpoint equation system symbolically over sets of game states.
  • Extract a winning strategy from the computed winning region and the choices made at relevant Zielonka-tree nodes.
  • For synthesis formulas phi_safety and phi_EL, first compile phi_safety to a deterministic symbolic safety automaton, then solve the induced symbolic game with phi_EL as the Emerson-Lei objective.

Implications

The method generalizes several familiar objectives while retaining symbolic set-based reasoning. Its practical value depends heavily on the size and shape of the Zielonka tree. The paper’s Safety-and-Emerson-Lei fragment suggests a path between pure safety synthesis and full LTL synthesis: keep the safety determinization separate, then use a structured liveness objective instead of going straight to generic parity games.

Graph View

Backlinks