CSL Conference 2007 Invited Paper
Abstract We consider zero-sum repeated games with omega-regular goals. Such hgames are played on a finite state space over an infinite number of rounds: at every round, the players select moves, either in turns or simultaneously; the current state and the selected moves determine the successor state. A play of the game thus consists in an infinite path over the state space or, if randomization is present, in a probability distribution over paths. Omega-regular goals generalize the class of regular goals (those expressible by finite automata) to infinite sequences, and include many well-known goals, such as the reachability and safety goals, as well as the Büchi and parity goals. The algorithms for solving repeated games with omega-regular goals can be broadly divided into enumerative and symbolic/ algorithms. Enumerative algorithms consider each state individually; currently, they achieve the best worst-case complexity among the known algorithms. Symbolic algorithms compute in terms of sets of states, or functions from states to real numbers, rather than single states; such sets or functions can often be represented symbolically (hence the name of the algorithms). Even though symbolic algorithms often cannot match the worst-case complexity of the enumerative algorithms, they are often efficient in practice. We illustrate how symbolic algorithms provide uniform solutions of many classes of repeated games, from turn-based, non-randomized games where at each state one of the players can deterministically win, to concurrent and randomized games where the ability to win must be characterized in probabilistic fashion. We also show that the symbolic algorithms, and the notation used to express them, are closely related to game metrics which provide a notion of distance between game states. Roughly, the distance between two states measures how closely a player can match, from one state, the ability of winning from the other state with respect to any omega-regular goal.