Showing 51–100 of 118 results for author: Raskin, J

Parameterized complexity of games with monotonically ordered ω-regular objectives

Authors: Véronique Bruyère, Quentin Hautem, Jean-François Raskin

Abstract: 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 ac… ▽ More 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. △ Less

Submitted 2 July, 2018; v1 submitted 19 July, 2017; originally announced July 2017.

Decidable Weighted Expressions with Presburger Combinators

Authors: Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin

Abstract: In this paper, we investigate the expressive power and the algorithmic properties of weighted expressions, which define functions from finite words to integers. First, we consider a slight extension of an expression formalism, introduced by Chatterjee. et. al. in the context of infinite words, by which to combine values given by unambiguous (max,+)-automata, using Presburger arithmetic. We show th… ▽ More In this paper, we investigate the expressive power and the algorithmic properties of weighted expressions, which define functions from finite words to integers. First, we consider a slight extension of an expression formalism, introduced by Chatterjee. et. al. in the context of infinite words, by which to combine values given by unambiguous (max,+)-automata, using Presburger arithmetic. We show that important decision problems such as emptiness, universality and comparison are PSpace-c for these expressions. We then investigate the extension of these expressions with Kleene star. This allows to iterate an expression over smaller fragments of the input word, and to combine the results by taking their iterated sum. The decision problems turn out to be undecidable, but we introduce the decidable and still expressive class of synchronised expressions. △ Less

Submitted 27 June, 2017; originally announced June 2017.

Comments: FCT2017 Acceptance

Admissibility in Concurrent Games

Authors: Nicolas Basset, Gilles Geeraerts, Jean-François Raskin, Ocan Sankur

Abstract: In this paper, we study the notion of admissibility for randomised strategies in concurrent games. Intuitively, an admissible strategy is one where the player plays `as well as possible', because there is no other strategy that dominates it, i.e., that wins (almost surely) against a super set of adversarial strategies. We prove that admissible strategies always exist in concurrent games, and we ch… ▽ More In this paper, we study the notion of admissibility for randomised strategies in concurrent games. Intuitively, an admissible strategy is one where the player plays `as well as possible', because there is no other strategy that dominates it, i.e., that wins (almost surely) against a super set of adversarial strategies. We prove that admissible strategies always exist in concurrent games, and we characterise them precisely. Then, when the objectives of the players are omega-regular, we show how to perform assume-admissible synthesis, i.e., how to compute admissible strategies that win (almost surely) under the hypothesis that the other players play admissible △ Less

Submitted 21 February, 2017; originally announced February 2017.

Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

Authors: Raphaël Berthon, Mickael Randour, Jean-François Raskin

Abstract: The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [BFRR14]: it aims at building system controllers that provide strict worst-case performance guarantees against an antagonistic environment while ensuring higher expected performance against a stochastic model of the environment. Our work extends the framework of [BFRR14] and follow-up papers, which focused on quantit… ▽ More The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [BFRR14]: it aims at building system controllers that provide strict worst-case performance guarantees against an antagonistic environment while ensuring higher expected performance against a stochastic model of the environment. Our work extends the framework of [BFRR14] and follow-up papers, which focused on quantitative objectives, by addressing the case of $ω$-regular conditions encoded as parity objectives, a natural way to represent functional requirements of systems. We build strategies that satisfy a main parity objective on all plays, while ensuring a secondary one with sufficient probability. This setting raises new challenges in comparison to quantitative objectives, as one cannot easily mix different strategies without endangering the functional properties of the system. We establish that, for all variants of this problem, deciding the existence of a strategy lies in ${\sf NP} \cap {\sf coNP}$, the same complexity class as classical parity games. Hence, our framework provides additional modeling power while staying in the same complexity class. [BFRR14] Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In Ernst W. Mayr and Natacha Portier, editors, 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, March 5-8, 2014, Lyon, France, volume 25 of LIPIcs, pages 199-213. Schloss Dagstuhl - Leibniz - Zentrum fuer Informatik, 2014. △ Less

Submitted 27 April, 2017; v1 submitted 17 February, 2017; originally announced February 2017.

Comments: Full version of ICALP 2017 paper

From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata

Authors: Javier Esparza, Jan Křetínský, Jean-François Raskin, Salomon Sickert

Abstract: Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formu… ▽ More Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Büchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, \enquote{Safraless} LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition. △ Less

Submitted 21 January, 2017; originally announced January 2017.

On Delay and Regret Determinization of Max-Plus Automata

Authors: Emmanuel Filiot, Ismaël Jecker, Nathan Lhote, Guillermo A. Pérez, Jean-François Raskin

