|Résumé||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
(1) how classical specification can be augmented with quantitative constraints,
(2) list different quantitative constraints that arise in this way, and
(3) show how to verify and synthesize systems that satisfied the
initial specification and optimize such quantitative constraints.
This is joint work with R. Bloem, K. Chatterjee, K. Greimel, T. Henzinger,
A. Radhakrishna, R. Singh, and C. von Essen.