Fair Adversaries and Randomization in Two-Player Games

Two-player games are used to model open systems. One player models the system, trying to respect some specification, while the other player models the environment. In classical model checking, the objective is to verify that the system can respect its specification, whatever the environment does. In this article, we consider a more realistic scenario when the environment is supposed to be fair. We define a notion of fair player in two-player games. Our solution is inspired by Banach-Mazur games, and leads to a definition of a novel class of 3-player games called ABM-games. For omega-regular specifications on finite arenas, we explore the properties of ABM-games and devise an algorithm for solving them. As the main result, we show that winning in an ABM-game (i.e. winning against a fair player) is equivalent to winning with probability one against the randomized adversary.