arXiv subjects

Véronique Bruyère

Publications and source records attributed to Véronique Bruyère.

At least 37 records · Page 2Linked to original sources

arXiv2018

Constrained existence problem for weak subgame perfect equilibria with omega-regular Boolean objectives (full version)

We study multiplayer turn-based games played on a finite directed graph such that each player aims at satisfying an omega-regular Boolean objective. Instead of the well-known notions of Nash equilibrium (NE) and subgame perfect equilibrium (SPE), we focus on the recent notion of weak subgame perfect equilibrium (weak SPE), a refinement of SPE. In this setting, players who deviate can only use the subclass of strategies that differ from the original one on a finite number of histories. We are interested in the constrained existence problem for weak SPEs. We provide a complete characterization of the computational complexity of this problem: it is P-complete for Explicit Muller objectives, NP-complete for Co-Büchi, Parity, Muller, Rabin, and Streett objectives, and PSPACE-complete for Reachability and Safety objectives (we only prove NP-membership for Büchi objectives). We also show that the constrained existence problem is fixed parameter tractable and is polynomial when the number of players is fixed. All these results are based on a fine analysis of a fixpoint algorithm that computes the set of possible payoff profiles underlying weak SPEs.

cs.GT↗

arXiv2018

Parameterized complexity of games with monotonically ordered ω-regular objectives

In recent years, two-player zero-sum games with multiple objectives have received a lot of interest as a model for the synthesis of complex reactive systems. In this framework, Player 1 wins if he can ensure that all objectives are satisfied against any behavior of Player 2. When this is not possible to satisfy all the objectives at once, an alternative is to use some preorder on the objectives according to which subset of objectives Player 1 wants to satisfy. For example, it is often natural to provide more significance to one objective over another, a situation that can be modelled with lexicographically ordered objectives for instance. Inspired by recent work on concurrent games with multiple ω-regular objectives by Bouyer et al., we investigate in detail turned-based games with monotonically ordered and ω-regular objectives. We study the threshold problem which asks whether player 1 can ensure a payoff greater than or equal to a given threshold w.r.t. a given monotonic preorder. As the number of objectives is usually much smaller than the size of the game graph, we provide a parametric complexity analysis and we show that our threshold problem is in FPT for all monotonic preorders and all classical types of ω-regular objectives. We also provide polynomial time algorithms for Büchi, coBüchi and explicit Muller objectives for a large subclass of monotonic preorders that includes among others the lexicographic preorder. In the particular case of lexicographic preorder, we also study the complexity of computing the values and the memory requirements of optimal strategies.

cs.GT↗

arXiv2017

On the existence of weak subgame perfect equilibria

We study multi-player turn-based games played on (potentially infinite) directed graphs. An outcome is assigned to every play of the game. Each player has a preference relation on the set of outcomes which allows him to compare plays. We focus on the recently introduced notion of weak subgame perfect equilibrium (weak SPE). This is a variant of the classical notion of SPE, where players who deviate can only use strategies deviating from their initial strategy in a finite number of histories. Having an SPE in a game implies having a weak SPE but the contrary is generally false. We propose general conditions on the structure of the game graph and on the preference relations of the players that guarantee the existence of a weak SPE, that additionally is finite-memory. From this general result, we derive two large classes of games for which there always exists a weak SPE: (i) the games with a finite-range outcome function, and (ii) the games with a finite underlying graph and a prefix-independent outcome function. For the second class, we identify conditions on the preference relations that guarantee memoryless strategies for the weak SPE.

cs.GT↗

arXiv2017

Computer aided synthesis: a game theoretic approach

In this invited contribution, we propose a comprehensive introduction to game theory applied in computer aided synthesis. In this context, we give some classical results on two-player zero-sum games and then on multi-player non zero-sum games. The simple case of one-player games is strongly related to automata theory on infinite words. All along the article, we focus on general approaches to solve the studied problems, and we provide several illustrative examples as well as intuitions on the proofs.

cs.GT↗

arXiv2016

Secure Equilibria in Weighted Games

