Verifying quantitative properties using bound functions

Abstract. We dene and study a quantitative generalization of the tra-ditional boolean framework of model-based specication and verication. In our setting, propositions have integer values at states, and properties have integer values on traces. For example, the value of a quantitative proposition at a state may represent power consumed at the state, and the value of a quantitative property on a trace may represent energy used along the trace. The value of a quantitative property at a state, then, is the maximum (or minimum) value achievable over all possible traces from the state. In this framework, model checking can be used to compute, for example, the minimum battery capacity necessary for achieving a given objective, or the maximal achievable lifetime of a sys-tem with a given initial battery capacity. In the case of open systems, these problems require the solution of games with integer values. Quantitative model checking and game solving is undecidable, except if bounds on the computation can be found. Indeed, many interesting quan-titative properties, like minimal necessary battery capacity and maximal achievable lifetime, can be naturally specied by quantitative-bound au-tomata, which are nite automata with integer registers whose analysis is constrained by a bound function f that maps each system K to an inte-ger f(K). Along with the linear-time, automaton-based view of quantita-tive verication, we present a corresponding branching-time view based on a quantitative-bound -calculus, and we study the relationship, ex-pressive power, and complexity of both views.