48 citations · 192 across the 15 of their papers we have counts for
16 papers
Games on Graphs: From Logic and Automata to Algorithms
Nathanaël Fijalkow, C. Aiswarya, Guy Avni +22
The objective of this book is to give a comprehensive presentation of the research field concerned with infinite duration games on graphs. Historically, these game models appeared…
JBMC: A Bounded Model Checking Tool for Java Bytecode
Romain Brenguier, Lucas Cordeiro, Daniel Kroening +1
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 a…
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
Swen Jacobs, Nicolas Basset, Roderick Bloem +11
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 th…
Admissibility in Quantitative Graph Games
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin +1
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,…
The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Romain Brenguier +13
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 benchm…
Decidability Results for Multi-objective Stochastic Games
Romain Brenguier, Vojtěch Forejt
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…
Optimal Assumptions for Synthesis
Romain Brenguier
Controller synthesis is the process of constructing a correct system automatically from its specification. This often requires assumptions about the behaviour of the environment. I…
Compositional Algorithms for Succinct Safety Games
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin +1
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 specif…
The Second Reactive Synthesis Competition (SYNTCOMP 2015)
Swen Jacobs, Roderick Bloem, Romain Brenguier +8
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 benchmar…
Non-Zero Sum Games for Reactive Synthesis
Romain Brenguier, Lorenzo Clemente, Paul Hunter +5
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…
Assume-Admissible Synthesis
Romain Brenguier, Jean-François Raskin, Ocan Sankur
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 noti…
The First Reactive Synthesis Competition (SYNTCOMP 2014)
Swen Jacobs, Roderick Bloem, Romain Brenguier +10
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 re…
Pure Nash Equilibria in Concurrent Deterministic Games
Patricia Bouyer, Romain Brenguier, Nicolas Markey +1
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 ga…
AbsSynthe: abstract synthesis from succinct safety specifications
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin +1
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 us…
Robust Equilibria in Concurrent Games
Romain Brenguier
We study the problem of finding robust equilibria in multiplayer concurrent games with mean payoff objectives. A -robust equilibrium is a strategy profile such that no coali…
The Complexity of Admissibility in Omega-Regular Games
Romain Brenguier, Jean-François Raskin, Mathieu Sassolas
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 Berwa…