Title: Reactive synthesis from Quantitative Constraints: An Automata Approach
Reactive synthesis is the automated construction, from a high-level description of its desired behavior, of a reactive system that continuously interacts with an uncontrollable external environment. The success of reactive synthesis from qualitative constraints calls for the question of whether one can perform synthesis from more expressive specifications?
In this talk, I will discuss the problem of reactive synthesis from quantitative constraints, referring to quantitative behaviors of systems such as rewards, costs, resources consumption, etc. The mention of quantitative properties may conjure up images of approaches that use numerical methods - optimization, linear programming, min-max games, and so on. In a paradigm shift, I will introduce a novel, purely automata-based approach to solve the synthesis problem whilst offering theoretical and practical improvements over the existing numerical methods-based state-of-the-art.
These significant improvements open the door for automata-based solutions in formal quantitative reasoning with exciting applications in planning and reinforcement learning.