We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as "PLTL" by Alur et al. and (in a different version called "PROMPT-LTL") by Kupferman et al..
We present an algorithm to determine optimal variable valuations that allow a player to win a game. Furthermore, we show how to determine whether a player wins a game with respect to some, infinitely many, or all valuations. All our algorithms run in doubly-exponential time; so, adding bounded temporal operators does not increase the complexity compared to solving plain LTL games.
The classical LTL synthesis problem is purely qualitative: the given LTL specification is realized or not by a reactive system. LTL is not expressive enough to formalize the correctness of reactive systems with respect to some quantitative aspects. This paper extends the qualitative LTL synthesis setting to a quantitative setting. The alphabet of actions is extended with a weight function ranging over the rational numbers. The value of an infinite word is the mean-payoff of the weights of its letters. The synthesis problem then amounts to automatically construct (if possible) a reactive system…
We consider the synthesis of distributed implementations for specifications in Prompt Linear Temporal Logic (PROMPT-LTL), which extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous systems, we show that, despite being more powerful, the distributed realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to consider an assume-guarantee synthesis problem, as we have to expre…
Electric boolean games are compact representations of games where the players have qualitative objectives described by LTL formulae and have limited resources. We study the complexity of several decision problems related to the analysis of rationality in electric boolean games with LTL objectives. In particular, we report that the problem of deciding whether a profile is a Nash equilibrium in an iterated electric boolean game is no harder than in iterated boolean games without resource bounds. We show that it is a PSPACE-complete problem. As a corollary, we obtain that both rational eliminatio…
Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. Recently, such games with quantitative winning conditions in weak MSO with the unbounding quantifier were studied, but their properties turned out to be unsatisfactory. In particular, unbounded lookahead is in general necessary. Here, we study delay games with winning conditions given by Prompt-LTL, Linear Temporal Logic equipped with a parameterized eventually operator whose scope is bounded. Our main result shows that solving Prompt-LTL delay games is c…
We consider the synthesis of distributed implementations for specifications in parameterized temporal logics such as PROMPT-LTL, which extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous distributed systems we show that, despite being more powerful, the realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to express scheduling assumptions and therefore consider an assu…
Monash University（莫纳什大学）；University of Oxford（牛津大学）；University of Kaiserslautern（凯泽斯劳滕大学）
Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational ver…
Monash University（莫纳什大学）；University of Kaiserslautern（凯泽斯劳滕大学）；Sapienza University of Rome（罗马大学）；University of Oxford（牛津大学）
In the context of multi-agent systems, the rational verification problem is concerned with checking which temporal logic properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives. Typically, those objectives are expressed as temporal logic formulae which the relevant agent desires to see satisfied. Unfortunately, rational verification is computationally complex, and requires specialised techniques in order to obtain practically useable implementations. In this paper, we present such a technique. This tech…
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…
Parity games have been broadly studied in recent years for their applications to controller synthesis and verification. In practice, partial solvers for parity games that execute in polynomial time, while incomplete, can solve most games in publicly available benchmark suites. In this paper, we combine those partial solvers with the classical recursive algorithm for parity games due to Zielonka. We also extend partial solvers to generalized parity games that are games with conjunction of parity objectives. We have implemented those algorithms and evaluated them on a large set of benchmarks pro…
Parity games are simple infinite games played on finite graphs with a winning condition that is expressive enough to capture nested least and greatest fixpoints. Through their tight relationship to the modal mu-calculus, they are used in practice for the model-checking and synthesis problems of the mu-calculus and related temporal logics like LTL and CTL. Solving parity games is a compelling complexity theoretic problem, as the problem lies in the intersection of UP and co-UP and is believed to admit a polynomial-time solution, motivating researchers to either find such a solution or to find s…
This paper studies the synthesis of control policies for an agent that has to satisfy a temporal logic specification in a partially observable environment, in the presence of an adversary. The interaction of the agent (defender) with the adversary is modeled as a partially observable stochastic game. The goal is to generate a defender policy to maximize satisfaction of a given temporal logic specification under any adversary policy. The search for policies is limited to the space of finite state controllers, which leads to a tractable approach to determine policies. We relate the satisfaction …
We propose a parametric family of measures of fairness in allocations of TU-cooperative games. Their definition is based on generalized Renyi Entropy, is related to the Cowell-Kuga generalized entropy indices in welfare economics, and aims to parallel the spirit of the notion of price of anarchy in the case of convex TU-cooperative games. Since computing these indices is NP-complete in general, we first upper bound the performance of a "reverse greedy" algorithm for approximately computing worst-case fairness. The result provides a general additive error guarantee in terms of two (problem depe…
Information Processing and Telecommunications Center（信息处理与电信中心）；Universidad Politécnica de Madrid（马德里理工大学）
Multiagent systems where agents interact among themselves and with a stochastic environment can be formalized as stochastic games. We study a subclass named Markov potential games (MPGs) that appear often in economic and engineering applications when the agents share a common resource. We consider MPGs with continuous state-action variables, coupled constraints and nonconvex rewards. Previous analysis followed a variational approach that is only valid for very simple cases (convex rewards, invertible dynamics, and no coupled constraints); or considered deterministic dynamics and provided open-…
Measuring contributions is a classical problem in cooperative game theory where the Shapley value is the most well-known solution concept. In this paper, we establish the convergence property of the Shapley value in parametric Bayesian learning games where players perform a Bayesian inference using their combined data, and the posterior-prior KL divergence is used as the characteristic function. We show that for any two players, under some regularity conditions, their difference in Shapley value converges in probability to the difference in Shapley value of a limiting game whose characteristic…
We show that computing an equilibrium in atomic splittable congestion games with player-specific affine cost functions $l_{e,i}(x) = a_{e,i} x + b_{e,i}$ is $\mathsf{PPAD}$-complete. To prove that the problem is contained in $\mathsf{PPAD}$, we develop a homotopy method that traces an equilibrium for varying flow demands of the players. A key technique for this method is to describe the evolution of the equilibrium locally by a novel block Laplacian matrix. Using the properties of this matrix give rise to a path following formulation for computing an equilibrium where states correspond to supp…
CNN-based steganalysis has recently achieved very good performance in detecting content-adaptive steganography. At the same time, recent works have shown that, by adopting an approach similar to that used to build adversarial examples, a steganographer can adopt an adversarial embedding strategy to effectively counter a target CNN steganalyzer. In turn, the good performance of the steganalyzer can be restored by retraining the CNN with adversarial stego images. A problem with this model is that, arguably, at training time the steganalizer is not aware of the exact parameters used by the stegan…
This paper studies the satisfaction of a class of temporal properties for cyber-physical systems (CPSs) over a finite-time horizon in the presence of an adversary, in an environment described by discrete-time dynamics. The temporal logic specification is given in safe-LTL_F, a fragment of linear temporal logic over traces of finite length. The interaction of the CPS with the adversary is modeled as a two-player zero-sum discrete-time dynamic stochastic game with the CPS as defender. We formulate a dynamic programming based approach to determine a stationary defender policy that maximized the p…
The yolk is an important concept in spatial voting games as it generalises the equilibrium and provides bounds on the uncovered set. We present near-linear time algorithms for computing the yolk in the spatial voting model in the plane. To the best of our knowledge our algorithm is the first algorithm that does not require precomputing the median lines and hence able to break the existing $O(n^{4/3})$ bound which equals the known upper bound on the number of median lines. We avoid this requirement by using Megiddo's parametric search, which is a powerful framework that could lead to faster alg…
We introduce the Colonel Blotto game with favoritism, an extension of the famous Colonel Blotto game where the winner-determination rule is generalized to include pre-allocations and asymmetry of the players' resources effectiveness on each battlefield. Such favoritism is found in many classical applications of the Colonel Blotto game. We focus on the Nash equilibrium. First, we consider the closely related model of all-pay auctions with favoritism and completely characterize its equilibrium. Based on this result, we prove the existence of a set of optimal univariate distributions -- which ser…
University of Michigan（密歇根大学）；Yahoo! Research（雅虎研究院）
We present a functional framework for automated mechanism design based on a two-stage game model of strategic interaction between the designer and the mechanism participants, and apply it to several classes of two-player infinite games of incomplete information. At the core of our framework is a black-box optimization algorithm which guides the selection process of candidate mechanisms. Our approach yields optimal or nearly optimal mechanisms in several application domains using various objective functions. By comparing our results with known optimal mechanisms, and in some cases improving on …
Learning problems commonly exhibit an interesting feedback mechanism wherein the population data reacts to competing decision makers' actions. This paper formulates a new game theoretic framework for this phenomenon, called "multi-player performative prediction". We focus on two distinct solution concepts, namely (i) performatively stable equilibria and (ii) Nash equilibria of the game. The latter equilibria are arguably more informative, but can be found efficiently only when the game is monotone. We show that under mild assumptions, the performatively stable equilibria can be found efficient…
One practical requirement in solving dynamic games is to ensure that the players play well from any decision point onward. To satisfy this requirement, existing efforts focus on equilibrium refinement, but the scalability and applicability of existing techniques are limited. In this paper, we propose Temporal-Induced Self-Play (TISP), a novel reinforcement learning-based framework to find strategies with decent performances from any decision point onward. TISP uses belief-space representation, backward induction, policy learning, and non-parametric approximation. Building upon TISP, we design …
This paper studies two important signal processing aspects of equilibrium behavior in non-cooperative games arising in social networks, namely, reinforcement learning and detection of equilibrium play. The first part of the paper presents a reinforcement learning (adaptive filtering) algorithm that facilitates learning an equilibrium by resorting to diffusion cooperation strategies in a social network. Agents form homophilic social groups, within which they exchange past experiences over an undirected graph. It is shown that, if all agents follow the proposed algorithm, their global behavior i…
