Compositional Quantitative Reasoning * Krishnendu Chatterjee

UC Los Angeles Mari"elle StoelingaUniversity of Twente Abstract. We present a compositional theory of system verifica-tion, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantitative system prop-erties, such as resource consumption, price, or a measure of how well a system satisfies its specification. The theory supports thecomposition of systems and specifications, and the hiding of variables. Boolean refinement relations are replaced by real-numbereddistances between descriptions of a system at different levels of detail. We show that the classical boolean rules for compositionalreasoning have quantitative counterparts in our setting