Post-doc positions in Brussels on games for reactive synthesis

Non-Zero Sum Game Graphs:
Applications to Reactive Synthesis and Beyond
(5 years FWB ARC research project, 2016-2021)

* Positions. Post-Doc positions are open at the Université libre de Bruxelles 
 (ULB). These positions are funded by and ARC collaborative research project 
 of the Fédération Wallonie-Bruxelles, under the lead of Prof. Jean-François 
 Raskin and Gilles Geeraerts.

* Summary of the research project. Reactive systems are computer systems that 
 maintain a continuous interaction with the environment in which they operate.
 Such systems are nowadays part of our daily life: think about common yet
 critical applications like engine control units in automotive, plane 
 autopilots, medical devices, etc. Clearly, any flaw in such critical systems
 can have catastrophic consequences. Yet, they exhibit several characteristics,
 like real-time constraints, concurrency, parallelism, etc., that make them
 difficult to design correctly.
To ensure the design of reactive computer systems that are dependable, safe 
and efficient, researchers and industrials have advocated the use of so-called 
formal methods, that rely on mathematical models to express precisely and 
analyse the behaviours of those systems. A very popular formal method is 
model checking: it amounts to comparing a model of a system to its 
specification in order to find design errors early in the development cycle. 
Hence, model checking can be regarded as a sophisticated debugging method. 
In this project, we will attack a more scientifically challenging goal, 
called synthesis. We want to propose techniques (models, algorithms and 
tools) that, given a specification for a reactive system and a model of its 
environment, compute (synthesise) a correct system, i.e., one that enforces 
the specification no matter how the environment behaves. The main model that 
will be considered in the project is that of games played on graphs, we will
seek to extend classical results to the setting of non-zero sum games. More 
precisely, the three main research directions of the project are:
	• To define and study new models and solution concepts based on multi-player non-zero-sum games.
	• To define and study new solutions concepts that avoid the fully adversarial assumption, because this assumption can be shown to be often too bold an abstraction of real systems.
	• To exploit the multi-player, non zero-sum, games on graph model beyond the setting of reactive synthesis. Other potential domains of application include: biological systems, multi-agent systems, network routing, (real-time) scheduling, automata theory, etc

* Starting dates. At any time during the project.

* Salary. Annual net salary (after all taxes) starts at €2,296.82/months for 
  a Post-Doc student, in addition, advantages include complete health 

* The research environment. ULB ( is a complete university 
  located in the city of Brussels at the center of Europe (25.000+ students 
  with 30% coming from abroad). The Formal Methods and Verification group is 
  part of the Computer Science Department of the Faculty of Sciences. The 
  group maintains a large number of active collaborations with other research 
  groups in computer-aided verification across Europe and the USA. The group 
  is also part of the Belgian Federated Center for Verification 
  ( that gathers all the Belgian research groups active in 
  computer aided verification and hosts a monthly seminar with renowned 
  guest speakers. The working language is English.

* Further information and application. Potential candidates can contact 
  Prof. Raskin (jraskin [at] ulb [dot] ac [dot] be) and Prof. Geeraerts 
  (gigeerae [at] ulb [dot] ac [dot] be).

Comments are closed.