---
OA_type: closed access
_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.\r\nQuantitative 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.\r\n"
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Arindam
  full_name: Chakrabarti, Arindam
  last_name: Chakrabarti
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  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
  last_name: Majumdar
citation:
  ama: 'Chakrabarti A, Chatterjee K, Henzinger TA, Kupferman O, Majumdar R. Verifying
    quantitative properties using bound functions. In: <i>Proceedings of the 13 IFIP
    WG 10.5 International Conference on Correct Hardware Design and Verification Methods</i>.
    Vol 3725. Springer Nature; 2005:50-64. doi:<a href="https://doi.org/10.1007/11560548_7">10.1007/11560548_7</a>'
  apa: 'Chakrabarti, A., Chatterjee, K., Henzinger, T. A., Kupferman, O., &#38; Majumdar,
    R. (2005). Verifying quantitative properties using bound functions. In <i>Proceedings
    of the 13 IFIP WG 10.5 international conference on Correct Hardware Design and
    Verification Methods</i> (Vol. 3725, pp. 50–64). Saarbrücken, Germany: Springer
    Nature. <a href="https://doi.org/10.1007/11560548_7">https://doi.org/10.1007/11560548_7</a>'
  chicago: Chakrabarti, Arindam, Krishnendu Chatterjee, Thomas A Henzinger, Orna Kupferman,
    and Ritankar Majumdar. “Verifying Quantitative Properties Using Bound Functions.”
    In <i>Proceedings of the 13 IFIP WG 10.5 International Conference on Correct Hardware
    Design and Verification Methods</i>, 3725:50–64. Springer Nature, 2005. <a href="https://doi.org/10.1007/11560548_7">https://doi.org/10.1007/11560548_7</a>.
  ieee: A. Chakrabarti, K. Chatterjee, T. A. Henzinger, O. Kupferman, and R. Majumdar,
    “Verifying quantitative properties using bound functions,” in <i>Proceedings of
    the 13 IFIP WG 10.5 international conference on Correct Hardware Design and Verification
    Methods</i>, Saarbrücken, Germany, 2005, vol. 3725, pp. 50–64.
  ista: 'Chakrabarti A, Chatterjee K, Henzinger TA, Kupferman O, Majumdar R. 2005.
    Verifying quantitative properties using bound functions. Proceedings of the 13
    IFIP WG 10.5 international conference on Correct Hardware Design and Verification
    Methods. CHARME: Correct Hardware Design and Verification Methods, LNCS, vol.
    3725, 50–64.'
  mla: Chakrabarti, Arindam, et al. “Verifying Quantitative Properties Using Bound
    Functions.” <i>Proceedings of the 13 IFIP WG 10.5 International Conference on
    Correct Hardware Design and Verification Methods</i>, vol. 3725, Springer Nature,
    2005, pp. 50–64, doi:<a href="https://doi.org/10.1007/11560548_7">10.1007/11560548_7</a>.
  short: A. Chakrabarti, K. Chatterjee, T.A. Henzinger, O. Kupferman, R. Majumdar,
    in:, Proceedings of the 13 IFIP WG 10.5 International Conference on Correct Hardware
    Design and Verification Methods, Springer Nature, 2005, pp. 50–64.
conference:
  end_date: 2005-10-06
  location: Saarbrücken, Germany
  name: 'CHARME: Correct Hardware Design and Verification Methods'
  start_date: 2005-10-03
date_created: 2018-12-11T12:09:29Z
date_published: 2005-09-19T00:00:00Z
date_updated: 2026-09-30T14:16:49Z
day: '19'
doi: 10.1007/11560548_7
extern: '1'
fulldoi: https://doi.org/10.1007/11560548_7
intvolume: '      3725'
language:
- iso: eng
month: '09'
oa_version: None
page: 50 - 64
publication: Proceedings of the 13 IFIP WG 10.5 international conference on Correct
  Hardware Design and Verification Methods
publication_identifier:
  isbn:
  - '9783540291053'
publication_status: published
publisher: Springer Nature
publist_id: '149'
status: public
title: Verifying quantitative properties using bound functions
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 3725
year: '2005'
...