Sciweavers

CHARME
2005
Springer

Verifying Quantitative Properties Using Bound Functions

14 years 21 days ago
Verifying Quantitative Properties Using Bound Functions
Abstract. 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...
Arindam Chakrabarti, Krishnendu Chatterjee, Thomas
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CHARME
Authors Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar
Comments (0)