In Formal Verification game theory is a recurring theme. I think that one of the most important applications is to define the Simulation Preorder as a game between two players: Spoiler (he) and Duplicator (she). Given a Transition System (in other words, one set $S$ equipped with a labelled transition relation $S \rightarrow S$) Spoiler, starting from a given state, chooses a transition and makes a move. Duplicator has to match the labelled transition and make a move from her starting state. Then, Spoiler makes another move from his last state and Duplicator has to match that transition again, and game goes on in this way. Spoiler first state simulates Duplicator's first state if she has a winning strategy in this game. In their paper "Advanced automata minimization", Lorenzo Clement and Richard Mayr, define a wide variety of simulation relations using games.

In Formal Verification game theory is a recurring theme. I think that one of the most important applications is to define the Simulation Preorder as a game between two players: Spoiler (he) and Duplicator (she). Given a Transition System (in other words, one set $S$ equipped with a labelled transition relation $S \rightarrow S$) Spoiler, starting from a given state, chooses a transition and makes a move. Duplicator has to match the labelled transition and make a move from her starting state. Then, Spoiler makes another move from his last state and Duplicator has to match that transition again, and game goes on in this way. Spoiler first state simulates Duplicator's first state if she has a winning strategy in this game. In their paper "Advanced automata minimization", Lorenzo Clemente and Richard Mayr, define a wide variety of simulation relations using games.