Search Results

Documents authored by Busatto-Gaston, Damien

Document
DOI: 10.4230/LIPIcs.FSTTCS.2024.15
Promptness and Fairness in Muller LTL Formulas

Authors: Damien Busatto-Gaston, Youssouf Oualhadj, Léo Tible, and Daniele Varacca

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

Abstract
In this paper we consider two different views of the model checking problem for the Linear Temporal Logic (LTL). On the one hand, we consider the universal model checking problem for LTL, where one asks that for a given system and a given formula all the runs of the system satisfy the formula. On the other hand, the fair model checking problem for LTL asks that for a given system and a given formula almost all the runs of the system satisfy the formula. It was shown that these two problems have the same theoretical complexity, i.e. PSPACE-complete. A less expensive fragment was identified in a previous work, namely the Muller fragment, which consists of combinations of repeated reachability properties. We consider prompt LTL formulas (pLTL), that extend LTL with an additional operator, i.e. the prompt-eventually. This operator ensures the existence of a bound such that reachability properties are satisfied within this bound. This extension comes at no cost since the model checking problem remains PSPACE-complete. We show that the corresponding Muller fragment of pLTL, with prompt repeated reachability properties, enjoys similar computational improvements. Another feature of Muller formulas is that the model checking problem becomes easier under the fairness assumption. This distinction is lost in the prompt setting, as we show that the two problems are equivalent instance-wise. Subsequently, we identify a new prefix independent fragment of pLTL for which the fair model checking problem is less expensive than the universal one.
Cite as

Damien Busatto-Gaston, Youssouf Oualhadj, Léo Tible, and Daniele Varacca. Promptness and Fairness in Muller LTL Formulas. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{busattogaston_et_al:LIPIcs.FSTTCS.2024.15,
  author =	{Busatto-Gaston, Damien and Oualhadj, Youssouf and Tible, L\'{e}o and Varacca, Daniele},
  title =	{{Promptness and Fairness in Muller LTL Formulas}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{15:1--15:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.15},
  URN =		{urn:nbn:de:0030-drops-222044},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.15},
  annote =	{Keywords: Model checking, Fairness, Temporal logics}
}
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.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.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.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}
}
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 About DROPS Imprint Privacy Contact