We consider two-player non zero-sum infinite duration games played on weighted graphs. We extend the notion of secure equilibrium introduced by Chatterjee et al., from the Boolean setting to this quantitative setting. As for the Boolean setting, our notion of secure equilibrium refines the classical notion of Nash equilibrium. We prove that secure equilibria always exist in a large class of weighted games which includes common measures like sup, inf, lim sup, lim inf, mean-payoff, and discounted sum. Moreover we show that one can synthesize finite-memory strategy profiles with few memory. We also prove that the constrained existence problem for secure equilibria is decidable for sup, inf, lim sup, lim inf and mean-payoff measures. Our solutions rely on new results for zero-sum quantitative games with lexicographic objectives that are interesting on their own right.

cs.GT↗

arXiv2016

Window Parity Games: An Alternative Approach Toward Parity Games with Time Bounds (Full Version)

Classical objectives in two-player zero-sum games played on graphs often deal with limit behaviors of infinite plays: e.g., mean-payoff and total-payoff in the quantitative setting, or parity in the qualitative one (a canonical way to encode omega-regular properties). Those objectives offer powerful abstraction mechanisms and often yield nice properties such as memoryless determinacy. However, their very nature provides no guarantee on time bounds within which something good can be witnessed. In this work, we consider two approaches toward inclusion of time bounds in parity games. The first one, parity-response games, is based on the notion of finitary parity games [CHH09] and parity games with costs [FZ14,WZ16]. The second one, window parity games, is inspired by window mean-payoff games [CDRR15]. We compare the two approaches and show that while they prove to be equivalent in some contexts, window parity games offer a more tractable alternative when the time bound is given as a parameter (P-c. vs. PSPACE-C.). In particular, it provides a conservative approximation of parity games computable in polynomial time. Furthermore, we extend both approaches to the multi-dimension setting. We give the full picture for both types of games with regard to complexity and memory bounds. [CHH09] K. Chatterjee, T.A. Henzinger, F. Horn (2009): Finitary winning in omega-regular games. ACM Trans. Comput. Log. 11(1). [FZ14] N. Fijalkow, M. Zimmermann (2014): Parity and Streett Games with Costs. LMCS 10(2). [WZ16] A. Weinert, M. Zimmermann (2016): Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. Proc. of CSL, LIPIcs 62, pp. 31:1-31:17, Schloss Dagstuhl - LZI. [CDRR15] K. Chatterjee, L. Doyen, M. Randour, J.-F. Raskin (2015): Looking at mean-payoff and total-payoff through windows. Information and Computation 242, pp. 25-52.

cs.LO↗

arXiv2016

Window Parity Games: An Alternative Approach Toward Parity Games with Time Bounds

Classical objectives in two-player zero-sum games played on graphs often deal with limit behaviors of infinite plays: e.g., mean-payoff and total-payoff in the quantitative setting, or parity in the qualitative one (a canonical way to encode omega-regular properties). Those objectives offer powerful abstraction mechanisms and often yield nice properties such as memoryless determinacy. However, their very nature provides no guarantee on time bounds within which something good can be witnessed. In this work, we consider two approaches toward inclusion of time bounds in parity games. The first one, parity-response games, is based on the notion of finitary parity games [CHH09] and parity games with costs [FZ14,WZ16]. The second one, window parity games, is inspired by window mean-payoff games [CDRR15]. We compare the two approaches and show that while they prove to be equivalent in some contexts, window parity games offer a more tractable alternative when the time bound is given as a parameter (P-c. vs. PSPACE-c.). In particular, it provides a conservative approximation of parity games computable in polynomial time. Furthermore, we extend both approaches to the multi-dimension setting. We give the full picture for both types of games with regard to complexity and memory bounds. [CHH09] K. Chatterjee, T.A. Henzinger, F. Horn (2009): Finitary winning in omega-regular games. ACM Trans. Comput. Log. 11(1). [FZ14] N. Fijalkow, M. Zimmermann (2014): Parity and Streett Games with Costs. LMCS 10(2). [WZ16] A. Weinert, M. Zimmermann (2016): Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. Proc. of CSL, LIPIcs, Schloss Dagstuhl - LZI. To appear. [CDRR15] K. Chatterjee, L. Doyen, M. Randour, J.-F. Raskin (2015): Looking at mean-payoff and total-payoff through windows. Information and Computation 242, pp. 25-52.

cs.LO↗

arXiv2016

On the complexity of heterogeneous multidimensional quantitative games

