Skip to main content

Automata-based quantitative reasoning

Suguman Bansal ( Rice university, USA )

Quantitative verification or the formal reasoning about quantitative properties of a system is an emerging area in the formal reasoning of systems, with applications in the design of cost- and resource-aware computational systems. At the core of reasoning about quantitative properties of systems lies the fundamental problem of comparison of the quantities associated with system runs. In this talk, I will introduce a novel mode of comparison between these runs: the online comparison of the aggregate values of two sequences of quantitative weights. This notion is embodied by comparator automata (comparators, in short), a new class of automata that read two infinite sequences of weights synchronously and relate their aggregate values. When applicable, comparator-based approaches operate by reducing a given problem in quantitative reasoning to one in qualitative reasoning bereft of any numerical computation. I will demonstrate the utility of our approach by employing comparator automata to the problem of quantitative inclusion with discounted sum, and show that it improves upon the state-of-the-art in theoretical complexity as well as practical performance. 

 

Speaker bio

Suguman Bansal is a final-year Ph.D. candidate at Rice University advised by Prof. Moshe Y. Vardi. Her research focuses on applying formal methods to building provably verifiable AI systems. She looks at the formal reasoning of quantitative measures of systems and uses them to design tools and techniques for enhancing automated verification and synthesis of AI systems. She is the recipient of a 2019 Future Faculty Fellowship, 2018 Rising Stars Award, 2016 Andrew Ladd Fellowship. She was a visiting fellow at the Simons Institute for Theoretical Computer Science at the University of California, Berkeley in 2018. She received her M.S. in Computer Science from Rice in 2016 and B.S. in Mathematics and Computer Science from Chennai Mathematical Institute in 2014.

Share this: