---
_id: '4560'
abstract:
- lang: eng
text: |
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 μ-calculus, and we study the relationship, expressive power, and complexity of both views.
alternative_title:
- LNCS
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Chakrabarti A, Chatterjee K, Henzinger TA, Kupferman O, Majumdar R. Verifying
quantitative properties using bound functions. In: Vol 3725. Springer; 2005:50-64.
doi:10.1007/11560548_7'
apa: 'Chakrabarti, A., Chatterjee, K., Henzinger, T. A., Kupferman, O., & Majumdar,
R. (2005). Verifying quantitative properties using bound functions (Vol. 3725,
pp. 50–64). Presented at the CHARME: Correct Hardware Design and Verification
Methods, Springer. https://doi.org/10.1007/11560548_7'
chicago: Chakrabarti, Arindam, Krishnendu Chatterjee, Thomas A Henzinger, Orna Kupferman,
and Ritankar Majumdar. “Verifying Quantitative Properties Using Bound Functions,”
3725:50–64. Springer, 2005. https://doi.org/10.1007/11560548_7.
ieee: 'A. Chakrabarti, K. Chatterjee, T. A. Henzinger, O. Kupferman, and R. Majumdar,
“Verifying quantitative properties using bound functions,” presented at the CHARME:
Correct Hardware Design and Verification Methods, 2005, vol. 3725, pp. 50–64.'
ista: 'Chakrabarti A, Chatterjee K, Henzinger TA, Kupferman O, Majumdar R. 2005.
Verifying quantitative properties using bound functions. CHARME: Correct Hardware
Design and Verification Methods, LNCS, vol. 3725, 50–64.'
mla: Chakrabarti, Arindam, et al. Verifying Quantitative Properties Using Bound
Functions. Vol. 3725, Springer, 2005, pp. 50–64, doi:10.1007/11560548_7.
short: A. Chakrabarti, K. Chatterjee, T.A. Henzinger, O. Kupferman, R. Majumdar,
in:, Springer, 2005, pp. 50–64.
conference:
name: 'CHARME: Correct Hardware Design and Verification Methods'
date_created: 2018-12-11T12:09:29Z
date_published: 2005-09-19T00:00:00Z
date_updated: 2021-01-12T07:59:42Z
day: '19'
doi: 10.1007/11560548_7
extern: 1
intvolume: ' 3725'
month: '09'
page: 50 - 64
publication_status: published
publisher: Springer
publist_id: '149'
quality_controlled: 0
status: public
title: Verifying quantitative properties using bound functions
type: conference
volume: 3725
year: '2005'
...