ControlleRS

Controllers in Many-sided Reactive Synthesis - A Strategic Perspective

Project highlights

  • FNRS Research Project.
  • Project leader: Mickael Randour.
  • Duration: January 2023 to December 2026. Budget ~270.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 and AI,
    • 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. Recent research focuses on taking into account the interplay between different quantitative (or qualitative) aspects 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 developers to decide how to balance the different aspects. My research group is at the forefront of research on many-sided synthesis, which supports such multi-objective reasoning.

The goal of ControlleRS is to challenge the key concept of strategy, currently based on automata-like finite-state machines acting as blueprints for implementable controllers. I aim to broaden the theoretical understanding and the practical usefulness of this abstract concept through the systematic study of alternative strategy models over the complete span from theoretical power to proper applicability. This endeavor promises fundamental advances toward truly implementable many-sided synthesis.

Publications supported by the project: 5

Peer-reviewed journals

  1. LMCS
    Arena-Independent Finite-Memory Determinacy in Stochastic Games
    Logical Methods in Computer Science, 2023

International peer-reviewed conferences

  1. FSTTCS
    Reachability Games and Friends: A Journey Through the Lens of Memory and Complexity
    Thomas BrihayeAline GoeminneJames C. A. Main, and Mickael Randour
    In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023, December 18-20, 2023, IIIT Hyderabad, Telangana, India , 2023
  2. IJCAI
    Half-Positional Objectives Recognized by Deterministic Büchi Automata (Extended Abstract)
    In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China , 2023
  3. ICALP
    How to Play Optimally for Regular Objectives?
    In 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany , 2023
  4. STACS
    Arena-Independent Memory Bounds for Nash Equilibria in Reachability Games
    In 41st International Symposium on Theoretical Aspects of Computer Science, STACS 2024, March 12-14, 2024, Clermont-Ferrand, France , 2024