Quantitative Compositional Reasoning

K. Chatterjee, L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, Mariëlle Ida Antoinette Stoelinga

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    15 Citations (Scopus)
    38 Downloads (Pure)

    Abstract

    We present a compositional theory of system verifica tion, 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 classical boolean rules for compositional reseaning have their quantitive counterparts in our setting. While our 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 wher all operations are computable in polynomial time.
    Original languageUndefined
    Title of host publicationThird International Conference on the Quantitative Evaluation of Systems (QEST'06)
    Place of PublicationLos Alamitos
    PublisherIEEE Computer Society Press
    Pages179-189
    Number of pages10
    ISBN (Print)0769526659
    DOIs
    Publication statusPublished - Sep 2006
    Event3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 - University of California, Riverside, United States
    Duration: 11 Sep 200614 Sep 2006
    Conference number: 3
    http://www.qest.org/qest2006/

    Publication series

    Name
    PublisherIEEE Computer Society Press
    Number2

    Conference

    Conference3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006
    Abbreviated titleQEST
    CountryUnited States
    CityRiverside
    Period11/09/0614/09/06
    Internet address

    Keywords

    • EWI-6940
    • IR-66362
    • METIS-238177

    Cite this