14 Search Results for "Geeraerts, Gilles"

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.5
MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm

Authors: S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan

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

Abstract
The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since timed automata tools do not handle alternation, existing methods perform an additional step of converting the alternating timed automata into timed automata. This "de-alternation" step proceeds by an intricate finite abstraction of the space of configurations of the alternating automaton. Recently, a model of generalized timed automata (GTA) has been proposed. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. An attractive feature of GTAs is the presence of future clocks which act like timers that guess a time to an event and stay alive until a timeout. Future clocks seem to provide another natural way to implement the guess-and-check: start the future clock with a guessed time to an event and check its occurrence using a timeout. Indeed, using this feature, we provide a new concise translation from MITL to GTA. In particular, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art. Thanks to this conversion, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. Due to the presence of future clocks, there is no finite time-abstract bisimulation (region equivalence) for GTAs, whereas liveness algorithms for timed automata crucially rely on the presence of the finite region equivalence. As our second contribution, we provide a new zone-based algorithm for checking Büchi non-emptiness in GTAs, which circumvents this fundamental challenge.
Cite as

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2024.5,
  author =	{Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
  title =	{{MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{5:1--5:19},
  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.5},
  URN =		{urn:nbn:de:0030-drops-207774},
  doi =		{10.4230/LIPIcs.CONCUR.2024.5},
  annote =	{Keywords: MITL model checking, timed automata, zones, liveness}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.14
As Soon as Possible but Rationally

Authors: Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin

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

Abstract
This paper addresses complexity problems in rational verification and synthesis for multi-player games played on weighted graphs, where the objective of each player is to minimize the cost of reaching a specific set of target vertices. In these games, one player, referred to as the system, declares his strategy upfront. The other players, composing the environment, then rationally make their moves according to their objectives. The rational behavior of these responding players is captured through two models: they opt for strategies that either represent a Nash equilibrium or lead to a play with a Pareto-optimal cost tuple.
Cite as

Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. As Soon as Possible but Rationally. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2024.14,
  author =	{Bruy\`{e}re, V\'{e}ronique and Grandmont, Christophe and Raskin, Jean-Fran\c{c}ois},
  title =	{{As Soon as Possible but Rationally}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{14:1--14:20},
  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.14},
  URN =		{urn:nbn:de:0030-drops-207869},
  doi =		{10.4230/LIPIcs.CONCUR.2024.14},
  annote =	{Keywords: Games played on graphs, rational verification, rational synthesis, Nash equilibrium, Pareto-optimality, quantitative reachability objectives}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.27
Inaproximability in Weighted Timed Games

Authors: Quentin Guilmant and Joël Ouaknine

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

Abstract
We consider two-player, turn-based weighted timed games played on timed automata equipped with (positive and negative) integer weights, in which one player seeks to reach a goal location whilst minimising the cumulative weight of the underlying path. Although the value problem for such games (is the value of the game below a given threshold?) is known to be undecidable, the question of whether one can approximate this value has remained a longstanding open problem. In this paper, we resolve this question by showing that approximating arbitrarily closely the value of a given weighted timed game is computationally unsolvable.
Cite as

Quentin Guilmant and Joël Ouaknine. Inaproximability in Weighted Timed Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guilmant_et_al:LIPIcs.CONCUR.2024.27,
  author =	{Guilmant, Quentin and Ouaknine, Jo\"{e}l},
  title =	{{Inaproximability in Weighted Timed Games}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{27:1--27:15},
  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.27},
  URN =		{urn:nbn:de:0030-drops-207998},
  doi =		{10.4230/LIPIcs.CONCUR.2024.27},
  annote =	{Keywords: Weighted timed games, approximation, undecidability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.74
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
DOI: 10.4230/LIPIcs.SAT.2024.15
Antichain with SAT and Tries

Authors: Lukáš Holík and Pavol Vargovčík

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
We introduce a SAT-enabled version of an antichain algorithm for checking language emptiness of alternating finite automata (AFA) with complex transition relations encoded as compact logical formulae. The SAT solver is used to compute predecessors of AFA configurations, and at the same time, to evaluate the subsumption of newly found configurations in the antichain of the previously found ones. The algorithm could be naively implemented by an incremental SAT solver where the growing antichain is represented by adding new clauses. To make it efficient, we 1) force the SAT solver to prioritize largest/subsumption-strongest predecessors (so that weaker configurations are not even generated), and 2) store the antichain clauses in a special variant of a trie that allows fast subsumption testing. The experimental results suggest that the resulting emptiness checker is very efficient compared to the state of the art and that our techniques improve the performance of the SAT solver.
Cite as

Lukáš Holík and Pavol Vargovčík. Antichain with SAT and Tries. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{holik_et_al:LIPIcs.SAT.2024.15,
  author =	{Hol{\'\i}k, Luk\'{a}\v{s} and Vargov\v{c}{\'\i}k, Pavol},
  title =	{{Antichain with SAT and Tries}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{15:1--15:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15},
  URN =		{urn:nbn:de:0030-drops-205372},
  doi =		{10.4230/LIPIcs.SAT.2024.15},
  annote =	{Keywords: SAT, Trie, Antichain, Alternating automata, Subset query}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.13
Simulations for Event-Clock Automata

Authors: S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied in [Gilles Geeraerts et al., 2011; Gilles Geeraerts et al., 2014], where the authors also proposed a solution using zone extrapolations. In this paper, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the 𝒢-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.
Cite as

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. Simulations for Event-Clock Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2022.13,
  author =	{Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
  title =	{{Simulations for Event-Clock Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir 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.CONCUR.2022.13},
  URN =		{urn:nbn:de:0030-drops-170766},
  doi =		{10.4230/LIPIcs.CONCUR.2022.13},
  annote =	{Keywords: Event-clock automata, verification, zones, simulations, reachability}
}
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}
}
  • Refine by Author
  • 8 Geeraerts, Gilles
  • 6 Monmege, Benjamin
  • 5 Brihaye, Thomas
  • 3 Haddad, Axel
  • 3 Raskin, Jean-François
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 2 Theory of computation → Algorithmic game theory
  • 2 Theory of computation → Quantitative automata
  • 2 Theory of computation → Timed and hybrid models
  • 1 Computer systems organization → Embedded systems
  • Show More...

  • Refine by Keyword
  • 2 Weighted timed games
  • 2 game theory
  • 2 reachability
  • 2 real-time systems
  • 2 timed automata
  • Show More...

  • Refine by Type
  • 14 document

  • Refine by Publication Year
  • 5 2024
  • 3 2015
  • 3 2017
  • 1 2018
  • 1 2019
  • 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact