automated verification engineers

Abstract: Mean-Payoff Games (MPGs) form an interesting family of deterministic, infinite-duration, zero-sum, turn-based games played by two players on a finite weighted directed graph. The goal of the players is to minimize, respectively maximize, the $\textit{limiting average}$ of the costs of the edges on an infinite path constructed by the two players. The complexity of solving MPGs is a long-standing open question. The decision problem associated with these games is known to be in $\text{NP}\cap \text{co-NP}$, and even $\text{UP}\cap \text{co-UP}$, yet the problem is not known to be in $\text{P}$. This is one of the simplest combinatorial problems with such a status. A full solution of an MPG gives the $\textit{value}$ of each vertex of the game, along with a pair of $\textit{optimal strategies}$ for the two players. (Each player has a succinct $\textit{positional}$ optimal strategy.) The problem of finding optimal strategies for the players given the values of all vertices is known as the $\textit{strategy recovery}$ problem. We describe a simple reduction from the problem of solving MPGs to the strategy recovery problem for MPGs. This shows that the strategy recovery problem for MPGs is essentially as hard as solving MPGs from scratch, i.e., without knowing the values. The reduction uses simple $\textit{game transformations}$ and simple $\textit{self-reducibility}$ and $\textit{peeling}$ arguments. This answers a question of Andersson and Miltersen. Mamino obtained a similar result for $\textit{stochastic}$ games with a limiting average objective, but his technique does not extend to deterministic games such as MPGs. We go one step further and show that finding an optimal strategy for one of the players of an MPG remains hard even if an optimal strategy of the second player, and hence all the values, are known.

Abstract: 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 $\mathsf{NP}$-complete. For safety objectives, we show that limit-sure winning coincides with almost-sure winning, which is known to lie in $\mathsf{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 $\mathsf{P}^{\mathsf{NP}}$-complete.

Abstract: This paper investigates the constrained existence problem for subgame perfect equilibria (SPEs) in multiplayer graph games. In the proposed framework, each player has a preference relation over the set of plays, assumed to be $ω$-recognizable. Equivalently, he has a preference relation over a finite set of payoffs, and the set of plays with the same payoff is $ω$-regular, for each payoff. This generic framework avoids the need to focus on specific payoff functions. We show that the constrained SPE existence problem is EXPTIME-complete, as well as for Nash equilibria (NEs).