Author name cluster

Stephane Le Roux

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.

4 papers

1 author row

LAMAS&SR Workshop 2021 Workshop Paper

Existence of Nash Equilibria in 2-Player Simultaneous Games and Priority Games Proven in Isabelle

Stephane Le Roux
Érik Martin-Dorel
Jan-Georg Smaus

In previous work, we have studied a very general formalism of two-player games relevant for applications such as model checking. We assume games in which strategies by the players lead to outcomes taken from a finite set, and each player strives for an outcome that is optimal according to his/her preferences. We have shown using the proof assistants Isabelle and Coq that if the game has a certain structure, then a Nash equilibrium exists; more precisely, any game can be abstracted by disregarding the preferences and simply saying that some outcomes are mapped to “win for player 1”, all the others to “win for player 2”. The particular structure we consider are those games for which every such abstraction leads to a game which has a determined winner. Here, we contribute several continuations of the work and their Isabelle formalisations.

PDF Details

IJCAI Conference 2017 Conference Paper

Reduction Techniques for Model Checking and Learning in MDPs

Suda Bharadwaj
Stephane Le Roux
Guillermo Perez
Ufuk Topcu

Omega-regular objectives in Markov decision processes (MDPs) reduce to reachability: find a policy which maximizes the probability of reaching a target set of states. Given an MDP, an initial distribution, and a target set of states, such a policy can be computed by most probabilistic model checking tools. If the MDP is only partially specified, i. e. , some prob- abilities are unknown, then model-learning techniques can be used to statistically approximate the probabilities and enable the computation of the de- sired policy. For fully specified MDPs, reducing the size of the MDP translates into faster model checking; for partially specified MDPs, into faster learning. We provide reduction techniques that al- low us to remove irrelevant transition probabilities: transition probabilities (known, or to be learned) that do not influence the maximal reachability probability. Among other applications, these reductions can be seen as a pre-processing of MDPs before model checking or as a way to reduce the number of experiments required to obtain a good approximation of an unknown MDP.

PDF Details

Highlights Conference 2016 Conference Abstract

Extending finite-memory determinacy by boolean combination of winning conditions

Stephane Le Roux
Arno Pauly

This talk considers turn-based, infinite duration, two-player, win/lose games played on finite graphs. In the literature, who wins a play is defined via winning conditions such as Muller, energy, reachability, mean-payoff, etc. The usual winning conditions guarantee the existence of winning strategies that are simple enough to be implemented via finite automata. This guarantee is called finite-memory determinacy. Advanced modeling may involve combinations of the usual winning conditions mentioned above. Finite-memory determinacy may or may not be preserved by such combinations. I will describe a criterion for boolean combinations of winning conditions to preserve this determinacy. The criterion is general enough to imply finite-memory determinacy of energy Muller games, multi-dimensional bounded energy games, etc.

Details

Highlights Conference 2015 Conference Abstract

Infinite subgame perfect equilibrium in the Hausdorff difference hierarchy

Stephane Le Roux

Subgame perfect equilibria are specific Nash equilibria in perfect information games in extensive form. They are important because they relate to the rationality of the players. They always exist in infinite games with continuous real-valued payoffs, but may fail to exist even in simple games with slightly discontinuous payoffs. This article considers only games whose outcome functions are measurable in the Hausdorff difference hierarchy of the open sets (i. e. Delta^0_2 when in the Baire space), and it characterizes the families of linear preferences such that every game using these preferences has a subgame perfect equilibrium: the preferences without infinite ascending chains (of course), and such that for all players a and b and outcomes x, y, z we have not (z <_a y <_a x and x <_b z <_b y). Moreover at each node of the game, the equilibrium constructed for the proof is Pareto-optimal among all the outcomes occurring in the subgame. Additional results for non-linear preferences are presented.

Details