Controllers in Many-sided Reactive Synthesis: a Strategic Perspective

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 this project 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.