6 Search Results for "Busatto-Gaston, Damien"

Document
DOI: 10.4230/LIPIcs.CSL.2026.33
Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games

Authors: Isa Vialard

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs, which remained stubbornly open for a decade, was recently shown to be undecidable. In this paper, we show that the Value Problem is decidable when considering two-clock almost non-Zeno wtgs.
Cite as

Isa Vialard. Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{vialard:LIPIcs.CSL.2026.33,
  author =	{Vialard, Isa},
  title =	{{Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.33},
  URN =		{urn:nbn:de:0030-drops-254580},
  doi =		{10.4230/LIPIcs.CSL.2026.33},
  annote =	{Keywords: Weighted timed games, decidability, real-time systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.36
Explainability is a Game for Probabilistic Bisimilarity Distances

Authors: Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
We revisit a game from the literature that characterizes the probabilistic bisimilarity distances of a labelled Markov chain. We illustrate how an optimal policy of the game can explain these distances. Like the games that characterize bisimilarity and probabilistic bisimilarity, the game is played on pairs of states and matches transitions of those states. To obtain more convincing and interpretable explanations than those provided by generic optimal policies, we restrict to optimal policies that delay reaching observably inequivalent state pairs for as long as possible (called 1-maximal) while quickly reaching equivalent ones (called 0-minimal). We present iterative algorithms that compute 1-maximal and 0-minimal policies and prove an exponential lower bound for the number of iterations of the algorithm that computes 1-maximal policies.
Cite as

Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel. Explainability is a Game for Probabilistic Bisimilarity Distances. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vlasman_et_al:LIPIcs.CONCUR.2025.36,
  author =	{Vlasman, Emily and Nanah Ji, Anto and Worrell, James and van Breugel, Franck},
  title =	{{Explainability is a Game for Probabilistic Bisimilarity Distances}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.36},
  URN =		{urn:nbn:de:0030-drops-239861},
  doi =		{10.4230/LIPIcs.CONCUR.2025.36},
  annote =	{Keywords: probabilistic bisimilarity distance, labelled Markov chain, game, policy, explainability}
}
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}
}
  • Refine by Type
  • 6 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2024
  • 1 2022
  • 1 2020
  • Show More...

  • Refine by Author
  • 4 Busatto-Gaston, Damien
  • 1 Bordais, Benjamin
  • 1 Chakraborty, Debraj
  • 1 Guha, Shibashis
  • 1 Monmege, Benjamin
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Timed and hybrid models
  • 1 Mathematics of computing → Probability and statistics
  • 1 Mathematics of computing → Stochastic processes
  • 1 Theory of computation → Algorithmic game theory
  • 1 Theory of computation → Convergence and learning in games
  • Show More...

  • Refine by Keyword
  • 2 Weighted timed games
  • 1 Approximation
  • 1 Fairness
  • 1 Game theory
  • 1 Markov decision process
  • Show More...

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