8 Search Results for "Oualhadj, Youssouf"


Document
A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs

Authors: Marnix Suilen, Marck van der Vegt, and Sebastian Junges

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)


Abstract
Markov Decision Processes (MDPs) model systems with uncertain transition dynamics. Multiple-environment MDPs (MEMDPs) extend MDPs. They intuitively reflect finite sets of MDPs that share the same state and action spaces but differ in the transition dynamics. The key objective in MEMDPs is to find a single strategy that satisfies a given objective in every associated MDP. The main result of this paper is PSPACE-completeness for almost-sure Rabin objectives in MEMDPs. This result clarifies the complexity landscape for MEMDPs and contrasts with results for the more general class of partially observable MDPs (POMDPs), where almost-sure reachability is already EXP-complete, and almost-sure Rabin objectives are undecidable.

Cite as

Marnix Suilen, Marck van der Vegt, and Sebastian Junges. A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{suilen_et_al:LIPIcs.CONCUR.2024.40,
  author =	{Suilen, Marnix and van der Vegt, Marck and Junges, Sebastian},
  title =	{{A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{40:1--40:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.40},
  URN =		{urn:nbn:de:0030-drops-208120},
  doi =		{10.4230/LIPIcs.CONCUR.2024.40},
  annote =	{Keywords: Markov Decision Processes, partial observability, linear-time Objectives}
}
Document
Synthesis of Robust Optimal Real-Time Systems

Authors: Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)


Abstract
Weighted Timed Games (WTGs for short) are widely used to describe real-time controller synthesis problems, but they rely on an unrealistic perfect measure of time elapse. In order to produce strategies tolerant to timing imprecisions, we consider a notion of robustness, expressed as a parametric semantics, first introduced for timed automata. WTGs are two-player zero-sum games played in a weighted timed automaton in which one of the players, that we call Min, wants to reach a target location while minimising the cumulated weight. The opponent player, in addition to controlling some of the locations, can perturb delays chosen by Min. The robust value problem asks, given some threshold, whether there exists a positive perturbation and a strategy for Min ensuring to reach the target, with an accumulated weight below the threshold, whatever the opponent does. We provide in this article the first decidability result for this robust value problem. More precisely, we show that we can compute the robust value function, in a parametric way, for the class of divergent WTGs (this class has been introduced previously to obtain decidability of the (classical) value problem in WTGs without bounding the number of clocks). To this end, we show that the robust value is the fixpoint of some operators, as is classically done for value iteration algorithms. We then combine in a very careful way two representations: piecewise affine functions introduced in [Alur et al., 2004] to analyse WTGs, and shrunk Difference Bound Matrices (shrunk DBMs for short) considered in [Sankur et al., 2011] to analyse robustness in timed automata. The crux of our result consists in showing that using this representation, the operator of value iteration can be computed for infinitesimally small perturbations. Last, we also study qualitative decision problems and close an open problem on robust reachability, showing it is EXPTIME-complete for general WTGs.

Cite as

Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Synthesis of Robust Optimal Real-Time Systems. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 74:1-74:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{monmege_et_al:LIPIcs.MFCS.2024.74,
  author =	{Monmege, Benjamin and Parreaux, Julie and Reynier, Pierre-Alain},
  title =	{{Synthesis of Robust Optimal Real-Time Systems}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{74:1--74:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.74},
  URN =		{urn:nbn:de:0030-drops-206304},
  doi =		{10.4230/LIPIcs.MFCS.2024.74},
  annote =	{Keywords: Weighted timed games, Algorithmic game theory, Robustness}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Finite-Memory Strategies for Almost-Sure Energy-MeanPayoff Objectives in MDPs

Authors: Mohan Dantam and Richard Mayr

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)


Abstract
We consider finite-state Markov decision processes with the combined Energy-MeanPayoff objective. The controller tries to avoid running out of energy while simultaneously attaining a strictly positive mean payoff in a second dimension. We show that finite memory suffices for almost surely winning strategies for the Energy-MeanPayoff objective. This is in contrast to the closely related Energy-Parity objective, where almost surely winning strategies require infinite memory in general. We show that exponential memory is sufficient (even for deterministic strategies) and necessary (even for randomized strategies) for almost surely winning Energy-MeanPayoff. The upper bound holds even if the strictly positive mean payoff part of the objective is generalized to multidimensional strictly positive mean payoff. Finally, it is decidable in pseudo-polynomial time whether an almost surely winning strategy exists.

Cite as

Mohan Dantam and Richard Mayr. Finite-Memory Strategies for Almost-Sure Energy-MeanPayoff Objectives in MDPs. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 133:1-133:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{dantam_et_al:LIPIcs.ICALP.2024.133,
  author =	{Dantam, Mohan and Mayr, Richard},
  title =	{{Finite-Memory Strategies for Almost-Sure Energy-MeanPayoff Objectives in MDPs}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{133:1--133:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.133},
  URN =		{urn:nbn:de:0030-drops-202762},
  doi =		{10.4230/LIPIcs.ICALP.2024.133},
  annote =	{Keywords: Markov decision processes, energy, mean payoff, parity, strategy complexity}
}
Document
Invited Talk
The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)

Authors: Patricia Bouyer, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)


Abstract
Two-player turn-based zero-sum games on (finite or infinite) graphs are a central framework in theoretical computer science - notably as a tool for controller synthesis, but also due to their connection with logic and automata theory. A crucial challenge in the field is to understand how complex strategies need to be to play optimally, given a type of game and a winning objective. In this invited contribution, we give a tour of recent advances aiming to characterize games where finite-memory strategies suffice (i.e., using a limited amount of information about the past). We mostly focus on so-called chromatic memory, which is limited to using colors - the basic building blocks of objectives - seen along a play to update itself. Chromatic memory has the advantage of being usable in different game graphs, and the corresponding class of strategies turns out to be of great interest to both the practical and the theoretical sides.

Cite as

Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk). In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2022.3,
  author =	{Bouyer, Patricia and Randour, Mickael and Vandenhove, Pierre},
  title =	{{The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.3},
  URN =		{urn:nbn:de:0030-drops-173957},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.3},
  annote =	{Keywords: two-player games on graphs, finite-memory strategies, chromatic memory, parity automata, \omega-regularity}
}
Document
Arena-Independent Finite-Memory Determinacy in Stochastic Games

