• Special Pages
• User

Help

# 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.