Research

I am a Post-doc student at University of Oxford. Until september 2015 I was at ULB, member of the ERC inVEST project, working in the MFV group, in charge of the verification seminars.

CV

My CV is available here: (English, French)

Research Activities

My work focuses on the sythesis of computerized systems. In particular, I use game theoretical concepts to find good strategies in multi-agent systems.

During my thesis, I studied the concept of Nash equilibrium in concurrent games. I also studied timed games. This games are perfectly suited for the control of real time systems. I developed algorithms for computing Nash equilibria in these kind of games with omega regular objectives and wrote a tool called PRALINE.

I am now mostly interested in:

  • quantitative objectives in timed games and multiplayer-games;
  • concepts for controller synthesis in distributed systems;
  • developing tools for synthesis.

Publications

BBMU14
Patricia Bouyer, Romain Brenguier, Nicolas Markey and Michael Ummels. Pure Nash Equilibria in Concurrent Games. Logical Methods in Computer Science, 2015. To appear. ( PDF )

Conferences

BR15
R. Brenguier, J.-F. Raskin   Optimal Values of Multidimensional Mean-Payoff Games .   In CAV 2015
BRS14
R. Brenguier, J.-F. Raskin and M. Sassolas.   The complexity of admissibility in omega-regular games.   In CSL-LICS 2014. July 2014
BPRS14
R. Brenguier and G. Perez and J.-F. Raskin and O. Sankur . AbsSynthe: abstract synthesis from succinct safety specificationsIn 3rd Workshop in Synthesis. 2014.
BCR14
R. Brenguier, F. Cassez and J.-F. Raskin.   Energy and Mean-Payoff Timed Games .   In HSCC 2014. Avril 2014.
Bre13a
R. BrenguierPRALINE: A Tool for Computing Nash Equilibria in Concurrent GamesIn CAV'13, LNCS 8044, pages 890-895. Springer, 2013. ( PDF | BibTeX + Abstract )
BGS12
R. Brenguier, S. Göller and O. Sankur A Comparison of Succinctly Represented Finite-State SystemsIn CONCUR'12, LNCS 7454, pages 147-161. Springer, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )
BBMU12
P. Bouyer, R. Brenguier, N. Markey and M. UmmelsConcurrent games with ordered objectivesIn FoSSaCS'12, LNCS 7213, pages 301-315. Springer, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )
BBMU11
P. Bouyer, R. Brenguier, N. Markey and M. UmmelsNash Equilibria in Concurrent Games with Büchi ObjectivesIn FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 375-386. Leibniz-Zentrum für Informatik, 2011. ( PDF | BibTeX + Abstract )
BBM10a
P. Bouyer, R. Brenguier and N. MarkeyComputing Equilibria in Two-Player Timed Games via Turn-Based Finite GamesIn FORMATS'10, LNCS 6246, pages 62-76. Springer, 2010. ( PDF | PDF (long version) | BibTeX + Abstract )
BBM10b
P. Bouyer, R. Brenguier and N. MarkeyNash Equilibria for Reachability Objectives in Multi-player Timed GamesIn CONCUR'10, LNCS 6269, pages 192-206. Springer, 2010. ( PDF | PDF (long version) | BibTeX + Abstract )

Theses

Bre12
R. BrenguierÉquilibres de Nash dans les Jeux Concurrents - Application aux Jeux Temporisés.  Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2012. ( PDF | BibTeX )
Bre09
R. BrenguierCalcul des équilibres de Nash dans les jeux temporisés.  Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2009. ( PDF | PS | PS.GZ | BibTeX )

Unpublished works

Bre14
R. Brenguier.   Robust Equilibria in Concurrent Games .   In CoRR, vol. abs/1311.7683

Talks

  • April 2015, seminar in LIF, Marseille (France) Admissibility Concepts for Synthesis
  • March 2015, MFV Seminar at ULB, Brussels (Belgium) Assume Admissible Synthesis
  • March 2015, ERC meeting, Vienna (Austria) Assume Admissible Synthesis
  • March 2015, seminar in LIAFA, Paris (France) Assume Admissible Synthesis
  • January 2015, Dagstuhl seminar, Dagstuhl (Allemagne) The Complexity of Admissibility in Omega-Regular Games
  • December 2014, seminar at INRIA, Grenoble (France) Controller synthesis: from circuits to quantitative, real-time and distributed systems
  • July 2014, CSL-LICS, Vienna (Austria) The Complexity of Admissibility in Omega-Regular Games
  • Avril 2014, HSCC, Berlin (Allemagne), Energy and Mean-Payoff Timed Games
  • MFV Seminar, ULB, March 21 2014 Energy and Mean Payoff Timed Games slides
  • The Complexity of Admissibility in omega-Regular Games GDR IM - GT-jeux: annual meeting, Paris, January 23 2014 slides
  • CFV Seminar, ULB slides
  • Older talks

Tools

  • PRALINE: Repellor ALgorIthm for Nash Equilibria (download last version)
  • AbsSynthe: abstract synthesis from succinct safety specifications
  • Reglisse A tool to generate hardware description (AIGER and Verilog) from safety conditions given by regular languages.
  • Speculoos: A set of tools for generating AIGER circuits.
  • Praline 2.0: Tools for controller synthesis in multi-agent systems.
Libraries:
  • Ocaml-cudd: An Ocaml interface to BDD and ADD functions of the CUDD library.
  • Ocaml-aiger: An Ocaml library to read, write and manipulate AIGER files.
Patch:
  • cudd: A patch for CUDD to use matrix multiplication in other rings than the default one.

Contact

You can contact me by

  • E-mail: romain.brenguier [at] ulb.ac.be
  • Phone: 26 50 56 24