Abstract: Decidability of the determinization problem for weighted automata over the semiring $(\mathbb{Z} \cup {-\infty}, \max, +)$, WA for short, is a long-standing open question. We propose two ways of approaching it by constraining the search space of deterministic WA: k-delay and r-regret. A WA N is k-delay determinizable if there exists a deterministic automaton D that defines the same function as N a… ▽ More Decidability of the determinization problem for weighted automata over the semiring $(\mathbb{Z} \cup {-\infty}, \max, +)$, WA for short, is a long-standing open question. We propose two ways of approaching it by constraining the search space of deterministic WA: k-delay and r-regret. A WA N is k-delay determinizable if there exists a deterministic automaton D that defines the same function as N and for all words α in the language of N, the accepting run of D on α is always at most k-away from a maximal accepting run of N on α. That is, along all prefixes of the same length, the absolute difference between the running sums of weights of the two runs is at most k. A WA N is r-regret determinizable if for all words α in its language, its non-determinism can be resolved on the fly to construct a run of N such that the absolute difference between its value and the value assigned to α by N is at most r. We show that a WA is determinizable if and only if it is k-delay determinizable for some k. Hence deciding the existence of some k is as difficult as the general determinization problem. When k and r are given as input, the k-delay and r-regret determinization problems are shown to be EXPtime-complete. We also show that determining whether a WA is r-regret determinizable for some r is in EXPtime. △ Less

Submitted 3 March, 2017; v1 submitted 11 January, 2017; originally announced January 2017.

On the existence of weak subgame perfect equilibria

Authors: Véronique Bruyère, Stéphane Le Roux, Arno Pauly, Jean-François Raskin

Abstract: 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 deviat… ▽ More 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. △ Less

Submitted 5 October, 2017; v1 submitted 5 December, 2016; originally announced December 2016.

Comments: 28 pages

MSC Class: 91A18

Optimizing Expectation with Guarantees in POMDPs (Technical Report)

Authors: Krishnendu Chatterjee, Petr Novotný, Guillermo A. Pérez, Jean-François Raskin, Đorđe Žikelić

Abstract: A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability t… ▽ More A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability to ensure that the payoff is at least a given threshold, but these approaches do not consider any optimization beyond satisfying this threshold constraint. In this work we go beyond both the "expectation" and "threshold" approaches and consider a "guaranteed payoff optimization (GPO)" problem for POMDPs, where we are given a threshold $t$ and the objective is to find a policy $σ$ such that a) each possible outcome of $σ$ yields a discounted-sum payoff of at least $t$, and b) the expected discounted-sum payoff of $σ$ is optimal (or near-optimal) among all policies satisfying a). We present a practical approach to tackle the GPO problem and evaluate it on standard POMDP benchmarks. △ Less

Submitted 29 January, 2017; v1 submitted 26 November, 2016; originally announced November 2016.

Admissibility in Quantitative Graph Games

Authors: Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, Ocan Sankur

Abstract: Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First, we show that, un- der the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the no- tion… ▽ More Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First, we show that, un- der the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the no- tion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide relevant verification and synthesis problems. △ Less

Submitted 26 November, 2016; originally announced November 2016.

Comments: This is the full version of an article that will be published in FSTTCS'16

ACM Class: F.1.1; D.2.4

Minkowski games

Authors: Stéphane Le Roux, Arno Pauly, Jean-François Raskin

Abstract: We introduce and study Minkowski games. These are two player games, where the players take turns to chose positions in $\mathbb{R}^d$ based on some rules. Variants include boundedness games, where one player wants to keep the positions bounded, and the other wants to escape to infinity; as well as safety games, where one player wants to stay within a prescribed set, while the other wants to leave… ▽ More We introduce and study Minkowski games. These are two player games, where the players take turns to chose positions in $\mathbb{R}^d$ based on some rules. Variants include boundedness games, where one player wants to keep the positions bounded, and the other wants to escape to infinity; as well as safety games, where one player wants to stay within a prescribed set, while the other wants to leave it. We provide some general characterizations of which player can win such games, and explore the computational complexity of the associated decision problems. A natural representation of boundedness games yields coNP-completeness, whereas the safety games are undecidable. △ Less

Submitted 25 November, 2016; v1 submitted 22 September, 2016; originally announced September 2016.

MSC Class: 91A44; 68Q25; 68U05

The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results

Authors: Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker

Abstract: We report on the benchmarks, participants and results of the third reactive synthesis competition(SYNTCOMP 2016). The benchmark library of SYNTCOMP 2016 has been extended to benchmarks in the new LTL-based temporal logic synthesis format (TLSF), and 2 new sets of benchmarks for the existing AIGER-based format for safety specifications. The participants of SYNTCOMP 2016 can be separated according t… ▽ More We report on the benchmarks, participants and results of the third reactive synthesis competition(SYNTCOMP 2016). The benchmark library of SYNTCOMP 2016 has been extended to benchmarks in the new LTL-based temporal logic synthesis format (TLSF), and 2 new sets of benchmarks for the existing AIGER-based format for safety specifications. The participants of SYNTCOMP 2016 can be separated according to these two classes of specifications, and we give an overview of the 6 tools that entered the competition in the AIGER-based track, and the 3 participants that entered the TLSF-based track. We briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2016. Finally, we present and analyze the results of our experimental evaluation, including a comparison to participants of previous competitions and a legacy tool. △ Less

Submitted 23 November, 2016; v1 submitted 2 September, 2016; originally announced September 2016.

Comments: In Proceedings SYNT 2016, arXiv:1611.07178

Journal ref: EPTCS 229, 2016, pp. 149-177

Compositional Algorithms for Succinct Safety Games

Authors: Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, Ocan Sankur

Abstract: We study the synthesis of circuits for succinct safety specifications given in the AIG format. We show how AIG safety specifications can be decomposed automatically into sub specifications. Then we propose symbolic compositional algorithms to solve the synthesis problem compositionally starting for the sub-specifications. We have evaluated the compositional algorithms on a set of benchmarks includ… ▽ More We study the synthesis of circuits for succinct safety specifications given in the AIG format. We show how AIG safety specifications can be decomposed automatically into sub specifications. Then we propose symbolic compositional algorithms to solve the synthesis problem compositionally starting for the sub-specifications. We have evaluated the compositional algorithms on a set of benchmarks including those proposed for the first synthesis competition organised in 2014 by the Synthesis Workshop affiliated to the CAV conference. We show that a large number of benchmarks can be decomposed automatically and solved more efficiently with the compositional algorithms that we propose in this paper. △ Less

Submitted 2 February, 2016; originally announced February 2016.

Comments: In Proceedings SYNT 2015, arXiv:1602.00786

ACM Class: F.3.1,B.1.2,B.6.3

Journal ref: EPTCS 202, 2016, pp. 98-111

The Second Reactive Synthesis Competition (SYNTCOMP 2015)

Authors: Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker

Abstract: We report on the design and results of the second reactive synthesis competition (SYNTCOMP 2015). We describe our extended benchmark library, with 6 completely new sets of benchmarks, and additional challenging instances for 4 of the benchmark sets that were already used in SYNTCOMP 2014. To enhance the analysis of experimental results, we introduce an extension of our benchmark format with meta-i… ▽ More We report on the design and results of the second reactive synthesis competition (SYNTCOMP 2015). We describe our extended benchmark library, with 6 completely new sets of benchmarks, and additional challenging instances for 4 of the benchmark sets that were already used in SYNTCOMP 2014. To enhance the analysis of experimental results, we introduce an extension of our benchmark format with meta-information, including a difficulty rating and a reference size for solutions. Tools are evaluated on a set of 250 benchmarks, selected to provide a good coverage of benchmarks from all classes and difficulties. We report on changes of the evaluation scheme and the experimental setup. Finally, we describe the entrants into SYNTCOMP 2015, as well as the results of our experimental evaluation. In our analysis, we emphasize progress over the tools that participated last year. △ Less

Submitted 2 February, 2016; originally announced February 2016.

Comments: In Proceedings SYNT 2015, arXiv:1602.00786

Journal ref: EPTCS 202, 2016, pp. 27-57

Non-Zero Sum Games for Reactive Synthesis

Authors: Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, Mathieu Sassolas

Abstract: In this invited contribution, we summarize new solution concepts useful for the synthesis of reactive systems that we have introduced in several recent publications. These solution concepts are developed in the context of non-zero sum games played on graphs. They are part of the contributions obtained in the inVEST project funded by the European Research Council. In this invited contribution, we summarize new solution concepts useful for the synthesis of reactive systems that we have introduced in several recent publications. These solution concepts are developed in the context of non-zero sum games played on graphs. They are part of the contributions obtained in the inVEST project funded by the European Research Council. △ Less

Submitted 17 December, 2015; originally announced December 2015.

Comments: LATA'16 invited paper

On the complexity of heterogeneous multidimensional quantitative games

Authors: Véronique Bruyère, Quentin Hautem, Jean-François Raskin

Abstract: 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,… ▽ More 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. △ Less

Submitted 21 June, 2016; v1 submitted 26 November, 2015; originally announced November 2015.

Minimizing Regret in Discounted-Sum Games

Authors: Paul Hunter, Guillermo A. Pérez, Jean-François Raskin

Abstract: In this paper, we study the problem of minimizing regret in discounted-sum games played on weighted game graphs. We give algorithms for the general problem of computing the minimal regret of the controller (Eve) as well as several variants depending on which strategies the environment (Adam) is permitted to use. We also consider the problem of synthesizing regret-free strategies for Eve in each of… ▽ More In this paper, we study the problem of minimizing regret in discounted-sum games played on weighted game graphs. We give algorithms for the general problem of computing the minimal regret of the controller (Eve) as well as several variants depending on which strategies the environment (Adam) is permitted to use. We also consider the problem of synthesizing regret-free strategies for Eve in each of these scenarios. △ Less

Submitted 4 May, 2018; v1 submitted 2 November, 2015; originally announced November 2015.

Comments: arXiv admin note: text overlap with arXiv:1504.01708; some typos have been removed in the proof of simple strategies being sufficient to minimize regret against any adversary

ACM Class: F.1.1; D.2.4

Assume-Admissible Synthesis

Authors: Romain Brenguier, Jean-François Raskin, Ocan Sankur

Abstract: In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. It is based on the notion of admissible strategies. We compare our novel rule with previous rules defined in the literature, and we show that contrary to the previous proposals, our rule defines sets of solutions which are rectangular. This pr… ▽ More In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. It is based on the notion of admissible strategies. We compare our novel rule with previous rules defined in the literature, and we show that contrary to the previous proposals, our rule defines sets of solutions which are rectangular. This property leads to solutions which are robust and resilient. We provide algorithms with optimal complexity and also an abstraction framework. △ Less

Submitted 2 July, 2015; originally announced July 2015.

Comments: 31 pages

ACM Class: D.2.4; F.3.1; I.2.2

The First Reactive Synthesis Competition (SYNTCOMP 2014)

Authors: Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker

Abstract: We introduce the reactive synthesis competition (SYNTCOMP), a long-term effort intended to stimulate and guide advances in the design and application of synthesis procedures for reactive systems. The first iteration of SYNTCOMP is based on the controller synthesis problem for finite-state systems and safety specifications. We provide an overview of this problem and existing approaches to solve it,… ▽ More We introduce the reactive synthesis competition (SYNTCOMP), a long-term effort intended to stimulate and guide advances in the design and application of synthesis procedures for reactive systems. The first iteration of SYNTCOMP is based on the controller synthesis problem for finite-state systems and safety specifications. We provide an overview of this problem and existing approaches to solve it, and report on the design and results of the first SYNTCOMP. This includes the definition of the benchmark format, the collection of benchmarks, the rules of the competition, and the five synthesis tools that participated. We present and analyze the results of the competition and draw conclusions on the state of the art. Finally, we give an outlook on future directions of SYNTCOMP. △ Less

Submitted 13 April, 2016; v1 submitted 29 June, 2015; originally announced June 2015.

Comments: 24 pages, published in STTT

Journal ref: International Journal on Software Tools for Technology Transfer, Online First, 2016, pp 1-24

Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives

Authors: Lorenzo Clemente, Jean-François Raskin

Abstract: The beyond worst-case threshold problem (BWC), recently introduced by Bruyère et al., asks given a quantitative game graph for the synthesis of a strategy that i) enforces some minimal level of performance against any adversary, and ii) achieves a good expectation against a stochastic model of the adversary. They solved the BWC problem for finite-memory strategies and unidimensional mean-payoff ob… ▽ More The beyond worst-case threshold problem (BWC), recently introduced by Bruyère et al., asks given a quantitative game graph for the synthesis of a strategy that i) enforces some minimal level of performance against any adversary, and ii) achieves a good expectation against a stochastic model of the adversary. They solved the BWC problem for finite-memory strategies and unidimensional mean-payoff objectives and they showed membership of the problem in NP$\cap$coNP. They also noted that infinite-memory strategies are more powerful than finite-memory ones, but the respective threshold problem was left open. We extend these results in several directions. First, we consider multidimensional mean-payoff objectives. Second, we study both finite-memory and infinite-memory strategies. We show that the multidimensional BWC problem is coNP-complete in both cases. Third, in the special case when the worst-case objective is unidimensional (but the expectation objective is still multidimensional) we show that the complexity decreases to NP$\cap$coNP. This solves the infinite-memory threshold problem left open by Bruyère et al., and this complexity cannot be improved without improving the currently known complexity of classical mean-payoff games. Finally, we introduce a natural relaxation of the BWC problem, the beyond almost-sure threshold problem (BAS), which asks for the synthesis of a strategy that ensures some minimal level of performance with probability one and a good expectation against the stochastic model of the adversary. We show that the multidimensional BAS threshold problem is solvable in P. △ Less

Submitted 21 November, 2017; v1 submitted 30 April, 2015; originally announced April 2015.

Comments: Technical report a paper accepted to LICS'15

Looking at Mean-Payoff through Foggy Windows

Authors: Paul Hunter, Guillermo A. Pérez, Jean-François Raskin

Abstract: 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… ▽ More 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. △ Less

Submitted 12 April, 2015; originally announced April 2015.

Reactive Synthesis Without Regret

Authors: Paul Hunter, Guillermo A. Pérez, Jean-François Raskin

Abstract: Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that m… ▽ More Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies. We also establish relations between the latter version and other problems studied in the literature. △ Less

Submitted 28 October, 2021; v1 submitted 7 April, 2015; originally announced April 2015.

Comments: Fixed inaccuracies spotted by Udi Boker and Karoliina Lehtinen and improved the presentation of a few proofs

ACM Class: F.1.1

Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability

Authors: Thomas Brihaye, Véronique Bruyère, Noémie Meunier, Jean-François Raskin

Abstract: 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. ve… ▽ More 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. △ Less

Submitted 10 April, 2015; v1 submitted 7 April, 2015; originally announced April 2015.

Variations on the Stochastic Shortest Path Problem

Authors: Mickael Randour, Jean-François Raskin, Ocan Sankur

Abstract: 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… ▽ More 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. △ Less

Submitted 4 November, 2014; originally announced November 2014.

Comments: Invited paper for VMCAI 2015

Percentile Queries in Multi-Dimensional Markov Decision Processes

Authors: Mickael Randour, Jean-François Raskin, Ocan Sankur

Abstract: Markov decision processes (MDPs) with multi-dimensional weights are useful to analyze systems with multiple objectives that may be conflicting and require the analysis of trade-offs. We study the complexity of percentile queries in such MDPs and give algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function $f$, thr… ▽ More Markov decision processes (MDPs) with multi-dimensional weights are useful to analyze systems with multiple objectives that may be conflicting and require the analysis of trade-offs. We study the complexity of percentile queries in such MDPs and give algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function $f$, thresholds $v_i$ (one per dimension), and probability thresholds $α_i$, we show how to compute a single strategy to enforce that for all dimensions $i$, the probability of outcomes $ρ$ satisfying $f_i(ρ) \geq v_i$ is at least $α_i$. We consider classical quantitative payoffs from the literature (sup, inf, lim sup, lim inf, mean-payoff, truncated sum, discounted sum). Our work extends to the quantitative case the multi-objective model checking problem studied by Etessami et al. in unweighted MDPs. △ Less

Submitted 7 December, 2016; v1 submitted 17 October, 2014; originally announced October 2014.

Comments: Extended version of CAV 2015 paper

AbsSynthe: abstract synthesis from succinct safety specifications

Authors: Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, Ocan Sankur

Abstract: 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. 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. △ Less

Submitted 21 July, 2014; originally announced July 2014.

Comments: In Proceedings SYNT 2014, arXiv:1407.4937

ACM Class: F.3.1,B.1.2,B.6.3

Journal ref: EPTCS 157, 2014, pp. 100-116

Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes

Authors: Aaron Bohy, Véronique Bruyère, Jean-François Raskin

Abstract: 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 combin… ▽ More 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. △ Less

Submitted 21 July, 2014; originally announced July 2014.

Comments: In Proceedings SYNT 2014, arXiv:1407.4937

Journal ref: EPTCS 157, 2014, pp. 51-67

Multiple-Environment Markov Decision Processes

Authors: Jean-François Raskin, Ocan Sankur

Abstract: 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 p… ▽ More 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. △ Less

Submitted 3 December, 2014; v1 submitted 19 May, 2014; originally announced May 2014.

Quantitative games with interval objectives

Authors: Paul Hunter, Jean-François Raskin

Abstract: 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… ▽ More 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?" △ Less

Submitted 18 April, 2014; originally announced April 2014.

Comments: Full version of CONCUR submission

ACM Class: F.1.1

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

Authors: Véronique Bruyère, Emmanuel Filiot, Mickael Randour, Jean-François Raskin

Abstract: 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 t… ▽ More 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. △ Less

Submitted 3 April, 2014; originally announced April 2014.

Comments: In Proceedings SR 2014, arXiv:1404.0414

Journal ref: EPTCS 146, 2014, pp. 1-8

Using top graphene layer as sacrificial protection during dielectric atomic layer deposition

Authors: Xiaohui Tang, Nicolas Reckinger, Olivier Poncelet, Pierre Louette, Jean-François Colomer, Jean-Pierre Raskin, Benoit Hackens, Laurent A. Francis

Abstract: We investigate the structural damage of graphene underlying dielectrics (HfO2 and Al2O3) by remote plasma-enhanced atomic layer deposition (PE-ALD). Dielectric film is grown on bilayer graphene without inducing significant damage to the bottom graphene layer. Based on Raman spectra, we demonstrate that the bottom graphene layer has the salient features of single layer graphene. During the initial… ▽ More We investigate the structural damage of graphene underlying dielectrics (HfO2 and Al2O3) by remote plasma-enhanced atomic layer deposition (PE-ALD). Dielectric film is grown on bilayer graphene without inducing significant damage to the bottom graphene layer. Based on Raman spectra, we demonstrate that the bottom graphene layer has the salient features of single layer graphene. During the initial half-cycle PE-ALD, the upper graphene layer reacts with the metal precursor, forming uniform nucleation islands or an active metallic carbide layer. After monolayer dielectric coverage, the bottom graphene layer has additional protection. The upper graphene layer serves as a sacrificial layer, which not only promotes the adhesion of dielectric on graphene, but also protects the lattice symmetry of the bottom graphene layer. Our results indicate that bilayer graphene allows for controlling/limiting the degree of defect during the ALD of dielectrics and could be a good starting material for building filed effect transistors and sensing devices. △ Less

Submitted 15 March, 2014; originally announced March 2014.

Secure Equilibria in Weighted Games

Authors: Véronique Bruyère, Noémie Meunier, Jean-François Raskin

Abstract: 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 weight… ▽ More 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. △ Less

Submitted 30 September, 2016; v1 submitted 17 February, 2014; originally announced February 2014.

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

Authors: Aaron Bohy, Véronique Bruyère, Jean-François Raskin

Abstract: 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 combin… ▽ More 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. △ Less

Submitted 20 June, 2014; v1 submitted 5 February, 2014; originally announced February 2014.

Doomsday Equilibria for Omega-Regular Games

Authors: Krishnendu Chatterjee, Laurent Doyen, Emmanuel Filiot, Jean-François Raskin

Abstract: 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… ▽ More 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. △ Less

Submitted 13 November, 2013; originally announced November 2013.

Mean-payoff Games with Partial Observation

Authors: Paul Hunter, Arno Pauly, Guillermo A. Pérez, Jean-François Raskin

Abstract: Mean-payoff games are important quantitative models for open reactive systems. They have been widely studied as games of full observation. In this paper we investigate the algorithmic properties of several sub-classes of mean-payoff games where the players have asymmetric information about the state of the game. These games are in general undecidable and not determined according to the classical d… ▽ More Mean-payoff games are important quantitative models for open reactive systems. They have been widely studied as games of full observation. In this paper we investigate the algorithmic properties of several sub-classes of mean-payoff games where the players have asymmetric information about the state of the game. These games are in general undecidable and not determined according to the classical definition. We show that such games are determined under a more general notion of winning strategy. We also consider mean-payoff games where the winner can be determined by the winner of a finite cycle-forming game. This yields several decidable classes of mean-payoff games of asymmetric information that require only finite-memory strategies, including a generalization of full-observation games where positional strategies are sufficient. We give an exponential time algorithm for determining the winner of the latter. △ Less

Submitted 8 October, 2017; v1 submitted 21 September, 2013; originally announced September 2013.

Comments: Fixes confusing/wrong comments in some proofs and misleading figures

ACM Class: F.1.1

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

Authors: Véronique Bruyère, Emmanuel Filiot, Mickael Randour, Jean-François Raskin

Abstract: 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 env… ▽ More 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. △ Less

Submitted 30 October, 2015; v1 submitted 21 September, 2013; originally announced September 2013.

Comments: Extended version. Journal version published in Information and Computation, conference version published in STACS 2014

The Complexity of Admissibility in Omega-Regular Games

Authors: Romain Brenguier, Jean-François Raskin, Mathieu Sassolas

Abstract: 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 complexi… ▽ More 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. △ Less

Submitted 23 January, 2014; v1 submitted 5 April, 2013; originally announced April 2013.

Self-Formation of Sub-10-nm Nanogaps by Silicidation for Resistive Switch in Air

Authors: Xiaohui Tang, Laurent A. Francis, Constantin Augustin Dutu, Nicolas Reckinger, Jean-Pierre Raskin

Abstract: We developed a simple and reliable method for the fabrication of sub-10-nm wide nanogaps. The self-formed nanogap is based on the stoichiometric solid-state reaction between metal and Si atoms during silicidation process. The nanogap width is deter- mined by the metal layer thickness. Our proposed method produces nanogaps either symmetric or asymmetric electrodes, as well as, multiple nanogaps wit… ▽ More We developed a simple and reliable method for the fabrication of sub-10-nm wide nanogaps. The self-formed nanogap is based on the stoichiometric solid-state reaction between metal and Si atoms during silicidation process. The nanogap width is deter- mined by the metal layer thickness. Our proposed method produces nanogaps either symmetric or asymmetric electrodes, as well as, multiple nanogaps within one unique process step for application to complex circuits. Therefore, this method provides high throughput and it is suitable for large-scale production. To demonstrate the feasibil- ity of the proposed fabrication method, nanogap resistive switches have been built and characterized. They exhibit a pronounced hysteresis with up to 103 on/off conductance ratios in air. Our results indicate that the voltages for initially electroforming the de- vice to the switch state are determinated by the nanogap sizes. However, the set and reset voltages of the device do not strongly dependent on the nanogap widths. These phenomena could be helpful to understand how the resistive switching is established. △ Less

Submitted 19 March, 2013; originally announced March 2013.

Comments: 26 pages, 6 figures, a research report

Looking at Mean-Payoff and Total-Payoff through Windows

Authors: Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, Jean-François Raskin

Abstract: 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.… ▽ More 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. △ Less

Submitted 3 November, 2014; v1 submitted 18 February, 2013; originally announced February 2013.

Comments: Extended version of ATVA 2013 version. Full version to appear in Information and Computation

Twisted bi-layer graphene: microscopic rainbows

Authors: J. Campos-Delgado, G. Algara-Siller, C. N. Santos, U. Kaiser, J. -P. Raskin

Abstract: Twisted bi-layer graphene (tBLG) has recently attracted interest due to the peculiar electrical properties that arise from its random rotational configurations. Our experiments on CVD-grown graphene from Cu foil and transferred onto Si substrates, with an oxide layer of 100 nm, reveal naturally-produced bi-layer graphene patches which present different colorations when shined with white light. In… ▽ More Twisted bi-layer graphene (tBLG) has recently attracted interest due to the peculiar electrical properties that arise from its random rotational configurations. Our experiments on CVD-grown graphene from Cu foil and transferred onto Si substrates, with an oxide layer of 100 nm, reveal naturally-produced bi-layer graphene patches which present different colorations when shined with white light. In particular yellow-, pink- and blue- colored areas are evidenced. Combining optical microscopy, Raman spectroscopy and transmission electron microscopy we have been able to assign these colorations to ranges of rotational angles between the two graphene layers. Optical contrast simulations have been carried out, proving that the observation of the different colorations is due to the angle-dependent electronic properties of tBLG combined with the reflection that results from the layered structure tBLG / 100 nm-thick SiO2 / Si. Our results could lead the way to an easy selective identification of bi-layer graphene merely through the observation on an optical microscope. △ Less

Submitted 16 April, 2013; v1 submitted 16 February, 2013; originally announced February 2013.

Comments: This paper has been withdrawn by the author due to copyright incompatibility with the journal of final publication

ω-Petri nets

Authors: Gilles Geeraerts, Alexander Heußner, M. Praveen, Jean-François Raskin

Abstract: 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 tha… ▽ More 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. △ Less

Submitted 28 January, 2013; originally announced January 2013.

Comments: 37 pages, 6 figures, submitted

Raman-scattering study of the phonon dispersion in twisted bi-layer graphene

Authors: J. Campos-Delgado, L. G. Cançado, C. A. Achete, A. Jorio, J. -P. Raskin

Abstract: Bi-layer graphene with a twist angle θ between the layers generates a superlattice structure known as Moiré pattern. This superlattice provides a θ-dependent q wavevector that activates phonons in the interior of the Brillouin zone. Here we show that this superlattice-induced Raman scattering can be used to probe the phonon dispersion in twisted bi-layer graphene (tBLG). The effect reported here i… ▽ More Bi-layer graphene with a twist angle θ between the layers generates a superlattice structure known as Moiré pattern. This superlattice provides a θ-dependent q wavevector that activates phonons in the interior of the Brillouin zone. Here we show that this superlattice-induced Raman scattering can be used to probe the phonon dispersion in twisted bi-layer graphene (tBLG). The effect reported here is different from the broadly studied double-resonance in graphene-related materials in many aspects, and despite the absence of stacking order in tBLG, layer breathing vibrations (namely ZO' phonons) are observed. △ Less

Submitted 28 March, 2013; v1 submitted 16 January, 2013; originally announced January 2013.

Comments: 18 pages, 4 figures, research article

Journal ref: Nano Research (2013)

Direct growth of graphitic carbon on Si(111)

Authors: Pham Thanh Trung, Frederic Joucken, Jessica Campos-Delgado, Jean-Pierre Raskin, Benoit Hackens, Robert Sporken

Abstract: Appropriate conditions for direct growth of graphitic films on Si(111) 7$\times$7 are investigated. The structural and electronic properties of the samples are studied by Auger Electron Spectroscopy (AES), X-ray Photoemission Spectroscopy (XPS), Low Energy Electron Diffraction (LEED), Raman spectroscopy and Scanning Tunneling Microscopy (STM). In particular, we present STM images of a carbon honey… ▽ More Appropriate conditions for direct growth of graphitic films on Si(111) 7$\times$7 are investigated. The structural and electronic properties of the samples are studied by Auger Electron Spectroscopy (AES), X-ray Photoemission Spectroscopy (XPS), Low Energy Electron Diffraction (LEED), Raman spectroscopy and Scanning Tunneling Microscopy (STM). In particular, we present STM images of a carbon honeycomb lattice grown directly on Si(111). Our results demonstrate that the quality of graphene films formed depends not only on the substrate temperature but also on the carbon buffer layer at the interface. This method might be very promising for graphene-based electronics and its integration into the silicon technology. △ Less

Submitted 22 December, 2012; originally announced December 2012.

Comments: Accepted in APL

Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints

Authors: Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin, James Worrell

Abstract: 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 characteris… ▽ More 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. △ Less

Submitted 6 November, 2012; originally announced November 2012.

Comments: Submitted

Synthesis from LTL Specifications with Mean-Payoff Objectives

Authors: Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin

Abstract: 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… ▽ More 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. △ Less

Submitted 9 January, 2013; v1 submitted 11 October, 2012; originally announced October 2012.

The Complexity of Multi-Mean-Payoff and Multi-Energy Games

Authors: Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Rabinovich, Jean-Francois Raskin

Abstract: In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (re… ▽ More In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of multi-energy games and show the inter-reducibility of multimean-payoff and multi-energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete. Finally we present the first solution of multi-meanpayoff games with infinite-memory strategies. We show that multi-mean-payoff games with mean-payoff-sup objectives can be decided in NP and coNP, whereas multi-mean-payoff games with mean-payoff-inf objectives are coNP-complete. △ Less

Submitted 14 September, 2012; originally announced September 2012.

Comments: arXiv admin note: substantial text overlap with arXiv:1007.1669

Anisotropic Vapor HF etching of silicon dioxide for Si microstructure release

Authors: Vikram Passi, Ulf Sodervall, Bengt Nilsson, Goran Petersson, Mats Hagberg, Christophe Krzeminski, Emmanuel Dubois, Bert Du Bois, Jean-Pierre Raskin

Abstract: Damages are created in a sacrificial layer of silicon dioxide by ion implantation to enhance the etch rate of silicon-dioxide in liquid and vapor phase hydrofluoric acid. The etch rate ratio between implanted and unimplanted silicon dioxide is more than 150 in vapor hydrofluoric acid (VHF). This feature is of interest to greatly reduce the underetch of microelectromechanical systems anchors. Based… ▽ More Damages are created in a sacrificial layer of silicon dioxide by ion implantation to enhance the etch rate of silicon-dioxide in liquid and vapor phase hydrofluoric acid. The etch rate ratio between implanted and unimplanted silicon dioxide is more than 150 in vapor hydrofluoric acid (VHF). This feature is of interest to greatly reduce the underetch of microelectromechanical systems anchors. Based on the experimentally extracted etch rate of unimplanted and implanted silicon dioxide, the patterning of the sacrificial layer can be predicted by simulation. △ Less

Submitted 10 July, 2012; originally announced July 2012.

Journal ref: Microelectronic Engineering 95 (2012) 83-89

Controllers with Minimal Observation Power (Application to Timed Systems)

Authors: Peter Bulychev, Franck Cassez, Alexandre David, Kim G. Larsen, Jean-Francois Raskin, Pierre-Alain Reynier

Abstract: We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some informat… ▽ More We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies. △ Less

Submitted 2 July, 2012; originally announced July 2012.

Comments: This is the full version of the ATVA'12 paper

Strategy Synthesis for Multi-dimensional Quantitative Objectives

Authors: Krishnendu Chatterjee, Mickael Randour, Jean-François Raskin

Abstract: 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 condi… ▽ More 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. △ Less

Submitted 3 November, 2014; v1 submitted 24 January, 2012; originally announced January 2012.

Comments: Conference version published in CONCUR 2012, LNCS 7454. Journal version published in Acta Informatica, volume 51, issue 3-4, Springer, 2014

Queue-Dispatch Asynchronous Systems

Authors: Gilles Geeraerts, Alexander Heußner, Jean-François Raskin

Abstract: 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 availabl… ▽ More 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. △ Less

Submitted 17 October, 2012; v1 submitted 23 January, 2012; originally announced January 2012.

Comments: 38 pages, submitted for publication

Energy-band engineering for improved charge retention in fully self-aligned double floating-gate single-electron memories

Authors: Xiaohui Tang, Christophe Krzeminski, Aurélien Lecavelier des Etangs-Levallois, Zhenkun Chen, Emmanuel Dubois, Erich Kasper, Alim Karmous, Nicolas Reckinger, Denis Flandre, Laurent A. Francis, Jean-Pierre Colinge, Jean-Pierre Raskin

Abstract: We present a new fully self-aligned single-electron memory with a single pair of nano floating gates, made of different materials (Si and Ge). The energy barrier that prevents stored charge leakage is induced not only by quantum effects but also by the conduction-band offset that arises between Ge and Si. The dimension and position of each floating gate are well defined and controlled. The devices… ▽ More We present a new fully self-aligned single-electron memory with a single pair of nano floating gates, made of different materials (Si and Ge). The energy barrier that prevents stored charge leakage is induced not only by quantum effects but also by the conduction-band offset that arises between Ge and Si. The dimension and position of each floating gate are well defined and controlled. The devices exhibit a long retention time and single-electron injection at room temperature. △ Less

Submitted 15 November, 2011; originally announced November 2011.

Journal ref: Nano Lett., 2011, 11 (11), pp 4520--4526