Automata-based quantitative reasoning
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.