Stochastic Games

This talk considers parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters rather than precise values. Parametric MDPs have been studied in the context of verifying robust randomizing algorithms and to study decision making in partially observable environments. We first review results regarding the complexity of finding values for these parameters such that the induced MDP satisfies some maximal or minimal reachability probability constraints and then discuss three intriguing open problems.

We consider controller synthesis via game theory. Controllers are derived from strategies of players in games whenever suitable strategies can be computed. Traditionally, strategies are represented by Mealy machines, i.e., automata with outputs along their transitions. This model has been extensively studied and is particularly well-suited for automata-based game solving techniques.

The Mealy machine standard for strategy representation, in spite of its established usefulness, may not be the most relevant in certain contexts. For instance, some strategies require exponential-size Mealy machines despite admitting a small program-like representation based on counters that is thus better suited for controller implementation. In a certain sense, Mealy machines can somewhat obfuscate the structure of strategies and their complexity (e.g., with respect to implementation). These concerns have recently led to a surge of alternative models to represent strategies such as decision trees, neural networks and programs.

We motivate a multifaceted vision of strategy complexity. For instance, strategy representations provide natural measures of complexity (e.g., their size). These measures are not necessarily directly comparable to one another. We are also interested in the applicability and relevance of strategy representations, and their relationships. In addition to model-based notions of complexity, measures that are independent of the chosen representation are also relevant, such as the inclusion of randomness in decision making.

This talk is based on joint work with Mickael Randour.

Population games are played on a non-deterministic finite automaton. Some number of tokens are placed on an initial state. At each round, one player picks a letter x, and the other answers by moving each token along an x-transition. The first player wins if she can make all tokens reach a final state, for any initial number of tokens.

In this talk we will survey the results obtained so far on this model, with a focus on the model where the second player picks transitions at random. We will sketch the latest algorithm to compute a winning strategy for the first player in that case, obtained with Hugo Gimbert and Patrick Totzke. We will also present and motivate several open problems concerning this model.

Abstract Reinforcement Learning (RL) has long outgrown the traditional representations that guaranteed policy convergence but severely limited its application to complex domains. Modern Deep RL enables far richer and complex behaviour, yet at the cost of transparency and explainability, as well as convergence guarantees. The same has been observed in Multi-agent RL settings, where in the past it has been shown that independent learning agents, i.e. not having access to the states nor actions of the other agents, could converge to interesting solution concepts, especially. When equipped with an additional protocol, fair solutions could even be obtained. Today the state-of-the art is Centralised learning, decentralized execution, and while it can handle larger state spaces, it gives in on distributivity. After discussing some convergence proofs which hold for tabular settings, some recent developments for policy distillation were discussed and for providing formal guarantees (see also talk by Florent Delgrange).

This tutorial presents an overview of PRISM-games, which is a tool for probabilistic model checking of stochastic games. This technique provides formal modelling and analysis of multi-agent systems with probabilistic behaviour. I will describe ways to model such systems using turn-based or concurrent stochastic games, and to formally specify desired properties of the agents’ strategies using probabilistic temporal logic. I will discuss the techniques that PRISM-games implements for model checking these logics, covering both zero-sum and equilibria-based properties, and present some illustrative case studies.

In order to provide guarantees on the behavior of a system, probabilism and non-determinism pose different challenges. Non-determinism typically necessitates a worst-case analysis, while probabilism allows for more nuanced assurances. This raises the question whether systems in which uncertainty is mainly subject to probabilism are more desirable. This talk presents an idea on how to measure the influence of non-determinism and probabilism, respectively, on the uncertainty of some quantitative aspect, e.g., the runtime, of a system. The talk aims to open a discussion on whether “more probabilistic” systems are indeed desirable and in which situations using such an objective (potentially in conjunction with further objectives) might be useful.

What could be greater fun than toying around with formal structures? One particularly beautiful structure to play with are automata over infinite words, and there is really no need to give any supporting argument for the pleasure part in the title. But how about profit? When using $\omega$-regular languages as target languages for practical applications like Markov chain model checking, MDP model checking and reinforcement learning, reactive synthesis, or as a target for an infinite word played out in a two player game, the classic approach has been to first produce a deterministic automaton D that recognises that language. This deterministic automaton is quite useful: we can essentially play on the syntactic product of the structure and use the acceptance mechanism it inherits from the automaton as target. This is beautiful and moves all the heavy lifting to the required automata transformations. But when we want even more profit in addition to the pleasure, the question arises whether deterministic automata are the best we can do. They are clearly good enough: determinism is as restrictive as it gets, and easily guarantees that one can just work on the product. But what we really want is the reverse: we want an automaton, so that we can work on the product, and determinism is just maximally restrictive, and therefore good enough for everything. At Dagstuhl, all will know that we can lift quite a few restrictions and instead turn to the gains we can make when we focus on the real needs of being able to work on the product. For Markov chains, this could be unambiguous automata, for MDPs this could be good-for-MDP automata, and for synthesis and games, this could be good-for-games automata. We will shed a light to a few nooks and corners of the vast room available open questions and answers, with a bias towards MDPs analysis in general and reinforcement learning in particular.