Authors: Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

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


Abstract
We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-making in presence of an antagonistic opponent in a random environment. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., randomization or memory requirements)? Our contributions further the understanding of arena-independent finite-memory (AIFM) determinacy, i.e., the study of objectives for which memory is needed, but in a way that only depends on limited parameters of the game graphs. First, we show that objectives for which pure AIFM strategies suffice to play optimally also admit pure AIFM subgame perfect strategies. Second, we show that we can reduce the study of objectives for which pure AIFM strategies suffice in two-player stochastic games to the easier study of one-player stochastic games (i.e., Markov decision processes). Third, we characterize the sufficiency of AIFM strategies through two intuitive properties of objectives. This work extends a line of research started on deterministic games in [Bouyer et al., 2020] to stochastic ones.

Cite as

Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Arena-Independent Finite-Memory Determinacy in Stochastic Games. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2021.26,
  author =	{Bouyer, Patricia and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
  title =	{{Arena-Independent Finite-Memory Determinacy in Stochastic Games}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{26:1--26:18},
  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.26},
  URN =		{urn:nbn:de:0030-drops-144037},
  doi =		{10.4230/LIPIcs.CONCUR.2021.26},
  annote =	{Keywords: two-player games on graphs, stochastic games, Markov decision processes, finite-memory determinacy, optimal strategies}
}
Document
Games Where You Can Play Optimally with Arena-Independent Finite Memory

