Probabilistic Model Checking for Energy-Utility Analysis

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in Buch/Sammelband/GutachtenBeigetragen

Abstract

In the context of a multi-disciplinary project, where we contribute with formal methods for reasoning about energy-awareness and other quantitative aspects of low-level resource management protocols, we made a series of interesting observations on the strengths and limitations of probabilistic model checking. To our surprise, the operating-system experts identified several relevant quantitative measures that are not supported by state-of-the-art probabilistic model checkers. Most notably are conditional probabilities and quantiles. Both are standard in mathematics and statistics, but research on them in the context of probabilistic model checking is rare. Another deficit of standard probabilistic model-checking techniques was the lack of methods for establishing properties imposing constraints on the energy-utility ratio.

In this article, we will present formalizations of the above mentioned quantitative measures, illustrate their significance by means of examples and sketch computation methods that we developed in our recent work.

Details

OriginalspracheEnglisch
TitelHorizons of the Mind. A Tribute to Prakash Panangaden
Redakteure/-innenFranck Breugel, Elham Kashefi, Catuscia Palamidessi, Jan Rutten
Herausgeber (Verlag)Springer, Cham
Seiten96-123
Seitenumfang28
ISBN (Print)978-3-319-06879-4
PublikationsstatusVeröffentlicht - 2014
Peer-Review-StatusNein

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 8464
ISSN0302-9743

Externe IDs

Scopus 84902526301
ORCID /0000-0002-5321-9343/work/142236668

Schlagworte

Schlagwörter

  • probabilistic model checking, energy-utility analysis

Bibliotheksschlagworte