## Compositional Quantitative Reasoning

*Krishnendu Chatterjee, Luca de Alfaro, Marco Faella,
Thomas A. Henzinger,
Rupak Majumdar, and Marielle Stoelinga*

We present a compositional theory of system verification, where
specifications assign real-numbered costs to systems. These costs can
express a wide variety of quantitative system properties, such as
resource consumption, price, or a measure of how well a system
satisfies its specification. The theory supports the composition of
systems and specifications, and the hiding of variables. Boolean
refinement relations are replaced by real-numbered distances between
descriptions of a system at different levels of detail. We show that
the classical boolean rules for compositional reasoning have
quantitative counterparts in our setting.

While our general theory allows costs to be specified by arbitrary
cost functions, we also consider a class of linear cost functions,
which give rise to an instance of our framework where all operations
are computable in polynomial time.

*Proceedings of the
Third Annual Conference on Quantitative Evaluation of Systems*
(QEST), IEEE Computer Society Press, 2006, pp. 179-188.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2006 IEEE.