arXiv subjects

Jean-François Raskin

Publications and source records attributed to Jean-François Raskin.

At least 91 records · Page 5Linked to original sources

arXiv2015

Looking at Mean-Payoff through Foggy Windows

Mean-payoff games (MPGs) are infinite duration two-player zero-sum games played on weighted graphs. Under the hypothesis of perfect information, they admit memoryless optimal strategies for both players and can be solved in NP-intersect-coNP. MPGs are suitable quantitative models for open reactive systems. However, in this context the assumption of perfect information is not always realistic. For the partial-observation case, the problem that asks if the first player has an observation-based winning strategy that enforces a given threshold on the mean-payoff, is undecidable. In this paper, we study the window mean-payoff objectives that were introduced recently as an alternative to the classical mean-payoff objectives. We show that, in sharp contrast to the classical mean-payoff objectives, some of the window mean-payoff objectives are decidable in games with partial-observation.

cs.LO↗

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

Multiple-Environment Markov Decision Processes

We introduce Multi-Environment Markov Decision Processes (MEMDPs) which are MDPs with a set of probabilistic transition functions. The goal in a MEMDP is to synthesize a single controller with guaranteed performances against all environments even though the environment is unknown a priori. While MEMDPs can be seen as a special class of partially observable MDPs, we show that several verification problems that are undecidable for partially observable MDPs, are decidable for MEMDPs and sometimes have even efficient solutions.

cs.LO↗

arXiv2014

Variations on the Stochastic Shortest Path Problem

In this invited contribution, we revisit the stochastic shortest path problem, and show how recent results allow one to improve over the classical solutions: we present algorithms to synthesize strategies with multiple guarantees on the distribution of the length of paths reaching a given target, rather than simply minimizing its expected value. The concepts and algorithms that we propose here are applications of more general results that have been obtained recently for Markov decision processes and that are described in a series of recent papers.

cs.LO↗

arXiv2014

Strategy Synthesis for Multi-dimensional Quantitative Objectives

Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express $ω$-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.

cs.GT↗

arXiv2014

Looking at Mean-Payoff and Total-Payoff through Windows

We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, two classical quantitative objectives. While for single-dimensional games the complexity and memory bounds for both objectives coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i) if the window size is polynomial, deciding the winner takes polynomial time, and (ii) the existence of a bounded window can be decided in NP $\cap$ coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i) the problem with fixed window size is EXPTIME-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window.

cs.GT↗

arXiv2014

AbsSynthe: abstract synthesis from succinct safety specifications

In this paper, we describe a synthesis algorithm for safety specifications described as circuits. Our algorithm is based on fixpoint computations, abstraction and refinement, it uses binary decision diagrams as symbolic data structure. We evaluate our tool on the benchmarks provided by the organizers of the synthesis competition organized within the SYNT'14 workshop.

cs.LO↗

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

Quantitative games with interval objectives

Traditionally quantitative games such as mean-payoff games and discount sum games have two players -- one trying to maximize the payoff, the other trying to minimize it. The associated decision problem, "Can Eve (the maximizer) achieve, for example, a positive payoff?" can be thought of as one player trying to attain a payoff in the interval $(0,\infty)$. In this paper we consider the more general problem of determining if a player can attain a payoff in a finite union of arbitrary intervals for various payoff functions (liminf, mean-payoff, discount sum, total sum). In particular this includes the interesting exact-value problem, "Can Eve achieve a payoff of exactly (e.g.) 0?"

cs.LO↗

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↗

arXiv2014

The Complexity of Admissibility in Omega-Regular Games

Iterated admissibility is a well-known and important concept in classical game theory, e.g. to determine rational behaviors in multi-player matrix games. As recently shown by Berwanger, this concept can be soundly extended to infinite games played on graphs with omega-regular objectives. In this paper, we study the algorithmic properties of this concept for such games. We settle the exact complexity of natural decision problems on the set of strategies that survive iterated elimination of dominated strategies. As a byproduct of our construction, we obtain automata which recognize all the possible outcomes of such strategies.