Authors: Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies. In 2005, Gimbert and Zielonka [Hugo Gimbert and Wieslaw Zielonka, 2005] provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory - finite or infinite - is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us. In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory strategies in all one-player games, then it is also the case in all two-player games. Finally, we pinpoint the boundaries of our results with regard to the literature: our work completely covers the case of arena-independent memory (e.g., multiple parity objectives, lower- and upper-bounded energy objectives), and paves the way to the arena-dependent case (e.g., multiple lower-bounded energy objectives).

Cite as

Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games Where You Can Play Optimally with Arena-Independent Finite Memory. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2020.24,
  author =	{Bouyer, Patricia and Le Roux, St\'{e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
  title =	{{Games Where You Can Play Optimally with Arena-Independent Finite Memory}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{24:1--24:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.24},
  URN =		{urn:nbn:de:0030-drops-128360},
  doi =		{10.4230/LIPIcs.CONCUR.2020.24},
  annote =	{Keywords: two-player games on graphs, finite-memory determinacy, optimal strategies}
}
Document
Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives

Authors: Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
The window mechanism was introduced by Chatterjee et al. [Krishnendu Chatterjee et al., 2015] to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games, thanks to the ability to reason about such time bounds in system specifications, but also the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering the fundamental threshold probability problem in Markov decision processes for window objectives. That is, given such an objective, we want to synthesize strategies that guarantee satisfying runs with a given probability. We solve this problem for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.

Cite as

Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.8,
  author =	{Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael},
  title =	{{Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.8},
  URN =		{urn:nbn:de:0030-drops-109103},
  doi =		{10.4230/LIPIcs.CONCUR.2019.8},
  annote =	{Keywords: Markov decision processes, window mean-payoff, window parity}
}
Document
The Complexity of Rational Synthesis for Concurrent Games

Authors: Rodica Condurache, Youssouf Oualhadj, and Nicolas Troquard

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
In this paper, we investigate the rational synthesis problem for concurrent game structures for a variety of objectives ranging from reachability to Muller condition. We propose a new algorithm that establishes the decidability of the non cooperative rational synthesis problem that relies solely on game theoretic techniques as opposed to previous approaches that are logic based. Given an instance of the rational synthesis problem, we construct a zero-sum turn-based game that can be adapted to each one of the class of objectives. We obtain new complexity results. In particular, we show that in the cases of reachability, safety, Büchi, and co-Büchi objectives the problem is in PSpace, providing a tight upper-bound to the PSpace-hardness already established for turn-based games. In the case of Muller objective the problem is in ExpTime. We also obtain positive results when we assume a fixed number of agents, in which case the problem falls into PTime for reachability, safety, Büchi, and co-Büchi objectives.

Cite as

Rodica Condurache, Youssouf Oualhadj, and Nicolas Troquard. The Complexity of Rational Synthesis for Concurrent Games. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 38:1-38:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{condurache_et_al:LIPIcs.CONCUR.2018.38,
  author =	{Condurache, Rodica and Oualhadj, Youssouf and Troquard, Nicolas},
  title =	{{The Complexity of Rational Synthesis for Concurrent Games}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{38:1--38:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.38},
  URN =		{urn:nbn:de:0030-drops-95766},
  doi =		{10.4230/LIPIcs.CONCUR.2018.38},
  annote =	{Keywords: Synthesis, concurrent games, Nash equilibria}
}
  • Refine by Author
  • 4 Oualhadj, Youssouf
  • 4 Randour, Mickael
  • 3 Bouyer, Patricia
  • 3 Vandenhove, Pierre
  • 1 Brihaye, Thomas
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Algorithmic game theory
  • 2 Theory of computation → Logic and verification
  • 1 Mathematics of computing → Probability and statistics
  • 1 Software and its engineering → Formal methods
  • Show More...

  • Refine by Keyword
  • 3 Markov decision processes
  • 3 two-player games on graphs
  • 2 finite-memory determinacy
  • 2 optimal strategies
  • 1 Algorithmic game theory
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 3 2024
  • 1 2018
  • 1 2019
  • 1 2020
  • 1 2021
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail