Title: Reactive synthesis from Quantitative Constraints: An Automata Approach

Speaker: Suguman Bansal    (bio) (bio)

Suguman Bansal is an NSF/CRA Computing Innovation Postdoctoral Fellow at the University of Pennsylvania, mentored by Prof. Rajeev Alur. Her research goal is on advancing Assured Autonomy using formal methods and programming languages to design-develop-deploy safe AI systems.

She is the recipient of the 2020 NSF CI Fellowship and has been named a 2021 MIT EECS Rising Star. Her research has appeared at venues including AAAI, CAV, TACAS, and POPL. She completed her Ph.D. in 2020, advised by Prof. Moshe Y. Vardi, from Rice University. She received B.S. with Honors in 2014 from Chennai Mathematical Institute.

When: Tuesday, 05 October 2021 at 1900 hrs (IST)    

Abstract:
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.