cs.GT↗

arXiv2013

Doomsday Equilibria for Omega-Regular Games

Two-player games on graphs provide the theoretical frame- work for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games. In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated. We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of omega-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.

cs.GT↗

arXiv2013

ω-Petri nets

We introduce ω-Petri nets (ωPN), an extension of plain Petri nets with ω-labeled input and output arcs, that is well-suited to analyse parametric concurrent systems with dynamic thread creation. Most techniques (such as the Karp and Miller tree or the Rackoff technique) that have been proposed in the setting of plain Petri nets do not apply directly to ωPN because ωPN define transition systems that have infinite branching. This motivates a thorough analysis of the computational aspects of ωPN. We show that an ωPN can be turned into an plain Petri net that allows to recover the reachability set of the ωPN, but that does not preserve termination. This yields complexity bounds for the reachability, (place) boundedness and coverability problems on ωPN. We provide a practical algorithm to compute a coverability set of the ωPN and to decide termination by adapting the classical Karp and Miller tree construction. We also adapt the Rackoff technique to ωPN, to obtain the exact complexity of the termination problem. Finally, we consider the extension of ωPN with reset and transfer arcs, and show how this extension impacts the decidability and complexity of the aforementioned problems.

cs.LO↗

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

Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints

In this paper, we study thetime-bounded reachability problem for rectangular hybrid automata with non-negative rates (RHA+). This problem was recently shown to be decidable [Brihaye et al, ICALP11] (even though the unbounded reachability problem for even very simple classes of hybrid automata is well-known to be undecidable). However, [Brihaye et al, ICALP11] does not provide a precise characterisation of the complexity of the time-bounded reachability problem. The contribution of the present paper is threefold. First, we provide a new NExpTime algorithm to solve the timed-bounded reachability problem on RHA+. This algorithm improves on the one of [Brihaye et al, ICALP11] by at least one exponential. Second, we show that this new algorithm is optimal, by establishing a matching lower bound: time-bounded reachability for RHA+ is therefore NExpTime-complete. Third, we extend these results in a practical direction, by showing that we can effectively compute fixpoints that characterise the sets of states that are reachable (resp. co-reachable) within T time units from a given starting state.

cs.LO↗

arXiv2012

Queue-Dispatch Asynchronous Systems

To make the development of efficient multi-core applications easier, libraries, such as Grand Central Dispatch, have been proposed. When using such a library, the programmer writes so-called blocks, which are chunks of codes, and dispatches them, using synchronous or asynchronous calls, to several types of waiting queues. A scheduler is then responsible for dispatching those blocks on the available cores. Blocks can synchronize via a global memory. In this paper, we propose Queue-Dispatch Asynchronous Systems as a mathematical model that faithfully formalizes the synchronization mechanisms and the behavior of the scheduler in those systems. We study in detail their relationships to classical formalisms such as pushdown systems, Petri nets, fifo systems, and counter systems. Our main technical contributions are precise worst-case complexity results for the Parikh coverability problem for several subclasses of our model.

cs.LO↗

arXiv2011

Event-Clock Automata: From Theory to Practice

Event clock automata (ECA) are a model for timed languages that has been introduced by Alur, Fix and Henzinger as an alternative to timed automata, with better theoretical properties (for instance, ECA are determinizable while timed automata are not). In this paper, we revisit and extend the theory of ECA. We first prove that no finite time abstract language equivalence exists for ECA, thereby disproving a claim in the original work on ECA. This means in particular that regions do not form a time abstract bisimulation. Nevertheless, we show that regions can still be used to build a finite automaton recognizing the untimed language of an ECA. Then, we extend the classical notions of zones and DBMs to let them handle event clocks instead of plain clocks (as in timed automata) by introducing event zones and Event DBMs (EDBMs). We discuss algorithms to handle event zones represented as EDBMs, as well as (semi-) algorithms based on EDBMs to decide language emptiness of ECA.

cs.LO↗