Clément Tamines

dblp:245/2655 · DBLP profile ↗
← Back
4ranked-venue papers
0as first author
4since 2021 · last 2024
0000-0003-1104-911XORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 3 · 3 since 2021Software engineering, systems software and programming languages · 1 · 1 since 2021
YearPublicationVenuePosition
2024 The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Swen Jacobs, Guillermo A. Pérez, Remco Abraham, Véronique Bruyère, Michaël Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov 0001, Felix Klein 0001, Michael Luttenberger, Klara J. Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaëtan Staquet, Clément Tamines, Leander Tentrup
Int. J. Softw. Tools Technol. Transf.23
2024 Stackelberg-Pareto Synthesis
abstract
We study the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study for several kinds of ω-regular objectives the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. We show that this problem is fixed-parameter tractable for games in which objectives are all reachability, safety, Büchi, co-Büchi, Boolean Büchi, parity, Muller, Streett, or Rabin objectives. We also show that this problem is NEXPTIME -complete except for the cases of Büchi objectives for which it is NP -complete and co-Büchi objectives for which it is in NEXPTIME and NP -hard. The problem is already NP -complete in the simple case of reachability objectives and graphs that are trees.
Véronique Bruyère, Baptiste Fievet, Jean-François Raskin, Clément Tamines
ACM Trans. Comput. Log.4
2022 Pareto-Rational Verification
abstract
peer reviewed
Véronique Bruyère, Jean-François Raskin, Clément Tamines
CONCUR3
2021 Stackelberg-Pareto Synthesis
abstract
In this paper, we study the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. For games in which objectives are either all parity or all reachability objectives, we show that this problem is fixed-parameter tractable and NEXPTIME-complete. This problem is already NP-complete in the simple case of reachability objectives and graphs that are trees.
Véronique Bruyère, Jean-François Raskin, Clément Tamines
CONCUR3