Citation
Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Tom Henzinger, Rupak Majumdar, Marielle Stoelinga. "Quantitative Compositional Pricing". QEST 06, September, 2006.

Abstract
We present a compositional theory of system verification, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantitative system properties, such as resource consumption, price, or a measure of how well a system satisfies its specification. The theory supports the composition of systems and specifications, and the hiding of variables. Boolean refinement relations are replaced by real-numbered distances between descriptions of a system at different levels of detail. We show that the classical boolean rules for compositional reasoning have quantitative counterparts in our setting. While our general theory allows costs to be specified by arbitrary cost functions, we also consider a class of linear cost functions, which give rise to an instance of our framework where all operations are computable in polynomial time.

Electronic downloads

• main.ps · application/postscript · 320 kbytes

• HTML

  Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Tom
  Henzinger, Rupak Majumdar, Marielle Stoelinga. <a
  href="http://chess.eecs.berkeley.edu/pubs/233.html"
  >Quantitative Compositional Pricing</a>, QEST 06,
  September, 2006.

• Plain text

  Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Tom
  Henzinger, Rupak Majumdar, Marielle Stoelinga.
  "Quantitative Compositional Pricing". QEST 06,
  September, 2006.

• BibTeX

  @inproceedings{ChatterjeedeAlfaroFaellaHenzingerMajumdarStoelinga06_QuantitativeCompositionalPricing,
      author = {Krishnendu Chatterjee and Luca de Alfaro and Marco
                Faella and Tom Henzinger and Rupak Majumdar and
                Marielle Stoelinga},
      title = {Quantitative Compositional Pricing},
      booktitle = {QEST 06},
      month = {September},
      year = {2006},
      abstract = {We present a compositional theory of system
                verification, where specifications assign
                real-numbered costs to systems. These costs can
                express a wide variety of quantitative system
                properties, such as resource consumption, price,
                or a measure of how well a system satisfies its
                specification. The theory supports the composition
                of systems and specifications, and the hiding of
                variables. Boolean refinement relations are
                replaced by real-numbered distances between
                descriptions of a system at different levels of
                detail. We show that the classical boolean rules
                for compositional reasoning have quantitative
                counterparts in our setting. While our general
                theory allows costs to be specified by arbitrary
                cost functions, we also consider a class of linear
                cost functions, which give rise to an instance of
                our framework where all operations are computable
                in polynomial time. },
      URL = {http://chess.eecs.berkeley.edu/pubs/233.html}
  }
  

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