James C. A. Main

Highlights Conference 2025 Conference Abstract

Taming Infinity one Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

• James C. A. Main

Highlights Conference 2024 Conference Abstract

A Single Dice Roll to Satisfy All Goals: Randomisation Requirements for Strategies in Multi-Objective Markov Decision Processes

• James C. A. Main

We study strategy requirements for multi-objective queries in Markov decision processes (MDPs). A multi-objective query is defined by finitely many real payoff functions over plays and a threshold for each function. A query asks whether there is a strategy such that, for all payoffs, the expectancy of the payoff is strictly greater than its respective threshold when playing according to the strategy. Pure strategies, i. e. , strategies that do not resort to randomisation, do not suffice for such queries in general. In this work, we analyse the randomisation requirements for multi-objective queries. We identify a strict subclass of randomised strategies that suffices to satisfy multi-objective queries. Given a query with $d$ payoffs, we show that it can be satisfied by mixing at most $d$ pure strategies, i. e. , by randomly selecting one of $d$ pure strategies and committing to it for the whole play. We also provide sufficient conditions that extend the previous property to queries with non-strict inequalities. This talk is based on ongoing joint work with Mickael Randour. James C. A. Main is a Fonds de la Recherche Scientifique – FNRS Research Fellow and a member of the TRAIL institute. Mickael Randour is a Fonds de la Recherche Scientifique – FNRS Research Associate and a member of the TRAIL institute. This work has been supported by the Fonds de la Recherche Scientifique – FNRS under Grant n° T. 0188. 23 (PDR ControlleRS).

LAMAS&SR Workshop 2023 Workshop Paper

Different Strokes in Randomised Strategies: Revisiting Kuhn's Theorem under Finite-memory Assumptions

• James C. A. Main
• Mickael Randour

Highlights Conference 2022 Conference Abstract

Different Strokes in Randomised Strategies: Revisiting Kuhn's Theorem Under Finite-Memory Assumptions

• James C. A. Main

Two-player (antagonistic) games on (possibly stochastic) graphs are a prevalent model in theoretical computer science, notably as a framework for reactive synthesis. Optimal strategies may require randomisation when dealing with inherently probabilistic goals, balancing multiple objectives, or in contexts of partial information. There is no unique way to define randomised strategies. For instance, one can use so-called mixed strategies or behavioural ones. In the most general settings, these two classes do not share the same expressiveness. A seminal result in game theory - Kuhn's theorem - asserts their equivalence in games of perfect recall. This result crucially relies on the possibility for strategies to use infinite memory, i. e. , unlimited knowledge of all the past of a play. However, computer systems are finite in practice. Hence it is pertinent to restrict our attention to finite-memory strategies, defined as automata with outputs. Randomisation can be implemented in these in different ways: the initialisation, outputs or transitions can be randomised or deterministic respectively. Depending on which aspects are randomised, the expressiveness of the corresponding class of finite-memory strategies differs. In this work, we study two-player turn-based stochastic games and provide a complete taxonomy of the classes of finite-memory strategies obtained by varying which of the three aforementioned components are randomised. Our taxonomy holds both in settings of perfect and imperfect information. This talk is based on joint work with Mickael Randour.

Highlights Conference 2021 Conference Abstract

Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

• James C. A. Main

The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs. It has since proved useful in a variety of settings, including parity objectives in games and both mean-payoff and parity objectives in Markov decision processes. We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking that all time-divergent paths of a timed automaton satisfy such a window parity objective can be done in polynomial space, and that the corresponding timed games can be solved in exponential time. This matches the complexity class of timed parity games, while adding the ability to reason about time bounds. We also consider multi-dimensional objectives and show that the complexity class does not increase. To the best of our knowledge, this is the first study of the window mechanism in a real-time setting. This is joint work with Mickael Randour and Jeremy Sproston.