Monte Carlo Tree Search Game Play

As of January 2024 ProB has a built-in algorithm for Monte Carlo Tree Search (MCTS). This can for example be used to perform game playing.

In order to make use of MCTS one needs to provide information about the game state of a model by providing DEFINITIONS for:

• GAME_OVER: must be TRUE when the game is finished; for a deadlock the game is also considered over (and by default drawn)
• GAME_VALUE: must evaluate to a number if GAME_OVER is true. 0 is considered a draw, a positive value a win for the max player and a negative value a win for the min player
• GAME_PLAYER: must evaluate to either "min" or "max", depending on which player has to move

The following definitions are optional and influence the MCTS algorithm:

• GAME_MCTS_RUNS
• GAME_MCTS_TIMEOUT
• GAME_MCTS_CACHE_LAST_TREE
• GAME_MCTS_MAX_SIMULATION_LENGTH

A simple example is the Nim game of sticks:

MACHINE Nim_MCTS
CONSTANTS Players, other
PROPERTIES
  Players = {"min","max"} &
  other = {"min"|->"max", "max"|->"min"}
DEFINITIONS
  GAME_OVER == bool(sticks < 1);
  GAME_VALUE == {"max"|->1, "min"|->-1}(player);
  GAME_PLAYER == player;
  GAME_MCTS_RUNS == 100
VARIABLES sticks, player
INVARIANT
 sticks:NATURAL &
 player:Players
INITIALISATION sticks := 5 || player := "max"
OPERATIONS
  Take1 = SELECT sticks>=1 THEN sticks := sticks-1 || player := other(player) END;
  Take2 = SELECT sticks>=2 THEN sticks := sticks-2 || player := other(player) END
END

MCTS tree can be visualised graphically.

MCTS commands are available by right-clicking in Tk operations view.
MCTS_AUTO_PLAY and RANDOM_ANIMATE are available as special event names for VisB.