Limit-sure Winning in Team Games without Shared Randomness
Authors: Léonard Brice, Thomas A. Henzinger, Alipasha Montaseri, Ali Shafiee, K. S. Thejaswini
Organizations: Institute of Science and Technology Austria Klosterneuburg, Austria · École Polytechnique Fédérale de Lausanne Lausanne, Switzerland · Université libre de Bruxelles Brussels, Belgium
We study concurrent stochastic games in which a team of agents plays against an adversarial environment. If the agents could access a shared source of randomness, then these games reduce to two-player games. Despite being common in the literature on coalition games, this assumption does not accurately model real-world systems. In this paper, we consider the setting where the agents only have access to individual sources of randomness, and must satisfy a given reachability or safety objective. The limit-sure problem asks whether the team can ensure that the objective is satisfied with probability at least 1−λ for every λ>0. For reachability objectives, we show that this problem is NP-complete. For safety objectives, we show that limit-sure winning coincides with almost-sure winning, which is known to lie in P. As a corollary of these results, we conclude that model checking of the qualitative fragment of the logic Individually Randomised ATL -- introduced in the recent work of Brice et al. -- is PNP-complete.
Figures & tables
Figure 1. The team game described in Example 1 . A game graph with three states: a failure state on the left, the initial state in the middle, and a goal state on the right. The failure and goal states are absorbing and drawn with double circles. From the initial state, the play moves to the failure state if both agents cross and the adversary scans. It moves to the goal state if both agents cross and the adversary waits, or if both agents hide and the adversary scans. It stays in the initial state if both agents hide and the adversary waits, or if the agents disagree, whatever the adversary does.
Figure 2. Proof outline for the NP upper bound. Six boxes form a sequence across two rows: limit-sure winning, a Puiseux strategy, polynomial-size action ranks, traps and the forest criterion, one stable encoded response, and weighted matroid intersection.
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 3. The Puiseux-winning team strategy of Example 10 (left) and the MDP it induces for the opponent (right). Boxes show ranks, and black dots are the actions of the opponent. On the left, a table gives the team strategy: each of the two agents crosses with probability epsilon, of rank 1, and hides with probability 1 minus epsilon, of rank 0. On the right, the induced MDP: from the initial state the opponent chooses to scan the first or second robot, with the two actions drawn as black dots. Under either action, the play moves to the failure state with probability epsilon squared (rank 2), to the goal state with probability epsilon times 1 minus epsilon (rank 1), and back to the initial state with probability 1 minus epsilon (rank 0). The goal and failure states are both double-circled.
Figure 4. The Markov chain of Example 14 and its three spanning forests. A Markov chain with transient states 1 and 2 and absorbing roots 3 and 4, drawn with double circles and self-loops of probability 1. State 1 moves to 2 with probability 1/2 and to 3 with probability 1/2. State 2 moves to 1 with probability 3/4 and to 4 with probability 1/4. Next to it are the three spanning forests rooted at 3 and 4, with the chosen edges in bold: first, edges 1 to 2 and 2 to 4, with weight 1/8, so 1 leads to 4; second, edges 2 to 1 and 1 to 3, with weight 3/8, so 1 leads to 3; third, edges 1 to 3 and 2 to 4, with weight 1/8, so 1 leads to 3.
Figure 5. States and their proposition labels. Arrow represents that every action profile and has transition probability 1 to the state. Two panels of states, each drawn as a box with its set of propositions. Base states are blue and hatted copies are orange. Panel (a), constant states: a cycle from t, labelled q and z, to the copy of f, labelled p, to f, labelled q, to the copy of t, labelled p, and back to t. Panel (b), variable states for each i: a chain from the copy of s_i plus, labelled p, to s_i plus, labelled q, to the copy of s_i minus, labelled p, to s_i minus, labelled q. Every arrow is taken with probability 1 under every action profile.
Figure 6. All transition from state si− . Transitions from state s_i minus, labelled q. Case 1: if the index does not match, a self-loop back to s_i minus. Case 2: if the choices are inconsistent, a transition to the copy of f. Case 3: a transition to the copy of t if the literal is y or not y for some y in Y_i, to the copy of s_j plus if the literal is x_j with j less than i, and to the copy of s_j minus if the literal is not x_j with j less than i. Each copy, labelled p, moves under all action profiles to the corresponding base state: f labelled q, t labelled q and z, s_j plus labelled q, and s_j minus labelled q.