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.

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.


Publications supported by the project

  • Life is Random, Time is Not: Markov Decision Processes with Window Objectives. Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, Mickael Randour. CONCUR'19, LIPIcs, Schloss Dagstuhl, 2019 Extended version on arXiv (23 pages).
  • Energy mean-payoff games. Véronique Bruyère, Quentin Hautem, Mickael Randour, Jean-François Raskin. CONCUR'19, LIPIcs, Schloss Dagstuhl, 2019.
  • LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL. Juraj Major, František Blahoudek, Miriama Sasaráková, Jan Strejček and Tatiana Zbončáková. ATVA'19, LNCS, Springer, 2019.
  • Generic Emptiness Check for Fun and Profit. Christel Baier, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller and Jan Strejček. ATVA'19, LNCS, Springer, 2019.
  • Extending finite-memory determinacy by Boolean combination of winning conditions. Stéphane Le Roux, Arno Pauly, Mickael Randour. FSTTCS'18, LIPIcs, 15 pages, Schloss Dagstuhl, 2018. Extended version on arXiv (20 pages).
  • Multi-weighted Markov decision processes with reachability objectives. Patricia Bouyer, Mauricio González, Nicolas Markey, Mickael Randour. GandALF'18, EPTCS 277, 15 pages, 2018. On arXiv (15 pages).