Search Results

Documents authored by Main, James C. A.

Document
DOI: 10.4230/LIPIcs.LICS.2026.68
Mixing Any Cocktail with Limited Ingredients: On the Structure of Payoff Sets in Multi-Objective POMDPs and Its Impact on Randomised Strategies

Authors: James C. A. Main and Mickael Randour

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
We consider multi-dimensional payoff functions in partially observable Markov decision processes. We study the structure of the set of expected payoff vectors of all strategies (policies) and study what kind are needed to achieve a given expected payoff vector. In general, pure strategies (i.e., not resorting to randomisation) do not suffice for this problem. We prove that for any payoff function for which the expectation is well-defined under all strategies, it is sufficient to mix (i.e., randomly select a pure strategy at the start of a play and committing to it for the rest of the play) finitely many pure strategies to approximate any expected payoff vector up to any precision. Furthermore, for any payoff function for which the expected payoff is finite under all strategies, any expected payoff vector can be obtained exactly by mixing finitely many strategies. These results are already novel in the context of (perfect information) Markov decision processes.
Cite as

James C. A. Main and Mickael Randour. Mixing Any Cocktail with Limited Ingredients: On the Structure of Payoff Sets in Multi-Objective POMDPs and Its Impact on Randomised Strategies. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 68:1-68:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{main_et_al:LIPIcs.LICS.2026.68,
  author =	{Main, James C. A. and Randour, Mickael},
  title =	{{Mixing Any Cocktail with Limited Ingredients: On the Structure of Payoff Sets in Multi-Objective POMDPs and Its Impact on Randomised Strategies}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{68:1--68:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.68},
  URN =		{urn:nbn:de:0030-drops-268559},
  doi =		{10.4230/LIPIcs.LICS.2026.68},
  annote =	{Keywords: partially observable Markov decision process, multiple objectives, randomised strategies, mixed strategies, strategy complexity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.138
Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

Authors: Michal Ajdarów, James C. A. Main, Petr Novotný, and Mickael Randour

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Markov decision processes (MDPs) are a canonical model to reason about decision making within a stochastic environment. We study a fundamental class of infinite MDPs: one-counter MDPs (OC-MDPs). They extend finite MDPs via an associated counter taking natural values, thus inducing an infinite MDP over the set of configurations (current state and counter value). We consider two characteristic objectives: reaching a target state (state-reachability), and reaching a target state with counter value zero (selective termination). The synthesis problem for the latter is not known to be decidable and connected to major open problems in number theory. Furthermore, even seemingly simple strategies (e.g., memoryless ones) in OC-MDPs might be impossible to build in practice (due to the underlying infinite configuration space): we need finite, and preferably small, representations. To overcome these obstacles, we introduce two natural classes of concisely represented strategies based on a (possibly infinite) partition of counter values in intervals. For both classes, and both objectives, we study the verification problem (does a given strategy ensure a high enough probability for the objective?), and two synthesis problems (does there exist such a strategy?): one where the interval partition is fixed as input, and one where it is only parameterized. We develop a generic approach based on a compression of the induced infinite MDP that yields decidability in all cases, with all complexities within PSPACE.
Cite as

Michal Ajdarów, James C. A. Main, Petr Novotný, and Mickael Randour. Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 138:1-138:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ajdarow_et_al:LIPIcs.ICALP.2025.138,
  author =	{Ajdar\'{o}w, Michal and Main, James C. A. and Novotn\'{y}, Petr and Randour, Mickael},
  title =	{{Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{138:1--138:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.138},
  URN =		{urn:nbn:de:0030-drops-235157},
  doi =		{10.4230/LIPIcs.ICALP.2025.138},
  annote =	{Keywords: one-counter Markov decision processes, randomised strategies, termination, reachability}
}
Document
DOI: 10.4230/LIPIcs.STACS.2024.50
Arena-Independent Memory Bounds for Nash Equilibria in Reachability Games

Authors: James C. A. Main

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study the memory requirements of Nash equilibria in turn-based multiplayer games on possibly infinite graphs with reachability, shortest path and Büchi objectives. We present constructions for finite-memory Nash equilibria in these games that apply to arbitrary game graphs, bypassing the finite-arena requirement that is central in existing approaches. We show that, for these three types of games, from any Nash equilibrium, we can derive another Nash equilibrium where all strategies are finite-memory such that the same players accomplish their objective, without increasing their cost for shortest path games. Furthermore, we provide memory bounds that are independent of the size of the game graph for reachability and shortest path games. These bounds depend only on the number of players. To the best of our knowledge, we provide the first results pertaining to finite-memory constrained Nash equilibria in infinite arenas and the first arena-independent memory bounds for Nash equilibria.
Cite as

James C. A. Main. Arena-Independent Memory Bounds for Nash Equilibria in Reachability Games. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 50:1-50:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{main:LIPIcs.STACS.2024.50,
  author =	{Main, James C. A.},
  title =	{{Arena-Independent Memory Bounds for Nash Equilibria in Reachability Games}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{50:1--50:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.50},
  URN =		{urn:nbn:de:0030-drops-197603},
  doi =		{10.4230/LIPIcs.STACS.2024.50},
  annote =	{Keywords: multiplayer games on graphs, Nash equilibrium, finite-memory strategies}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2023.1
Reachability Games and Friends: A Journey Through the Lens of Memory and Complexity (Invited Talk)

Authors: Thomas Brihaye, Aline Goeminne, James C. A. Main, and Mickael Randour

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
Reachability objectives are arguably the most basic ones in the theory of games on graphs (and beyond). But far from being bland, they constitute the cornerstone of this field. Reachability is everywhere, as are the tools we use to reason about it. In this invited contribution, we take the reader on a journey through a zoo of models that have reachability objectives at their core. Our goal is to illustrate how model complexity impacts the complexity of strategies needed to play optimally in the corresponding games and computational complexity.
Cite as

Thomas Brihaye, Aline Goeminne, James C. A. Main, and Mickael Randour. Reachability Games and Friends: A Journey Through the Lens of Memory and Complexity (Invited Talk). In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 1:1-1:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.FSTTCS.2023.1,
  author =	{Brihaye, Thomas and Goeminne, Aline and Main, James C. A. and Randour, Mickael},
  title =	{{Reachability Games and Friends: A Journey Through the Lens of Memory and Complexity}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{1:1--1:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.1},
  URN =		{urn:nbn:de:0030-drops-193747},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.1},
  annote =	{Keywords: Games on graphs, reachability, finite-memory strategies, complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.22
Different Strokes in Randomised Strategies: Revisiting Kuhn’s Theorem Under Finite-Memory Assumptions

Authors: James C. A. Main and Mickael Randour

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
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 past observations. 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, and in games with more than two players.
Cite as

James C. A. Main and Mickael Randour. Different Strokes in Randomised Strategies: Revisiting Kuhn’s Theorem Under Finite-Memory Assumptions. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{main_et_al:LIPIcs.CONCUR.2022.22,
  author =	{Main, James C. A. and Randour, Mickael},
  title =	{{Different Strokes in Randomised Strategies: Revisiting Kuhn’s Theorem Under Finite-Memory Assumptions}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.22},
  URN =		{urn:nbn:de:0030-drops-170854},
  doi =		{10.4230/LIPIcs.CONCUR.2022.22},
  annote =	{Keywords: two-player games on graphs, stochastic games, Markov decision processes, finite-memory strategies, randomised strategies}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.25
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

Authors: James C. A. Main, Mickael Randour, and Jeremy Sproston

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
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 [Krishnendu Chatterjee et al., 2015]. It has since proved useful in a variety of settings, including parity objectives in games [Véronique Bruyère et al., 2016] and both mean-payoff and parity objectives in Markov decision processes [Thomas Brihaye et al., 2020]. 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.
Cite as

James C. A. Main, Mickael Randour, and Jeremy Sproston. Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{main_et_al:LIPIcs.CONCUR.2021.25,
  author =	{Main, James C. A. and Randour, Mickael and Sproston, Jeremy},
  title =	{{Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{25:1--25:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.25},
  URN =		{urn:nbn:de:0030-drops-144021},
  doi =		{10.4230/LIPIcs.CONCUR.2021.25},
  annote =	{Keywords: Window objectives, timed automata, timed games, parity games}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact