-
Games on Graphs
Authors:
Nathanaël Fijalkow,
Nathalie Bertrand,
Patricia Bouyer-Decitre,
Romain Brenguier,
Arnaud Carayol,
John Fearnley,
Hugo Gimbert,
Florian Horn,
Rasmus Ibsen-Jensen,
Nicolas Markey,
Benjamin Monmege,
Petr Novotný,
Mickael Randour,
Ocan Sankur,
Sylvain Schmitz,
Olivier Serre,
Mateusz Skomra
Abstract:
The objective of this collaborative textbook is to present the state of the art on games on graphs, which is part of a larger research topic called game theory. Games on graphs is the field concerned with games whose rules and evolution are represented by a graph.
The objective of this collaborative textbook is to present the state of the art on games on graphs, which is part of a larger research topic called game theory. Games on graphs is the field concerned with games whose rules and evolution are represented by a graph.
△ Less
Submitted 17 May, 2023;
originally announced May 2023.
-
JBMC: A Bounded Model Checking Tool for Java Bytecode
Authors:
Romain Brenguier,
Lucas Cordeiro,
Daniel Kroening,
Peter Schrammel
Abstract:
JBMC is an open-source SAT- and SMT-based bounded model checking tool for verifying Java bytecode. JBMC relies on an operational model of the Java libraries, which conservatively approximates their semantics, to verify assertion violations, array out-of-bounds, unintended arithmetic overflows, and other kinds of functional and runtime errors in Java bytecode. JBMC can be used to either falsify pro…
▽ More
JBMC is an open-source SAT- and SMT-based bounded model checking tool for verifying Java bytecode. JBMC relies on an operational model of the Java libraries, which conservatively approximates their semantics, to verify assertion violations, array out-of-bounds, unintended arithmetic overflows, and other kinds of functional and runtime errors in Java bytecode. JBMC can be used to either falsify properties or prove program correctness if an upper bound on the depth of the state-space is known. Practical applications of JBMC include but are not limited to bug finding, property checking, test input generation, detection of security vulnerabilities, and program synthesis. Here we provide a detailed description of JBMC's architecture and its functionalities, including an in-depth discussion of its background theories and underlying technologies, including a state-of-the-art string solver to ensure safety and security of Java bytecode.
△ Less
Submitted 5 February, 2023;
originally announced February 2023.
-
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
Authors:
Swen Jacobs,
Nicolas Basset,
Roderick Bloem,
Romain Brenguier,
Maximilien Colange,
Peter Faymonville,
Bernd Finkbeiner,
Ayrat Khalimov,
Felix Klein,
Thibaud Michaud,
Guillermo A. Pérez,
Jean-François Raskin,
Ocan Sankur,
Leander Tentrup
Abstract:
We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2017. We present the participants of SYNTCOMP 2017, with a focus on changes with respect to the previous years and on the two completely new…
▽ More
We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the benchmark selection, evaluation scheme and the experimental setup of SYNTCOMP 2017. We present the participants of SYNTCOMP 2017, with a focus on changes with respect to the previous years and on the two completely new tools that have entered the competition. Finally, we present and analyze the results of our experimental evaluation, including a ranking of tools with respect to quantity and quality of solutions.
△ Less
Submitted 28 November, 2017;
originally announced November 2017.
-
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.
-
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.
-
Decidability Results for Multi-objective Stochastic Games
Authors:
Romain Brenguier,
Vojtěch Forejt
Abstract:
We study stochastic two-player turn-based games in which the objective of one player is to ensure several infinite-horizon total reward objectives, while the other player attempts to spoil at least one of the objectives. The games have previously been shown not to be determined, and an approximation algorithm for computing a Pareto curve has been given. The major drawback of the existing algorithm…
▽ More
We study stochastic two-player turn-based games in which the objective of one player is to ensure several infinite-horizon total reward objectives, while the other player attempts to spoil at least one of the objectives. The games have previously been shown not to be determined, and an approximation algorithm for computing a Pareto curve has been given. The major drawback of the existing algorithm is that it needs to compute Pareto curves for finite horizon objectives (for increasing length of the horizon), and the size of these Pareto curves can grow unboundedly, even when the infinite-horizon Pareto curve is small. By adapting existing results, we first give an algorithm that computes the Pareto curve for determined games. Then, as the main result of the paper, we show that for the natural class of stopping games and when there are two reward objectives, the problem of deciding whether a player can ensure satisfaction of the objectives with given thresholds is decidable. The result relies on intricate and novel proof which shows that the Pareto curves contain only finitely many points. As a consequence, we get that the two-objective discounted-reward problem for unrestricted class of stochastic games is decidable.
△ Less
Submitted 12 May, 2016;
originally announced May 2016.
-
Optimal Assumptions for Synthesis
Authors:
Romain Brenguier
Abstract:
Controller synthesis is the process of constructing a correct system automatically from its specification. This often requires assumptions about the behaviour of the environment. It is difficult for the designer to identify the assumptions that ensures the existence of a correct controller, and doing so manually can lead to assumptions that are stronger than necessary. As a consequence the generat…
▽ More
Controller synthesis is the process of constructing a correct system automatically from its specification. This often requires assumptions about the behaviour of the environment. It is difficult for the designer to identify the assumptions that ensures the existence of a correct controller, and doing so manually can lead to assumptions that are stronger than necessary. As a consequence the generated controllers are suboptimal in terms of generality and robustness. In this work, given a specification, we identify the weakest assumptions that ensures the existence of a controller. We also consider two important classes of assumptions: the ones that can be ensured by the environment and assumptions that speaks only about inputs of the systems. We show that optimal assumptions correspond to strongly winning strategies, admissible strategies and remorsefree strategies respectively. Based on this correspondence, we propose an algorithm for computing optimal assumptions that can be ensured by the environment.
△ Less
Submitted 12 April, 2016;
originally announced April 2016.
-
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.
-
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.
-
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.
-
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.
-
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.
-
Pure Nash Equilibria in Concurrent Deterministic Games
Authors:
Patricia Bouyer,
Romain Brenguier,
Nicolas Markey,
Michael Ummels
Abstract:
We study pure-strategy Nash equilibria in multi-player concurrent deterministic games, for a variety of preference relations. We provide a novel construction, called the suspect game, which transforms a multi-player concurrent game into a two-player turn-based game which turns Nash equilibria into winning strategies (for some objective that depends on the preference relations of the players in th…
▽ More
We study pure-strategy Nash equilibria in multi-player concurrent deterministic games, for a variety of preference relations. We provide a novel construction, called the suspect game, which transforms a multi-player concurrent game into a two-player turn-based game which turns Nash equilibria into winning strategies (for some objective that depends on the preference relations of the players in the original game). We use that transformation to design algorithms for computing Nash equilibria in finite games, which in most cases have optimal worst-case complexity, for large classes of preference relations. This includes the purely qualitative framework, where each player has a single omega-regular objective that she wants to satisfy, but also the larger class of semi-quantitative objectives, where each player has several omega-regular objectives equipped with a preorder (for instance, a player may want to satisfy all her objectives, or to maximise the number of objectives that she achieves.)
△ Less
Submitted 18 June, 2015; v1 submitted 23 March, 2015;
originally announced March 2015.
-
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.
-
Robust Equilibria in Concurrent Games
Authors:
Romain Brenguier
Abstract:
We study the problem of finding robust equilibria in multiplayer concurrent games with mean payoff objectives. A $(k,t)$-robust equilibrium is a strategy profile such that no coalition of size $k$ can improve the payoff of one its member by deviating, and no coalition of size $t$ can decrease the payoff of other players. We are interested in pure equilibria, that is, solutions that can be implemen…
▽ More
We study the problem of finding robust equilibria in multiplayer concurrent games with mean payoff objectives. A $(k,t)$-robust equilibrium is a strategy profile such that no coalition of size $k$ can improve the payoff of one its member by deviating, and no coalition of size $t$ can decrease the payoff of other players. We are interested in pure equilibria, that is, solutions that can be implemented using non-randomized strategies. We suggest a general transformation from multiplayer games to two-player games such that pure equilibria in the first game correspond to winning strategies in the second one. We then devise from this transformation, an algorithm which computes equilibria in mean-payoff games. Robust equilibria in mean-payoff games reduce to winning strategies in multidimensional mean-payoff games for some threshold satisfying some constraints. We then show that the existence of such equilibria can be decided in polynomial space, and that the decision problem is PSPACE-complete.
△ Less
Submitted 1 February, 2016; v1 submitted 29 November, 2013;
originally announced November 2013.
-
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.
