BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Véronique Bruyère

Véronique Bruyère appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Computer Science and Game TheoryFormal Languages and Automata TheoryLogic in Computer ScienceData Structures and AlgorithmsSystems and Control

Catalog footprint

What is connected

14works
5topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

14 published item(s)

preprint2022arXiv

Pareto-Rational Verification

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 regard to its set of objectives, given the behavior of the system (which is committed in advance of any interaction). We examine two ways of specifying this behavior, first by means of a deterministic Moore machine, and then by lifting its determinism. In the latter case the machine may embed several different behaviors for the system, and the universal rational verification problem aims at verifying that all of them are correct when the environment is rational. For parity objectives, we prove that the Pareto-rational verification problem is co-NP-complete and that its universal version is in PSPACE and both NP-hard and co-NP-hard. For Boolean Büchi objectives, the former problem is $Π_2\mathsf{P}$-complete and the latter is PSPACE-complete. We also study the case where the objectives are expressed using LTL formulas and show that the first problem is PSPACE-complete, and that the second is 2EXPTIME-complete. Both problems are also shown to be fixed-parameter tractable (FPT) for parity and Boolean Büchi objectives. Finally, we evaluate two variations of the FPT algorithm proposed to solve the Pareto-rational verification problem on a parametric toy example as well as on randomly generated instances.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Stackelberg-Pareto Synthesis (Extended Version)

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

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.

0 citations0 reviewsNo code linkedOpen access