Search Results

Documents authored by Geeraerts, Gilles

Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.35
Dynamics on Games: Simulation-Based Techniques and Applications to Routing

Authors: Thomas Brihaye, Gilles Geeraerts, Marion Hallet, Benjamin Monmege, and Bruno Quoitin

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We consider multi-player games played on graphs, in which the players aim at fulfilling their own (not necessarily antagonistic) objectives. In the spirit of evolutionary game theory, we suppose that the players have the right to repeatedly update their respective strategies (for instance, to improve the outcome w.r.t. the current strategy profile). This generates a dynamics in the game which may eventually stabilise to an equilibrium. The objective of the present paper is twofold. First, we aim at drawing a general framework to reason about the termination of such dynamics. In particular, we identify preorders on games (inspired from the classical notion of simulation between transitions systems, and from the notion of graph minor) which preserve termination of dynamics. Second, we show the applicability of the previously developed framework to interdomain routing problems.
Cite as

Thomas Brihaye, Gilles Geeraerts, Marion Hallet, Benjamin Monmege, and Bruno Quoitin. Dynamics on Games: Simulation-Based Techniques and Applications to Routing. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 35:1-35:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.FSTTCS.2019.35,
  author =	{Brihaye, Thomas and Geeraerts, Gilles and Hallet, Marion and Monmege, Benjamin and Quoitin, Bruno},
  title =	{{Dynamics on Games: Simulation-Based Techniques and Applications to Routing}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{35:1--35:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.35},
  URN =		{urn:nbn:de:0030-drops-115978},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.35},
  annote =	{Keywords: games on graphs, dynamics, simulation, network}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.36
Safe and Optimal Scheduling for Hard and Soft Tasks

Authors: Gilles Geeraerts, Shibashis Guha, and Jean-François Raskin

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

Abstract
We consider a stochastic scheduling problem with both hard and soft tasks on a single machine. Each task is described by a discrete probability distribution over possible execution times, and possible inter-arrival times of the job, and a fixed deadline. Soft tasks also carry a penalty cost to be paid when they miss a deadline. We ask to compute an online and non-clairvoyant scheduler (i.e. one that must take decisions without knowing the future evolution of the system) that is safe and efficient. Safety imposes that deadline of hard tasks are never violated while efficient means that we want to minimise the mean cost of missing deadlines by soft tasks. First, we show that the dynamics of such a system can be modelled as a finite Markov Decision Process (MDP). Second, we show that our scheduling problem is PP-hard and in EXPTime. Third, we report on a prototype tool that solves our scheduling problem by relying on the Storm tool to analyse the corresponding MDP. We show how antichain techniques can be used as a potential heuristic.
Cite as

Gilles Geeraerts, Shibashis Guha, and Jean-François Raskin. Safe and Optimal Scheduling for Hard and Soft Tasks. 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. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{geeraerts_et_al:LIPIcs.FSTTCS.2018.36,
  author =	{Geeraerts, Gilles and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Safe and Optimal Scheduling for Hard and Soft Tasks}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{36:1--36:22},
  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.36},
  URN =		{urn:nbn:de:0030-drops-99352},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.36},
  annote =	{Keywords: Non-clairvoyant scheduling, hard and soft tasks, automatic synthesis, Markov decision processes}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.7
Timed-Automata-Based Verification of MITL over Signals

Authors: Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
It has been argued that the most suitable semantic model for real-time formalisms is the non-negative real line (signals), i.e. the continuous semantics, which naturally captures the continuous evolution of system states. Existing tools like UPPAAL are, however, based on omega-sequences with timestamps (timed words), i.e. the pointwise semantics. Furthermore, the support for logic formalisms is very limited in these tools. In this article, we amend these issues by a compositional translation from Metric Temporal Interval Logic (MITL) to signal automata. Combined with an emptiness-preserving encoding of signal automata into timed automata, we obtain a practical automata-based approach to MITL model-checking over signals. We implement the translation in our tool MightyL and report on case studies using LTSmin as the back-end.
Cite as

Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. Timed-Automata-Based Verification of MITL over Signals. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.TIME.2017.7,
  author =	{Brihaye, Thomas and Geeraerts, Gilles and Ho, Hsi-Ming and Monmege, Benjamin},
  title =	{{Timed-Automata-Based Verification of MITL over Signals}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.7},
  URN =		{urn:nbn:de:0030-drops-79126},
  doi =		{10.4230/LIPIcs.TIME.2017.7},
  annote =	{Keywords: real-time temporal logic, timed automata, real-time systems}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.13
Models and Algorithms for Chronology

Authors: Gilles Geeraerts, Eythan Levy, and Frédéric Pluquet

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
The last decades have seen the rise of many fundamental chronological debates in Old World archaeology, with far-reaching historical implications. Yet, outside of radiocarbon dating - where Bayesian formal tools and models are applied - these chronological debates are still relying on non-formal models, and dates are mostly derived by hand, without the use of mathematical or computational tools, albeit the large number of complex constraints to be taken into account. This article presents formal models and algorithms for encoding archaeologically-relevant chronological constraints, computing optimal chronologies in an automated way, and automatically checking for chronological properties of a given model.
Cite as