In this paper, we study two-player zero-sum turn-based games played on a finite multidimensional weighted graph. In recent papers all dimensions use the same measure, whereas here we allow to combine different measures. Such heterogeneous multidimensional quantitative games provide a general and natural model for the study of reactive system synthesis. We focus on classical measures like the Inf, Sup, LimInf, and LimSup of the weights seen along the play, as well as on the window mean-payoff (WMP) measure. This new measure is a natural strengthening of the mean-payoff measure. We allow objectives defined as Boolean combinations of heterogeneous constraints. While multidimensional games with Boolean combinations of mean-payoff constraints are undecidable, we show that the problem becomes EXPTIME-complete for DNF/CNF Boolean combinations of heterogeneous measures taken among {WMP, Inf, Sup, LimInf, LimSup} and that exponential memory strategies are sufficient for both players to win. We provide a detailed study of the complexity and the memory requirements when the Boolean combination of the measures is replaced by an intersection. EXPTIME-completeness and exponential memory strategies still hold for the intersection of measures in {WMP, Inf, Sup, LimInf, LimSup}, and we get PSPACE-completeness when WMP measure is no longer considered. To avoid EXPTIME-or PSPACE-hardness, we impose at most one occurrence of WMP measure and fix the number of Sup measures, and we propose several refinements (on the number of occurrences of the other measures) for which we get polynomial algorithms and lower memory requirements. For all the considered classes of games, we also study parameterized complexity.

cs.GT↗

arXiv2015

Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games

We extend the quantitative synthesis framework by going beyond the worst-case. On the one hand, classical analysis of two-player games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees. On the other hand, stochastic models like Markov decision processes represent situations where the system is faced to a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing an higher expected value against a particular stochastic model of the environment given as input. This problem is relevant to produce system controllers that provide nice expected performance in the everyday situation while ensuring a strict (but relaxed) performance threshold even in the event of very bad (while unlikely) circumstances. We study the beyond worst-case synthesis problem for two important quantitative settings: the mean-payoff and the shortest path. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.

cs.GT↗

arXiv2015

Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability

We study $n$-player turn-based games played on a finite directed graph. For each play, the players have to pay a cost that they want to minimize. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. We also study natural variants of SPE, named weak (resp. very weak) SPE, where players who deviate cannot use the full class of strategies but only a subclass with a finite number of (resp. a unique) deviation step(s). Our results are threefold. Firstly, we characterize in the form of a Folk theorem the set of all plays that are the outcome of a weak SPE. Secondly, for the class of quantitative reachability games, we prove the existence of a finite-memory SPE and provide an algorithm for computing it (only existence was known with no information regarding the memory). Moreover, we show that the existence of a constrained SPE, i.e. an SPE such that each player pays a cost less than a given constant, can be decided. The proofs rely on our Folk theorem for weak SPEs (which coincide with SPEs in the case of quantitative reachability games) and on the decidability of MSO logic on infinite words. Finally with similar techniques, we provide a second general class of games for which the existence of a (constrained) weak SPE is decidable.

cs.GT↗

arXiv2014

Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes

When treating Markov decision processes (MDPs) with large state spaces, using explicit representations quickly becomes unfeasible. Lately, Wimmer et al. have proposed a so-called symblicit algorithm for the synthesis of optimal strategies in MDPs, in the quantitative setting of expected mean-payoff. This algorithm, based on the strategy iteration algorithm of Howard and Veinott, efficiently combines symbolic and explicit data structures, and uses binary decision diagrams as symbolic representation. The aim of this paper is to show that the new data structure of pseudo-antichains (an extension of antichains) provides another interesting alternative, especially for the class of monotonic MDPs. We design efficient pseudo-antichain based symblicit algorithms (with open source implementations) for two quantitative settings: the expected mean-payoff and the stochastic shortest path. For two practical applications coming from automated planning and LTL synthesis, we report promising experimental results w.r.t. both the run time and the memory consumption.

cs.LO↗

arXiv2014

Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes (extended version)

cs.DS↗

arXiv2014

Expectations or Guarantees? I Want It All! A crossroad between games and MDPs

When reasoning about the strategic capabilities of an agent, it is important to consider the nature of its adversaries. In the particular context of controller synthesis for quantitative specifications, the usual problem is to devise a strategy for a reactive system which yields some desired performance, taking into account the possible impact of the environment of the system. There are at least two ways to look at this environment. In the classical analysis of two-player quantitative games, the environment is purely antagonistic and the problem is to provide strict performance guarantees. In Markov decision processes, the environment is seen as purely stochastic: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. In this expository work, we report on recent results introducing the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing an higher expected value against a particular stochastic model of the environment given as input. This problem is relevant to produce system controllers that provide nice expected performance in the everyday situation while ensuring a strict (but relaxed) performance threshold even in the event of very bad (while unlikely) circumstances. It has been studied for both the mean-payoff and the shortest path quantitative measures.

