Behavioral properties of open systems can be formalized as objectives in two-player games. Turn-based games model asynchronous interaction between the players (the system and its environment) by interleaving their moves. Concurrent games model synchronous interaction: the players always move simultaneously. Infinitary winning criteria are considered: Büchi, co-Büchi, and more general parity conditions. A generalization of determinacy for parity games to concurrent parity games demands probabilistic (mixed) strategies: either player 1 has a mixed strategy to win with probability 1 (almost-sure winning), or player 2 has a mixed strategy to win with positive probability. This work provides efficient reductions of concurrent probabilistic Büchi and co-Büchi games to turn-based games with Büchi condition and parity winning condition with three priorities, respectively. From a theoretical point of view, the latter reduction shows that one can trade the probabilistic nature of almost-sure winning for a more general parity (fairness) condition. The reductions improve understanding of concurrent games and provide an alternative simple proof of determinacy of concurrent Büchi and co-Büchi games. From a practical point of view, the reductions turn solvers of turn-based games into solvers of concurrent probabilistic games. Thus improvements in the well-studied algorithms for the former carry over immediately to the latter. In particular, a recent improvement in the complexity of solving turn-based parity games yields an improvement in time complexity of solving concurrent probabilistic co-Büchi games from cubic to quadratic.
CITATION STYLE
Jurdziński, M., Kupferman, O., & Henzinger, T. A. (2002). Trading probability for Fairness. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2471, pp. 292–305). Springer Verlag. https://doi.org/10.1007/3-540-45793-3_20
Mendeley helps you to discover research relevant for your work.