Down the Borel hierarchy: solving Muller games via safety games

DOI10.1016/J.TCS.2014.01.017zbMATH Open1314.91053OpenAlexW1994610451MaRDI QIDQ477197FDOQ477197

Authors Daniel Neider, Roman Rabinovich, Martín G. Zimmermann

Publication date 2 December 2014

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.2457

zbMATH Keywords

Muller gamessafety gamesgame reductionspermissive strategies

Mathematics Subject Classification ID

Formal languages and automata (68Q45) 2-person games (91A05) Specification and verification (program logics, model checking, etc.) (68Q60) Games involving graphs (91A43)

Abstract: We transform a Muller game with n vertices into a safety game with (n!)^3 vertices whose solution allows to determine the winning regions of the Muller game and to compute a finite-state winning strategy for one player. This yields a novel antichain-based memory structure and a natural notion of permissive strategies for Muller games. Moreover, we generalize our construction by presenting a new type of game reduction from infinite games to safety games and show its applicability to several other winning conditions.

Recommendations

• scientific article; zbMATH DE number 7340147
• What kind of memory is needed to win infinitary Muller games?
• Playing Safe
• scientific article; zbMATH DE number 1017515
• scientific article; zbMATH DE number 1096547

Cites work

• scientific article; zbMATH DE number 722611 (Why is no real title available?)
• scientific article; zbMATH DE number 1500523 (Why is no real title available?)
• Antichains and compositional algorithms for LTL synthesis
• Automata, logics, and infinite games. A guide to current research
• Better Quality in Synthesis through Quantitative Objectives
• Bounded Synthesis
• Cost-parity and cost-Streett games
• Explicit Muller games are PTIME
• Faster algorithms for mean-payoff games
• Finitary winning in \({\omega}\)-regular games
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Infinite games played on finite graphs
• Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited
• Permissive strategies: from parity games to safety games
• Playing Muller games in a hurry
• Playing infinite games in finite time.
• Playing pushdown parity games in a hurry
• Small strategies for safety games
• Symbolic synthesis of finite-state controllers for request-response specifications
• Time-Optimal Winning Strategies for Poset Games

Cited in

(8)

• Compositional construction of most general controllers
• scientific article; zbMATH DE number 7340147 (Why is no real title available?)
• Playing Muller games in a hurry
• Quantitative reductions and vertex-ranked infinite games
• What kind of memory is needed to win infinitary Muller games?
• Synthesizing permissive winning strategy templates for parity games
• Assume-admissible synthesis
• Computer Science Logic

Describes a project that uses

Uses Software

• GAVS

This page was built for publication: Down the Borel hierarchy: solving Muller games via safety games

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q477197)