Trading Probability for Fairness
================================

Properties of open systems can be modeled as objectives in two-player
games. Depending on the interaction between the system and its
environment, the games may be either turn-based (transitions of the
system and its environment are interleaved) or concurrent (transitions
are taken simultaneously). Depending on the properties we model, the
objectives may be achieved in a finite game (safety properties) or an
infinite game (general properties, specified with Buchi, co-Buchi,
or parity fairness conditions). Finally, winning may be required
surely (the objective should be achieved for sure) or almost surely
(the objective should be achieved with probability 1).  Almost-sure
winning involves randomized strategies for the players and is harder
to analyze. For example, while sure reachability games can be solved
in linear time, the best algorithm for solving almost-sure
reachability is quadratic.

In this paper it is shown that probabilistic concurrent games can be
reduced to non-probabilistic turn-based games with a more general
fairness condition. For example, finding the set of states that are
almost-surely winning for player 1 in a concurrent reachability game
can be reduced to finding the set of states that are surely winning
for player 1 in a turn-based Buchi game. From a theoretical point of
view, the reductions show that it is possible to trade the
probabilistic nature of almost-sure winning by a more general fairness
condition in a game with sure winning.  The reductions improve our
understanding of games and suggest alternative simple proofs of some
known results such as determinacy of concurrent probabilistic Buchi
games.  From a practical point of view, our reductions turn solvers
of non-probabilistic turn-based games into solvers of probabilistic
concurrent games. An improvement in the well-studied algorithms for
the former would immediately carry over to the latter.  In particular,
a recent improvement in the upper bound for non-probabilistic
turn-based parity games allows us to improve the bound for solving
probabilistic concurrent co-Buchi games from cubic to quadratic.