Down the Borel hierarchy: solving Muller games via safety games

DOI10.1016/J.TCS.2014.01.017zbMATH Open1314.91053arXiv1210.2457OpenAlexW1994610451MaRDI 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)

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.

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

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

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)

Cites Work

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

Cited In (7)

• Title not available (Why is that?)
• Compositional construction of most general controllers
• What kind of memory is needed to win infinitary Muller games?
• Quantitative reductions and vertex-ranked infinite games
• Computer Science Logic
• Synthesizing permissive winning strategy templates for parity games
• Assume-admissible synthesis

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)