"Non-Zero Sum Game Graphs: Applications to Reactive Synthesis and Beyond"

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,… 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.

Another challenging method, called synthesis, is 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 synthesis problem is the central topic of this project, driven by the Verification and formal methods’ team (Computer Department, Faculté des Sciences).

Spokesperson

Jean-François Raskin
Verification and formal methods’ team
Faculty of Sciences

Dates
Created on August 31, 2018