Two-player game

Two-player game is the simplest setting of strategic interaction in game theory: two agents with their own objectives make sequential or simultaneous choices, and the outcome for each depends on the joint choice. In the context of computation and logic, two-player games are often played on graphs: one player (the existential) tries to reach a goal, while the other (the universal) tries to prevent it. This structure is the operational heart of alternating automata, where acceptance is defined as the existence of a winning strategy for the existential player.

The equivalence between two-player games and alternating computation is not decorative. It is the bridge between the mathematical theory of games and the engineering practice of formal verification. Every time a model checker asks whether a system satisfies a safety property, it is asking who wins a two-player game on the system's state graph.