Author name cluster

Clément Tamines

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

Highlights Conference 2022 Conference Abstract

Pareto-Rational Verification

Clément Tamines

We study the rational verification problem which consists in verifying the correctness of a system executing in an environment that is assumed to behave rationally. We consider the model of rationality in which the environment only executes behaviors that are Pareto-optimal with regards to its set of objectives, given the behaviour of the system (which is committed in advance of any interaction). When the objectives are ω-regular, we prove that the Pareto-rational verification problem is co-NP-complete and fixed-parameter tractable (FPT) in the number of objectives of the environment. When the objectives are described by LTL formulas, the problem is PSPACE-complete, similarly to the classical LTL model-checking problem. In order to evaluate the applicability of our results in practice, we have implemented and evaluated two variations of our FPT algorithm on our running example and on randomly generated instances. This is a joint work with Véronique Bruyère and Jean-François Raskin.

Details

Highlights Conference 2021 Conference Abstract

Stackelberg-Pareto Synthesis

Clément Tamines

In this talk, we consider 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. This talk presents joint work with Véronique Bruyère and Jean-François Raskin.

Details