Quantitative Verification and Synthesis
Quantitative constraints have been successfully used to state and analyze non-functional properties such as energy consumption, performance, or reliability. Functional properties are typically viewed in a purely qualitative sense. Desired properties are written in temporal languages and the outcome of verification is a simple Yes or No answer stating that a system satisfies or does not satisfy the desired property. We believe that this black and white view is insufficient both for verification and for synthesis. Instead, we propose that specifications should have a quantitative aspect.
Our recent research shows that quantitative techniques give new insights into qualitative specifications. For instance, average-reward properties allow us to express properties like default behavior or preference relations between implementations that all satisfy the functional property. These additional properties are particularly useful in a synthesis setting, where we aim to automatically construct a system that satisfies the specification, because they allow us to guide the synthesis process making the outcome of synthesis more predictable.
In this talk I will give an overview of
- how classical specification can be augmented with quantitative constraints,
- list different quantitative constraints that arise in this way, and
- show how to verify and synthesize systems that satisfied the initial specification and optimize such quantitative constraints.
This is joint work with Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger, Arjun Radhakrishna, and Rohit Singh.