<aside> <img src="/icons/report_orange.svg" alt="/icons/report_orange.svg" width="40px" />
Definition: Two player zero-sum games ****on graphs are a common formalism in formal verification. The two players jointly determine an infinite path stepwise, where the owner of the current vertex gets to extend the path to a valid successor.
One player aims to satisfy a given winning condition, such as reaching a target vertex, and the opposing player aims to prevent that.
Under very general conditions, that are satisfied here, such games are determined, meaning that exactly one player has a winning strategy that guarantees a favourable outcome for them no matter their opponent’s choices.
Solving a game refers to the algorithmic task to determine which player has a winning strategy.
</aside>
Cops and Robber Game