PhD and Post-Doc positions at the Université libre de Bruxelles

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

Verifying Learning Artificial Intelligence Systems
(4 years Excellent of Science project, 2018-2021)
in collaboration with KULeuven and U Namur

Subgame perfection in graph games
(4 years PDR FNRS project, 2018-2021)
in collaboration with U Mons

* Positions. Several Post-Doc positions are open at the Université libre de Bruxelles 
(ULB). These positions are funded by three projects (listed above), under the lead of 
Prof. Jean-François Raskin, Prof. Gilles Geeraerts, and Dr. Emmanuel Filiot.

* Summary of the research projects. 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 four main research directions of those projects 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
	• To study how verification techniques can be lifted to be applicable to systems that uses learning

* Starting dates. At any time during the project.

* Salary. Annual net salary (after all taxes) starts at 2,421.51 euros/month for a 
Post-Doc student, and at 1,964.92 euros / month for a PhD student. In addition, 
advantages include complete health insurance.

* 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), 
Prof. Geeraerts (gigeerae [at] ulb [dot] ac [dot] be), and 
Dr. Emmanuel Filiot (efiliot [at] ulb [dot] ac [dot] be).

Comments are closed.