We study Recursive Concurrent Stochastic Games (RCSGs), extending our recent analysis of recursive simple stochastic games to a concurrent setting where the two players choose moves simultaneously and independently at each state. For multi-exit games, our earlier work already showed undecidability for basic questions like termination, thus we focus on the important case of single-exit RCSGs (1-RCSGs).
We first characterize the value of a 1-RCSG termination game as the least fixed point solution of a system of nonlinear minimax functional equations, and use it to show PSPACE decidability for the quantitative termination problem. We then give a strategy improvement technique, which we use to show that player 1 (maximizer) has ε-optimal randomized Stackless & Memoryless (r-SM) strategies for all ε> 0, while player 2 (minimizer) has optimal r-SM strategies. Thus, such games are r-SM-determined. These results mirror and generalize in a strong sense the randomized memoryless determinacy results for finite stochastic games, and extend the classic Hoffman-Karp strategy improvement approach from the finite to an infinite state setting. The proofs in our infinite-state setting are very different however, relying on subtle analytic properties of certain power series that arise from studying 1-RCSGs.
We show that our upper bounds, even for qualitative (probability 1) termination, can not be improved, even to NP, without a major breakthrough, by giving two reductions: first a P-time reduction from the long-standing square-root sum problem to the quantitative termination decision problem for finite concurrent stochastic games, and then a P-time reduction from the latter problem to the qualitative termination problem for 1-RCSGs.
In general, finite concurrent two-player reachability games are only determined in a weak sense: the supremum probability to win can be approached via stochastic strategies, but cannot be realized. We introduce a class of concurrent games that are determined in a much stronger sense, and in a way, it is the larger class with this property. To this end, we introduce the notion of \emph{local interaction} at a state of a graph game: it is a \emph{game form} whose outcomes (i.e. a table whose entries) are the next states, which depend on the concurrent actions of the players. By definition, a gam…
We investigate concurrent two-player win/lose stochastic games on finite graphs with prefix-independent objectives. We characterize subgame optimal strategies and use this characterization to show various memory transfer results: 1) For a given (prefix-independent) objective, if every game that has a subgame almost-surely winning strategy also has a positional one, then every game that has a subgame optimal strategy also has a positional one; 2) Assume that the (prefix-independent) objective has a neutral color. If every turn-based game that has a subgame almost-surely winning strategy also ha…
Representation theorems for actual and alpha powers over general concurrent game frames without assuming independence of agents
Institute for Logic, Language and Computation, University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；School of Philosophy, Beijing Normal University（北京师范大学哲学学院）；Department of Information Science and Media Studies, University of Bergen（卑尔根大学信息科学与媒体研究系）；School of Philosophy, Shanxi University（山西大学哲学学院）
Game-theoretic techniques and equilibria analysis facilitate the design and verification of competitive systems. While algorithmic complexity of equilibria computation has been extensively studied, practical implementation and application of game-theoretic methods is more recent. Tools such as PRISM-games support automated verification and synthesis of zero-sum and (epsilon-optimal subgame-perfect) social welfare Nash equilibria properties for concurrent stochastic games. However, these methods become inefficient as the number of agents grows and may also generate equilibria that yield signifi…
The problem of finding pure strategy Nash equilibria in multiagent concurrent games with finite-horizon temporal goals has received some recent attention. Earlier work solved this problem through the use of Rabin automata. In this work, we take advantage of the finite-horizon nature of the agents' goals and show that checking for and finding pure strategy Nash equilibria can be done using a combination of safety games and lasso testing in Büchi automata. To separate strategic reasoning from temporal reasoning, we model agents' goals by deterministic finite-word automata (DFAs), since finite-ho…
We study two-player concurrent stochastic games on finite graphs, with Büchi and co-Büchi objectives. The goal of the first player is to maximize the probability of satisfying the given objective. Following Martin's determinacy theorem for Blackwell games, we know that such games have a value. Natural questions are then: does there exist an optimal strategy, that is, a strategy achieving the value of the game? what is the memory required for playing (almost-)optimally? The situation is rather simple to describe for turn-based games, where positional pure strategies suffice to play optimally in…
Concurrent multi-player games with $ω$-regular objectives are a standard model for systems that consist of several interacting components, each with its own objective. The standard solution concept for such games is Nash Equilibrium, which is a "stable" strategy profile for the players. In many settings, the system is not fully observable by the interacting components, e.g., due to internal variables. Then, the interaction is modelled by a partial information game. Unfortunately, the problem of whether a partial information game has an NE is not known to be decidable. A particular setting of p…
Representation theorems for actual and alpha powers over two-agent general concurrent game frames
Institute for Logic, Language and Computation, University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；School of Philosophy, Beijing Normal University（北京师范大学哲学学院）；Department of Information Science and Media Studies, University of Bergen（卑尔根大学信息科学与媒体研究系）；School of Philosophy, Shanxi University（山西大学哲学学院）
University of Oxford（牛津大学）；University of Göteborg（哥德堡大学）
In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we study the design of incentives so that a desirable equilibrium is obtained, for instance, an equilibrium satisfying a given temporal logic property -- a problem that we call equilibrium design. We base our study on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players' goals as mean-payoff objectives. In particular, we consider system specifications given b…
We present two recursive strategy improvement algorithms for solving simple stochastic games. First we present an algorithm for solving SSGs of degree $d$ that uses at most $O\left(\left\lfloor(d+1)^2/2\right\rfloor^{n/2}\right)$ iterations, with $n$ the number of MAX vertices. Then, we focus on binary SSG and propose an algorithm that has complexity $O\left(φ^nPoly(N)\right)$ where $φ= (1 + \sqrt{5})/2$ is the golden ratio. To the best of our knowledge, this is the first deterministic strategy improvement algorithm that visits $2^{cn}$ strategies with $c < 1$.
We show that the problem of deciding whether in a multi-player perfect information recursive game (i.e. a stochastic game with terminal rewards) there exists a stationary Nash equilibrium ensuring each player a certain payoff is Existential Theory of the Reals complete. Our result holds for acyclic games, where a Nash equilibrium may be computed efficiently by backward induction, and even for deterministic acyclic games with non-negative terminal rewards. We further extend our results to the existence of Nash equilibria where a single player is surely winning. Combining our result with known g…
我们考虑在有限状态空间上进行无限回合的2人博弈。游戏是并行的：在每一轮中，两个玩家同时选择他们的动作;当前状态和动作决定继任者。我们认为欧米茄经常获胜的条件作为平价目标。我们考虑的定性分析问题：几乎肯定和有限肯定获胜的状态集的计算，其中玩家1可以确保赢得概率1和概率任意接近1，分别。一般来说，几乎肯定和有限肯定获胜策略需要无限记忆和无限精度。本文研究了并发奇偶博弈定性分析的有限理性问题，其中策略集参与人1被限制为有限资源策略。就精度而言，策略可以是确定性的、均匀的、有限精度的或无限精度的;就记忆而言，策略可以是无记忆的、有限记忆的或无限记忆的。我们提出了一个精确和完整的定性获胜集的所有组合类的策略的特征。特别是，我们表明，统一的无记忆策略是强大的有限精度的无限记忆策略，和无限精度的无记忆策略是强大的无限精度的有限记忆策略。我们证明了获胜集可以在O（n^{2d+3}）时间内计算，其中n是游戏的大小，2d是优先级的数量，并且我们的算法是符号的。在NP cap coNP中可以判定一个状态是否属于获胜集的成员问题。虽然这种复杂性是相同的简单类的回合制游戏，其中在每个状态下，只有一个玩家有一个选择的动作，我们的算法，这是通过表征的胜利集作为μ演算公式，是相当多的参与。
We study a type of generalized recursive game introduced by Castronova, Chen, and Zumbrun featuring increasing stakes, with an emphasis on continuous guts poker and $1$ v. $n$ coalitions. Our main results are to develop practical numerical algorithms with rigorous underlying theory for the approximation of optimal mutiplayer strategies, and to use these to obtain a number of interesting observations about guts. Outcomes are a striking 2-strategy optimum for $n$-player coalitions, with asymptotic advantage approximately $16\%$; convergence of Fictitious Play to symmetric Nash equilibrium; and a…
We study two-player reachability games on finite graphs. At each state the interaction between the players is concurrent and there is a stochastic Nature. Players also play stochastically. The literature tells us that 1) Player B, who wants to avoid the target state, has a positional strategy that maximizes the probability to win (uniformly from every state) and 2) from every state, for every ε > 0, Player A has a strategy that maximizes up to ε the probability to win. Our work is two-fold. First, we present a double-fixed-point procedure that says from which state Player A has a strategy that…
We present novel techniques for neuro-symbolic concurrent stochastic games, a recently proposed modelling formalism to represent a set of probabilistic agents operating in a continuous-space environment using a combination of neural network based perception mechanisms and traditional symbolic methods. To date, only zero-sum variants of the model were studied, which is too restrictive when agents have distinct objectives. We formalise notions of equilibria for these models and present algorithms to synthesise them. Focusing on the finite-horizon setting, and (global) social welfare subgame-perf…
Representation Theorems for Actual Powers over Two-Agent General Concurrent Game Frames
Institute for Logic, Language and Computation, University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；Beijing Normal University（北京师范大学）；University of Bergen（卑尔根大学）；Shanxi University（山西大学）
National University of Singapore（新加坡国立大学）；Massachusetts Institute of Technology（麻省理工学院）
This paper presents a recursive reasoning formalism of Bayesian optimization (BO) to model the reasoning process in the interactions between boundedly rational, self-interested agents with unknown, complex, and costly-to-evaluate payoff functions in repeated games, which we call Recursive Reasoning-Based BO (R2-B2). Our R2-B2 algorithm is general in that it does not constrain the relationship among the payoff functions of different agents and can thus be applied to various types of games such as constant-sum, general-sum, and common-payoff games. We prove that by reasoning at level 2 or more a…
Despite the success of generative adversarial networks (GANs) in generating visually appealing images, they are notoriously challenging to train. In order to stabilize the learning dynamics in minimax games, we propose a novel recursive reasoning algorithm: Level $k$ Gradient Play (Lv.$k$ GP) algorithm. In contrast to many existing algorithms, our algorithm does not require sophisticated heuristics or curvature information. We show that as $k$ increases, Lv.$k$ GP converges asymptotically towards an accurate estimation of players' future strategy. Moreover, we justify that Lv.$\infty$ GP natur…
Interval Scheduling Games with Color-Based Concurrent Jobs
Viavi Solutions（维亚维解决方案）；School of Business and Economics, Maastricht University（马斯特里赫特大学商学院与经济系）；School of Computer Science, Reichman University（瑞克曼大学计算机科学学院）
We introduce and study a natural extension of the Alternating time temporal logic ATL, called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features just one, but quite expressive, coalitional strategic operator, viz. the coalitional goal assignment operator, which is based on a mapping assigning to each set of players in the game its coalitional goal, formalised by a path formula of the language of TLCGA, i.e. a formula prefixed with a temporal operator X,U, or G, representing a temporalised objective for the respective coalition, describing the property of the plays on which tha…