Markov Decision Processes (MDPs) are a fundamental mathematical model for reasoning about uncertainty and have a foundational role in the theory of reinforcement learning. Over the past decade, there have been substantial advances in the design and analysis of algorithms for provably computing approximately optimal policies for MDPs in a variety of settings. In this talk, I will survey these advances touching upon optimization tools of potential broader utility. Additionally, I will discuss recent joint work with Ishani Karmarkar, Jiayi Wang, and Yujia Jin on solving MDPS (arXiv:2405.12952).

We consider partially observable Markov decision processes (POMDPs) with parity objectives. We study the qualitative problem of deciding whether there exists an almost surely winning strategy. Such a problem is undecidable in general, already for coBüchi objectives.

We introduce two decidable properties requiring that, almost surely and infinitely often, the exact state can be deduced (which is called a revelation). Assuming the first property, we show that coBüchi is decidable, while parity with three priorities is still undecidable. Assuming the second property, we show that parity is decidable. Technically, the decidable cases all reduce to the analysis of the finite belief support MDP. We also consider partially observable zero-sum games and show that coBüchi is still undecidable under the revealing properties.

We study the complexity of computing stationary Nash equilibrium (NE) in n-player infinite-horizon general-sum stochastic games. We focus on the problem of computing NE in such stochastic games when each player is restricted to choosing a stationary policy and rewards are discounted. First, we prove that computing such NE is in PPAD (in addition to clearly being PPAD-hard). Second, we consider turn-based specializations of such games where at each state there is at most a single player that can take actions and show that these (seemingly simpler) games remain PPAD-hard. Third, we show that under further structural assumptions on the rewards computing NE in such turn-based games is possible in polynomial time. Towards achieving these results we establish structural facts about stochastic games of broader utility, including monotonicity of utilities under single-state single-action changes and reductions to settings where each player controls a single state.

Evaluating, validating and comparing algorithms for solving stochastic games requires a set of benchmarks. This set should be “realistic”, easy-to-use, and structurally diverse. I provide an overview of the state-of-the-art benchmark sets, pointing out their shortcomings and sketching how we can improve them.

My insights on this topic are based on my continued work on algorithms for stochastic games, in particular [1, 2, 3, 4, 5], and the discussions we had about the MDP benchmark set at the previous Dagstuhl Seminar 24134.

This blackboard session studied the connection between decision making in Partially Observable Markov Decision Processes (POMDPs) and parametric Markov chains (pMCs), which were discussed at length in an earlier talk. After reviewing results from the main reference given below a discussion revolved mostly about the possibilities to extend these results in different directions, e.g., by partitioning the set of parameters in controllable and uncontrollable parameters, by connecting Partially Observable Stochastic Games (or Concurrent Stochastic Games) with pMDPs. This lead to a discussion of the important features which make parameter synthesis in MDPs hard.

This break-out session was concerned with two questions. Firstly, how to measure the difficulty and structure of benchmarks so that we can pinpoint what makes real ones easy (or hard) and what to focus one in order to design practical algorithms [1]. Second, how to describe the fine structure of strategies and utilize it in order to represent them (i) explainably and (ii) so that they are easier to compute [2].

In 2017, Bertrand, Dewaskar, Genest and Gimbert introduced a population games, inspired by questions from biology on the control of yeast populations [1]. A population game is described by an NFA with one initial and one final state. Some number of tokens are placed on an initial state of an NFA. Two players then play alternately: Controller chooses a letter $a$, then Environment moves each token along an $a$-labelled transitions chosen at random. Controller wins if all tokens end up on the same final state eventually. The question is then: does Controller have a winning strategy against any number of tokens?

A randomized version of those games was later presented by Colcombet, Fijalkow and Ohlmann [2]: this is the model studied in this working group. In this framework, the Environment picks the next transition of each token uniformly at random. The new question is: Can Controller win with probability 1 against any number of tokens? That first paper established decidablity of this problem. However, the expected time needed by Controller to win may in general be exponential in the number of tokens.

This working group was dedicated to the search for decidable characterizations of games where Controller can win in polynomial and polylogarithmic time. We made progress in several directions, Most notably, we built a clear plan to characterize the polylogarithmic case, leaving reducing the initial problem to a couple of lemmas that we believe we can prove with a little more work.