ManySynth - Many-sided Synthesis of Reactive Systems: Foundations, Algorithms, and Tools

UMONS              FNRS

Project highlights

  • FNRS Incentive Grant for Scientific Research.
  • Project leader: Mickael Randour.
  • Duration: January 2018 to December 2019. Budget ~250.000 euros.
  • Postdoctoral positions are available: contact me! Here is a non-exhaustive list of possible topics:
    • multi-criteria approaches in formal methods,
    • machine learning meets formal methods,
    • multi-objective games,
    • synthesis in stochastic systems,
    • tool development,
    • industrial applications.

Project summary

We live in the days of ubiquitous computing: we are surrounded by reactive (computer) systems that continuously interact with their environment through user input, sensors, etc. Their correctness is often critical, either for safety reasons (e.g., ABS for cars) or due to constraints of mass production (e.g., smartphones). Unfortunately, their development is difficult and prone to errors. Formal verification and synthesis have proved to be success stories of computer science, aiming at the automated construction of provably-safe system controllers. Many techniques take roots in the game- theoretic framework, modeling the interaction between the system and its environment as a competitive game.

One crucial change over the last decade is the evolution from Boolean to quantitative specifications, giving birth to models describing performance of systems. However, prevalent frameworks only permit to consider a single quantitative (or qualitative) aspect at a time: they do not take into account their interplay and the resulting trade-offs. Such trade-offs may occur between different resources (e.g., decreasing response time requires additional computing power and energy consumption) but also between different behavioral models (e.g., average-case vs. worst-case performance). Those interactions are at the core of practical scenarios and require the developers to decide how to balance the different aspects. Hence, there is an absolute need for frameworks and tools capable of modeling interplays for the synthesis approach to be effective in practice. I coin the term “many-sided models” for such rich models in opposition to single-sided ones, which only allow to reason about a unique aspect of reactive systems.

The goal of ManySynth is to allow next-generation synthesis by establishing formal foundations, algorithms, and tools to support the paradigm shift from single-sided qualitative and quantitative models to many-sided ones, developing fundamental advances in this direction.