cs.GT↗

arXiv2013

On (Subgame Perfect) Secure Equilibrium in Quantitative Reachability Games

We study turn-based quantitative multiplayer non zero-sum games played on finite graphs with reachability objectives. In such games, each player aims at reaching his own goal set of states as soon as possible. A previous work on this model showed that Nash equilibria (resp. secure equilibria) are guaranteed to exist in the multiplayer (resp. two-player) case. The existence of secure equilibria in the multiplayer case remained and is still an open problem. In this paper, we focus our study on the concept of subgame perfect equilibrium, a refinement of Nash equilibrium well-suited in the framework of games played on graphs. We also introduce the new concept of subgame perfect secure equilibrium. We prove the existence of subgame perfect equilibria (resp. subgame perfect secure equilibria) in multiplayer (resp. two-player) quantitative reachability games. Moreover, we provide an algorithm deciding the existence of secure equilibria in the multiplayer case.

cs.GT↗

arXiv2013

Synthesis from LTL Specifications with Mean-Payoff Objectives

The classical LTL synthesis problem is purely qualitative: the given LTL specification is realized or not by a reactive system. LTL is not expressive enough to formalize the correctness of reactive systems with respect to some quantitative aspects. This paper extends the qualitative LTL synthesis setting to a quantitative setting. The alphabet of actions is extended with a weight function ranging over the rational numbers. The value of an infinite word is the mean-payoff of the weights of its letters. The synthesis problem then amounts to automatically construct (if possible) a reactive system whose executions all satisfy a given LTL formula and have mean-payoff values greater than or equal to some given threshold. The latter problem is called LTLMP synthesis and the LTLMP realizability problem asks to check whether such a system exists. We first show that LTLMP realizability is not more difficult than LTL realizability: it is 2ExpTime-Complete. This is done by reduction to two-player mean-payoff parity games. While infinite memory strategies are required to realize LTLMP specifications in general, we show that epsilon-optimality can be obtained with finite memory strategies, for any epsilon > 0. To obtain an efficient algorithm in practice, we define a Safraless procedure to decide whether there exists a finite-memory strategy that realizes a given specification for some given threshold. This procedure is based on a reduction to two-player energy safety games which are in turn reduced to safety games. Finally, we show that those safety games can be solved efficiently by exploiting the structure of their state spaces and by using antichains as a symbolic data-structure. All our results extend to multi-dimensional weights. We have implemented an antichain-based procedure and we report on some promising experimental results.

cs.LO↗

arXiv2012

On Equilibria in Quantitative Games with Reachability/Safety Objectives

In this paper, we study turn-based quantitative multiplayer non zero-sum games played on finite graphs with both reachability and safety objectives. In this framework a player with a reachability objective aims at reaching his own goal as soon as possible, whereas a player with a safety objective aims at avoiding his bad set or, if impossible, delaying its visit as long as possible. We prove the existence of Nash equilibria with finite memory in quantitative multiplayer reachability/safety games. Moreover, we prove the existence of finite-memory secure equilibria for quantitative two-player reachability games.

cs.GT↗

arXiv2012

Visibly pushdown automata on trees: universality and u-universality

An automaton is universal if it accepts every possible input. We study the notion of u-universality, which asserts that the automaton accepts every input starting with u. Universality and u-universality are both EXPTIME-hard for non-deterministic tree automata. We propose efficient antichain-based techniques to address these problems for visibly pushdown automata operating on trees. One of our approaches yields algorithms for the universality and u-universality of hedge automata.

cs.FL↗

arXiv2011

Trees with Given Stability Number and Minimum Number of Stable Sets

We study the structure of trees minimizing their number of stable sets for given order $n$ and stability number $α$. Our main result is that the edges of a non-trivial extremal tree can be partitioned into $n-α$ stars, each of size $\lceil \frac{n-1}{n-α} \rceil$ or $\lfloor \frac{n-1}{n-α}\rfloor$, so that every vertex is included in at most two distinct stars, and the centers of these stars form a stable set of the tree.

math.CO↗