## Verifying Quantitative Properties using Bound Functions

*Arindam Chakrabarti, Krishnendu Chatterjee,
Thomas A. Henzinger,
Orna Kupferman, and Rupak Majumdar*

We define and study a quantitative generalization of the traditional
boolean framework of model-based specification and verification. 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 system 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
quantitative properties, like minimal necessary battery capacity and
maximal achievable lifetime, can be naturally specified by
*quantitative-bound automata*, which are finite automata with
integer registers whose analysis is constrained by a bound function
*f* that maps each system *K* to an integer *f(K)*.
Along with the linear-time, automaton-based view of quantitative
verification, we present a corresponding branching-time view based on
a quantitative-bound mu-calculus, and we study the relationship,
expressive power, and complexity of both views.

*Proceedings of the 13th International Conference on
Correct Hardware Design and Verification Methods*
(CHARME),
Lecture Notes in Computer Science 3725,
Springer, 2005, pp. 50-64.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2005 Springer.