Probabilistic Model Checking for Energy-Utility Analysis

Christel BaierChristel Baier, Clemens DubslaffClemens Dubslaff, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz, Sascha WunderlichSascha Wunderlich

DOI Link

Christel Baier, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz, Sascha Wunderlich
Probabilistic Model Checking for Energy-Utility Analysis
In Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of Lecture Notes in Computer Science, 96--123. Springer, 2014

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-06880-0_5.

@incollection{BDKKW2014,
  author    = {Christel Baier and Clemens Dubslaff and Joachim Klein and Sascha
               Kl{\"{u}}ppelholz and Sascha Wunderlich},
  title     = {Probabilistic Model Checking for Energy-Utility Analysis},
  booktitle = {Horizons of the Mind. A Tribute to Prakash Panangaden},
  series    = {Lecture Notes in Computer Science},
  volume    = {8464},
  publisher = {Springer},
  year      = {2014},
  pages     = {96--123},
  doi       = {10.1007/978-3-319-06880-0_5}
}