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.

MCTS Game Play for XTL Files

You can also use MCTS game play for XTL specifications, i.e., where you use Prolog facts start, trans and prop to define a system. The MCTS definitions should be provided as prob_game_info/3 facts. Below is a small example of Nim using an XTL specification:

% a version of Nim using ProB's new MCTS API

% definitions for the XTL interface
start(pos(max,9)). % e.g., we start with 9 sticks
trans(Act,S1,S2) :- move(S1,Act,S2).
prop(S,'='(sticks,V)) :- S=pos(_,V).
prop(S,'='(utility,V)) :- utility(S,V).
prop(S,'='(player,V)) :- player(S,V).

% Game rules proper:

% a player can either remove 1 or 2 sticks
move(pos(P1,M),take1,pos(P2,M1)) :- M>0, M1 is M-1, other_player(P1,P2).
move(pos(P1,M),take2,pos(P2,M1)) :- M>1, M1 is M-2, other_player(P1,P2).

end(pos(_,X)) :- X<1. % the game is over when no sticks are left

utility(pos(max,_),1). % other player took last stick; we won
utility(pos(min,_),-1). % max lost

player(pos(P,_),P).


% definitions for the MCTS API:
prob_game_info('GAME_PLAYER',S,V) :- player(S,V).
prob_game_info('GAME_VALUE',S,V) :- utility(S,V).
prob_game_info('GAME_OVER',S,V) :- (end(S) -> V=true ; V=false).
prob_game_info('GAME_MCTS_RUNS',_,V) :- V=100.