Gilles Geeraerts, Eythan Levy, and Frédéric Pluquet. Models and Algorithms for Chronology. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{geeraerts_et_al:LIPIcs.TIME.2017.13,
  author =	{Geeraerts, Gilles and Levy, Eythan and Pluquet, Fr\'{e}d\'{e}ric},
  title =	{{Models and Algorithms for Chronology}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.13},
  URN =		{urn:nbn:de:0030-drops-79294},
  doi =		{10.4230/LIPIcs.TIME.2017.13},
  annote =	{Keywords: Chronology, Algorithms, Archaeology, Formal methods}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.123
Admissiblity in Concurrent Games

Authors: Nicolas Basset, Gilles Geeraerts, Jean-François Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
In this paper, we study the notion of admissibility for randomised strategies in concurrent games. Intuitively, an admissible strategy is one where the player plays 'as well as possible', because there is no other strategy that dominates it, i.e., that wins (almost surely) against a superset of adversarial strategies. We prove that admissible strategies always exist in concurrent games, and we characterise them precisely. Then, when the objectives of the players are omega-regular, we show how to perform assume-admissible synthesis, i.e., how to compute admissible strategies that win (almost surely) under the hypothesis that the other players play admissible strategies only.
Cite as

Nicolas Basset, Gilles Geeraerts, Jean-François Raskin, and Ocan Sankur. Admissiblity in Concurrent Games. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 123:1-123:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{basset_et_al:LIPIcs.ICALP.2017.123,
  author =	{Basset, Nicolas and Geeraerts, Gilles and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{Admissiblity in Concurrent Games}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{123:1--123:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian 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.ICALP.2017.123},
  URN =		{urn:nbn:de:0030-drops-74765},
  doi =		{10.4230/LIPIcs.ICALP.2017.123},
  annote =	{Keywords: Multi-player games, admissibility, concurrent games, randomized strategies}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.278
Simple Priced Timed Games are not That Simple

Authors: Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the costs of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary (positive and negative) weights and show that, for an important subclass of theirs (the so-called simple priced timed games), one can compute, in exponential time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called reset-acyclic priced timed games (with arbitrary weights and one-clock).
Cite as

Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. Simple Priced Timed Games are not That Simple. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 278-292, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.FSTTCS.2015.278,
  author =	{Brihaye, Thomas and Geeraerts, Gilles and Haddad, Axel and Lefaucheux, Engel and Monmege, Benjamin},
  title =	{{Simple Priced Timed Games are not That Simple}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{278--292},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.278},
  URN =		{urn:nbn:de:0030-drops-56235},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.278},
  annote =	{Keywords: Priced timed games, real-time systems, game theory}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.293
Quantitative Games under Failures

Authors: Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Benjamin Monmege, Guillermo A. Pérez, and Gabriel Renault

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We study a generalisation of sabotage games, a model of dynamic network games introduced by van Benthem. The original definition of the game is inherently finite and therefore does not allow one to model infinite processes. We propose an extension of the sabotage games in which the first player (Runner) traverses an arena with dynamic weights determined by the second player (Saboteur). In our model of quantitative sabotage games, Saboteur is now given a budget that he can distribute amongst the edges of the graph, whilst Runner attempts to minimise the quantity of budget witnessed while completing his task. We show that, on the one hand, for most of the classical cost functions considered in the literature, the problem of determining if Runner has a strategy to ensure a cost below some threshold is EXPTIME-complete. On the other hand, if the budget of Saboteur is fixed a priori, then the problem is in PTIME for most cost functions. Finally, we show that restricting the dynamics of the game also leads to better complexity.
Cite as

Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Benjamin Monmege, Guillermo A. Pérez, and Gabriel Renault. Quantitative Games under Failures. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 293-306, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.FSTTCS.2015.293,
  author =	{Brihaye, Thomas and Geeraerts, Gilles and Haddad, Axel and Monmege, Benjamin and P\'{e}rez, Guillermo A. and Renault, Gabriel},
  title =	{{Quantitative Games under Failures}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{293--306},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.293},
  URN =		{urn:nbn:de:0030-drops-56229},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.293},
  annote =	{Keywords: Quantitative games, verification, synthesis, game theory}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.297
To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games

Authors: Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Quantitative games are two-player zero-sum games played on directed weighted graphs. Total-payoff games - that can be seen as a refinement of the well-studied mean-payoff games - are the variant where the payoff of a play is computed as the sum of the weights. Our aim is to describe the first pseudo-polynomial time algorithm for total-payoff games in the presence of arbitrary weights. It consists of a non-trivial application of the value iteration paradigm. Indeed, it requires to study, as a milestone, a refinement of these games, called min-cost reachability games, where we add a reachability objective to one of the players. For these games, we give an efficient value iteration algorithm to compute the values and optimal strategies (when they exist), that runs in pseudo-polynomial time. We also propose heuristics to speed up the computations.
Cite as

Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 297-310, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2015.297,
  author =	{Brihaye, Thomas and Geeraerts, Gilles and Haddad, Axel and Monmege, Benjamin},
  title =	{{To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{297--310},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.297},
  URN =		{urn:nbn:de:0030-drops-53729},
  doi =		{10.4230/LIPIcs.CONCUR.2015.297},
  annote =	{Keywords: Games on graphs, reachability, quantitative games, value iteration}
}
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