Citation
Arindam Chakrabarti, Krishnendu Chatterjee, Tom Henzinger, Orna Kupferman, Rupak Majumdar. "Verifying Quantitative Properties Using Bound Functions". CHARME, 50--64, October, 2005.

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 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.

Electronic downloads

• charme05.ps · application/postscript · 394 kbytes

• HTML

  Arindam Chakrabarti, Krishnendu Chatterjee, Tom Henzinger,
  Orna Kupferman, Rupak Majumdar. <a
  href="http://chess.eecs.berkeley.edu/pubs/77.html"
  >Verifying Quantitative Properties Using Bound
  Functions</a>, CHARME, 50--64, October, 2005.

• Plain text

  Arindam Chakrabarti, Krishnendu Chatterjee, Tom Henzinger,
  Orna Kupferman, Rupak Majumdar. "Verifying Quantitative
  Properties Using Bound Functions". CHARME, 50--64,
  October, 2005.

• BibTeX

  @inproceedings{ChakrabartiChatterjeeHenzingerKupfermanMajumdar05_VerifyingQuantitativePropertiesUsingBoundFunctions,
      author = {Arindam Chakrabarti and Krishnendu Chatterjee and
                Tom Henzinger and Orna Kupferman and Rupak Majumdar},
      title = {Verifying Quantitative Properties Using Bound
                Functions},
      booktitle = {CHARME},
      pages = {50--64},
      month = {October},
      year = {2005},
      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 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. },
      URL = {http://chess.eecs.berkeley.edu/pubs/77.html}
  }
  

Posted by Krishnendu Chatterjee, PhD on 9 May 2006.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.