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 insurance.
* The research environment. ULB (http://www.ulb.ac.be) 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 (http://cfv.ulb.ac.be) 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).
----
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ [email protected] ]]
