In game theory, deciding whether a designed player wins a game corresponds to check whether he has a winning strategy. There are situations in which it is important to know whether some extra winning strategy also exists. In this paper we investigate this question over two-player finite games, under the reachability objective. We provide an automata-based technique that, given such a game, it allows to decide in linear time whether the game admits more than a winning strategy. We discuss along the paper some case studies and use them to show how to apply our solution methodology.
Game theory is a very powerful mathematical framework with several useful
applications in different fields. In economics, it is used to deal with solution
concepts such as Nash equilibrium [
In the basic setting, a game consists of two players playing in a turn-based manner, i.e, the moves of the players are interleaved. Solving a two-player game amounts to check whether one of the players has a winning strategy. That is, he can use a sequence of moves (a strategy ) that makes him to satisfy the game target, no matter how his opponent plays. In several settings, however, having instead a more precise (quantitative) answer would be beneficial. For example, in planning a rescue, it would be useful to know whether a robot team has more than a winning strategy from a critical stage, just to have a backup plan in case the scenario changes during the rescue. Such a redundancy allows to strengthen the ability of winning the game and therefore its safety.
In this paper, we address the quantitative question of checking whether a player has more than a strategy to win a two-player finite game G. We investigate this problem under the reachability target and show an automata-based solution to solve it in linear time. Precisely, we build an automaton that accepts only trees that are witnesses of more than one winning strategy for the designed player over the game G. Hence, we reduce the addressed quantitative question to the emptiness of this automaton. To give an evidence of our approach, we report on some cooperative and adversarial game examples.
Related works. Counting strategies has been deeply exploited in the formal
verification setting [
In this section we consider two different case studies of two-player games. In the first case the players behave adversarial. In the second one, they are cooperative. Cop and Robber Game. Assume we have a maze where a cop aims to catch a robber, while the latter, playing adversarial, aims for the opposite. For simplicity, we assume the maze to be a grid divided in rooms, each of them named by its coordinates in the plane (see Figure 1). Each room can have one or more doors that allow the robber and the cop to move from one room to another. Each door has associated a direction along with it can be crossed. Both the cop and the robber can enter every room. The cop, being in a room, can physically block only one of its doors. The robber can move in another room if there is a non-blocked door he can take, placed between the two rooms, with the right direction. The robber wins the game if he can reach one of the safe places (EXIT) situated in the four corners of the maze. Otherwise, the robber is blocked in a room or he can never reach a safe place, and thus the cop wins the game. We assume that both the cop and the robber are initially siting in the middle of the maze, that is in the room (1; 1). Starting from the maze depicted in Figure 1, one can see that the robber has only one strategy to win the game. Consider now two orthogonal variations of the maze. For the first one, consider flipping the direction of the door d12. In this case, the robber loses the game. As second variation, consider flipping the direction of the door d4. Then the robber wins the game and he has now two strategies to accomplish it.
Escape Game. Assume we have an arena similar to the one described in the previous example, but now with a cooperative interaction between two players, a human and a controller, aiming at the same target. Precisely, consider the arena depicted in Figure 2 representing a building where a fire is occurring. The building consists of rooms and, as before, each room has one-way doors and its position is determined by its coordinates. We assume that there is only one exit in the corner (2; 2). One can think of this game as a simplified version of an automatic control station that starts working after an alarm fire occurs and all doors have been closed. Accordingly, we assume that the two players play in turn and at the starting moment all doors are closed. At each control turn, he opens one door of the room in which the human is staying. The human turn consists of taking one of the doors left open if its direction is in accordance with the move. We assume that there is no communication between the players, but the move. We start the game with the human siting in the room (0; 0) and the controller moving first. It is not hard to see that the human can reach the exit trough the doors d1, d4, d7, d10 opened by the controller. Actually, this is the only possible way the human has to reach the exit. Conversely, if we consider the scenario in which the direction of the door d3 is flipped, then there are two strategies to let the human to reach the exit. Therefore, the latter scenario can be considered as better (i.e., more robust) than the former. Clearly, this extra information can be used to improve an exit fire plan at its designing level.
0 1 2 EXIT
!d8 EXIT !d4 H
!d9 d5 !d10 EXIT
In this paper, we consider two-player turn-based games that are suitable to represent the case studies we have introduced in the previous section. Precisely, we consider games consisting of an arena and a target. The arena describes the configurations of the game through a set of states, being partitioned between the two players. In each state, only the player that owns it can take a move. This kind of interaction is also known as token-passing. About the target, we consider the reachability objective, that is some states are declared target. A winning strategy for a designed player is a path from the initial state to a target state. If such a winning strategy exists we say that the player wins the game. Clearly, the player has more than a winning strategy if there are different paths reaching a target state. The formal definition of the considered game model follows. Definition 1. A turn-based two-player reachability game ( 2TRG, for short), played between Player 0 and Player 1, is a tuple G , < St; sI ; tr; W >, where St is a finite non-empty set of states, partitioned in St0 and St1 with Sti being the set of states of Player i, sI 2 St is a designated initial state, W is a set of target states, and tr Sti St1 i, for i 2 f0; 1g is a transition function mapping a state of a player to a state belonging to the other player.
The previous two case studies can be easily modeled using a 2TRG. We now give some details. As set of states we use all the rooms in the maze, together with the status of their doors. For example, the state ((0; 0); fdc1; dc3g) is the initial state of the Escape Game where dic means that the door di is closed. For an open door, instead, we will use the label o in place of c. Formally, let Di;j be the set of doors (up to four) belonging to the room (i; j), which can be flagged either with c (closed) or o (open), then we set St f((i; j); Di;j ) j 0 i; j 2g. Transitions are taken by the human/robber in order to change the room (coordinates) or by the cop/controller to change the status of its doors. These moves are taken in accordance with the shape of the maze. The partitioning of the states between the players follows immediately, as well as the definition of the target states.
To check whether Player 1 has a winning strategy in a 2TRG G one can use a classic backward algorithm. We briefly recall it. Let succ : St ! 2St be the function that for each state s 2 St in G gives the set of its successors. The algorithm starts from a set S equal to W. Iteratively, it tries to increase S by adding all states that sutisfy one following conditions holds: (i) s 2 St0 and succ(s) S; or, (ii) s 2 St1 and succ(s) \ S 6= ;. If S increases at each iteration and at a certain point we enter the initial state, then Player 1 wins the game.
In case one wants to ensure that more than a winning strategy exists, the
above algorithm becomes not appropriate. We use instead a top-down
automatatheoretic approach. To give an intuition of this solution, first consider that in
a 2TRG a witness for a winning strategy is a tree that takes for each node
corresponding to a state s in the game, one successor if s belongs to Player 1, or
all successors, otherwise. Indeed, if all the leaves of this tree are target states,
then surely Player 1 has a winning strategy over the game. In case we want to
ensure that at least two winning strategies exist then at a certain point along the
tree Player 1 must take two successors. We build a tree automaton that accepts
exactly this kind of witness trees. For the lack of space, we omit the definition of
tree and the related concepts. We refer for this to [
Definition 2. A nondeterministic tree automaton (N TA, for short) is a tuple A , < Q; ; q0; ; F >, where Q is a set of states, is an alphabet, q0 2 Q is an initial state, : Q ! 2Q is a transition function mapping pairs of states and symbols to a set of states, and F Q is a set of the accepting states.
An N TA A recognizes trees and works as follows. For a node tree labeled by and A being in a state s, it sends different copies of itself to successors in accordance with . For example, if (s; ) = f(s1; s2); (s3; s4)g either A proceeds with (s1; s2) or (s3; s4), by associating them to two (possibly different) successors. By L(A) we denote the set of trees accepted by A. It is not empty if L(A) 6= ;.
We now give the main result of this paper, i.e. we show that it is possible to decide in linear time whether, in a 2TRG, Player 1 has more than a winning strategy. We later report on the application of this result along the case studies. Theorem 1. For a 2TRG game G it is possible to decide in linear time whether Player 1 has more than a strategy to win the game.
Proof (sketch). Consider a 2TRG game G. We build an N TA A that accepts all trees that are witnesses of more than a winning strategy for Player 1 over G. We briefly describe the automaton. It uses St fok; splitg as set of states where ok and split are flags and the latter is used to remember that along the tree Player 1 has to ensure the existence of two winning strategies by opportunely choosing a point where to "split". We use a one-letter alphabet , as this set takes no role. For the initial state we set q0 = (sI ; split). For the transitions, starting from a state q = (s; f lag), we distinguish between two cases: (i) s 2 St0. If f lag = ok then (q) = succ(s) fokg, otherwise, let succ(s) = fs1; : : : ; sng then (q) = f((s1; f1); : : : ; (sn; fn))g and there exists 1 i n such that fi = split and for all j 6= i, we have fj = ok. (ii) s 2 St1. If f lag = ok then (q) = f((s0; ok))g with s0 2 succ(s), otherwise, we have (q) = f((s0; ok); (s00; ok)); ((s0; split))g, with s0; s00 2 succ(s) and s0 6= s00. The set of accepting states is W fokg. A tree is accepted by A if at a certain point Player 1 can take two successors in G both leading to a target state.
The size of the automaton is just linear in the size of the game. Moreover, by
using the fact that, from [
Consider the Escape Game example. By applying the above construction, the automaton A accepts an empty language. Indeed, for each input tree, A always leads to a leaf containing either a state with a non-target component (i.e., the tree is a witness of a losing strategy) or with a flag split (i.e., Player 1 cannot select two winning strategies). Conversely, consider the same game, but flipping the direction of the door d3 in the maze. In this case, A accepts exactly one tree. Indeed starting from the initial state (((0; 0); fdc1; dc3g); split), A sends two copies of itself to two successors in the tree, respectively with states (((0; 0); fdo1; dc3g); ok) and (((0; 0); fd1; do3g); ok), corresponding to two different winning strategies for c the controller.
A similar reasoning can be exploited with the Cop and Robber Game example. Indeed, the automaton accepts an empty language. Conversely, by flipping the door d4, it accepts the tree that is witnessing of two different winning strategies each of them going through one of the two doors left unblocked by the cop. 5
In this paper we have introduced a simple but effective automata-based methodology to check whether a player has more than a winning strategy in a two-player game under the reachability objective. We have showed how this methodology can be applied in practice by reporting on its use over two different game scenarios, one cooperative and one adversarial. We believe that the solution algorithm we have conceived in this paper can be used as core engine to count strategies in more involved game scenarios and in many solution concepts reasoning.
This work opens to several interesting questions and extensions. For instance,
it would be worth investigating game scenarios in which one or both players
have imperfect information regarding some moves of the other player. The
imperfect information setting is an important field of study in game theory with
several practical applications. For some related works see [