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: 14 (2 best paper awards)

  • Arena-Independent Finite-Memory Determinacy in Stochastic Games. Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, Pierre Vandenhove. CONCUR'21, LIPIcs, Schloss Dagsthul, 2021. Extended version on arXiv (35 pages).
  • Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives. James C. A. Main, Mickael Randour, Jeremy Sproston. CONCUR'21, LIPIcs, Schloss Dagsthul, 2021. Extended version on arXiv (36 pages).
  • Life is Random, Time is Not: Markov Decision Processes with Window Objectives. Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, Mickael Randour. Logical Methods in Computer Science, volume 16, issue 4, pages 13:1-13:30, 2020. Extended version on arXiv (23 pages).
  • Decisiveness of Stochastic Systems and its Application to Hybrid Models. Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière, Pierre Vandenhove. GandALF'20, EPTCS, 18 pages, 2020. Extended version on arXiv.
  • Games Where You Can Play Optimally with Arena-Independent Finite Memory. Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, Pierre Vandenhove. CONCUR'20, LIPIcs, 22 pages, Schloss Dagstuhl, 2020. Extended version on arXiv.
  • Simple Strategies in Multi-Objective MDPs. Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour. TACAS'20, LNCS 12078, 25 pages, Springer, 2020. Extended version on arXiv.
  • Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. Frantisek Blahoudek, Alexandre Duret-Lutz, Jan Strejcek. CAV'20, LNCS 12225, 13 pages, Springer, 2020.
  • LTL to Smaller Self-Loop Alternating Automata and Back. František Blahoudek, Juraj Major, Jan Strejček. ICTAC'19, LNCS 11884, 20 pages, Springer, 2019. On arXiv. Best paper award at ICTAC 2019.
  • Life is Random, Time is Not: Markov Decision Processes with Window Objectives. Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, Mickael Randour. CONCUR'19, LIPIcs 140, 18 pages, Schloss Dagstuhl, 2019. Extended version on arXiv (23 pages). Best paper award at CONCUR 2019.
  • Energy mean-payoff games. Véronique Bruyère, Quentin Hautem, Mickael Randour, Jean-François Raskin. CONCUR'19, LIPIcs 140, 17 pages, Schloss Dagstuhl, 2019. On arXiv (29 pages)
  • 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 11781, 9 pages, 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 11781, 17 pages, 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).