3 Search Results for "Busatto-Gaston, Damien"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.115
Strategy Synthesis for Global Window PCTL

Authors: Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
Given a Markov decision process (MDP) M and a formula Φ, the strategy synthesis problem asks if there exists a strategy σ s.t. the resulting Markov chain M[σ] satisfies Φ. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.
Cite as

Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin. Strategy Synthesis for Global Window PCTL. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 115:1-115:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.ICALP.2022.115,
  author =	{Bordais, Benjamin and Busatto-Gaston, Damien and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Strategy Synthesis for Global Window PCTL}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{115:1--115:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.115},
  URN =		{urn:nbn:de:0030-drops-164562},
  doi =		{10.4230/LIPIcs.ICALP.2022.115},
  annote =	{Keywords: Markov decision processes, synthesis, PCTL}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.40
Monte Carlo Tree Search Guided by Symbolic Advice for MDPs

Authors: Damien Busatto-Gaston, Debraj Chakraborty, and Jean-Francois Raskin

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

Abstract
In this paper, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). We augment the MCTS algorithm with the notion of symbolic advice, and show that its classical theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We describe how to use QBF and SAT solvers to implement symbolic advice in an efficient way. We illustrate our new algorithm using the popular game Pac-Man and show that the performances of our algorithm exceed those of plain MCTS as well as the performances of human players.
Cite as

Damien Busatto-Gaston, Debraj Chakraborty, and Jean-Francois Raskin. Monte Carlo Tree Search Guided by Symbolic Advice for MDPs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 40:1-40:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{busattogaston_et_al:LIPIcs.CONCUR.2020.40,
  author =	{Busatto-Gaston, Damien and Chakraborty, Debraj and Raskin, Jean-Francois},
  title =	{{Monte Carlo Tree Search Guided by Symbolic Advice for MDPs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{40:1--40:24},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.40},
  URN =		{urn:nbn:de:0030-drops-128523},
  doi =		{10.4230/LIPIcs.CONCUR.2020.40},
  annote =	{Keywords: Markov decision process, Monte Carlo tree search, symbolic advice, simulation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.28
Symbolic Approximation of Weighted Timed Games

Authors: Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the accumulated weight while reaching a target. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. For non-negative weights, the largest class that can be analysed has been introduced by Bouyer, Jaziri and Markey in 2015. Though the value problem is undecidable, the authors show how to approximate the value by considering regions with a refined granularity. In this work, we extend this class to incorporate negative weights, allowing one to model energy for instance, and prove that the value can still be approximated, with the same complexity. In addition, we show that a symbolic algorithm, relying on the paradigm of value iteration, can be used as an approximation schema on this class.
Cite as

Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Symbolic Approximation of Weighted Timed Games. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{busattogaston_et_al:LIPIcs.FSTTCS.2018.28,
  author =	{Busatto-Gaston, Damien and Monmege, Benjamin and Reynier, Pierre-Alain},
  title =	{{Symbolic Approximation of Weighted Timed Games}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.28},
  URN =		{urn:nbn:de:0030-drops-99277},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.28},
  annote =	{Keywords: Weighted timed games, Real-time systems, Game theory, Approximation}
}
  • Refine by Author
  • 3 Busatto-Gaston, Damien
  • 1 Bordais, Benjamin
  • 1 Chakraborty, Debraj
  • 1 Guha, Shibashis
  • 1 Monmege, Benjamin
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Stochastic processes
  • 1 Theory of computation → Algorithmic game theory
  • 1 Theory of computation → Convergence and learning in games
  • 1 Theory of computation → Quantitative automata
  • 1 Theory of computation → Theory of randomized search heuristics
  • Show More...

  • Refine by Keyword
  • 1 Approximation
  • 1 Game theory
  • 1 Markov decision process
  • 1 Markov decision processes
  • 1 Monte Carlo tree search
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2018
  • 1 2020
  • 1 2022

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact