Memoryless Determinacy of Infinite Parity Games: Another Simple Proof
share
The memoryless determinacy of infinite parity games was proven independently by Emerson and Jutla, and Mostowski, with various applications in computer science. Then Zielonka provided an elegant and simple argument. Several simpler proofs can be found in the literature in the case where the underlying graph is finite. These proofs usually proceed by induction on the number of relevant vertices. Recently, Haddad provided an even simpler argument by precisely defining what a relevant vertex is: one that has incoming edges and proper outgoing edges. The proof splits one relevant vertex into two non-relevant ones for the induction step, and concludes after a case disjunction. This note adapts Haddad's technique to the infinite case. A priority is relevant if it labels relevant vertices, and the proof proceeds by induction on the number of relevant priorities (as Zielonka). Haddad's vertex split is replaced with the splitting of many vertices, and the case disjunction with a transfinite induction over the winning regions (as Zielonka). The main difference with Zielonka is that here the notions of traps, attractors, etc., are not used. Memoryless determinacy was generalized by Grädel and Walukiewicz to infinite sets of priorities, but it is unclear whether Haddad's technique can be adapted to such a setting.
READ FULL TEXT