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 Auto Game Play command is available in ProB Tcl/Tk by right-clicking in the operations view.

The last MCTS tree can be visualised graphically. In ProB Tcl/Tk by right-clicking in the "Operations" pane and selecting "Show last MCTS tree". In ProB2-UI you can view the MCTS tree via the "Graph Visualisation" dialog in the Visualisation menu.

You can also trigger MCTS play in VisB. Here MCTS_AUTO_PLAY is available as special event name.