Energy-Utility Quantiles

Christel BaierChristel Baier, Marcus DaumMarcus Daum, Clemens DubslaffClemens Dubslaff, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Christel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz
Energy-Utility Quantiles
Proc. of the 6th NASA Formal Methods Symposium (NFM), volume 8430 of Lecture Notes in Computer Science, 285--299, 2014. Springer

Details
Bibtex

KurzfassungAbstract
The concept of quantiles is well-known in statistics, but its benefits for the formal quantitative analysis of probabilistic systems have been noticed only recently. To compute quantiles in Markov decision processes where the objective is a probability constraint for an until (i.e., constrained reachability) property with an upper reward bound, an iterative linear-programming (LP) approach has been proposed in a recent paper. We consider here a more general class of quantiles with probability or expectation objectives, allowing to reason about the trade-off between costs in terms of energy and some utility measure. We show how the iterative LP approach can be adapted for these types of quantiles and propose another iterative approach that decomposes the LP to be solved into smaller ones. This algorithm has been implemented and evaluated in case studies for quantiles where the objective is a probability constraint for until properties with upper reward bounds.
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-06200-6_24.

@inproceedings{BDDKK2014,
  author    = {Christel Baier and Marcus Daum and Clemens Dubslaff and Joachim
               Klein and Sascha Kl{\"{u}}ppelholz},
  title     = {Energy-Utility Quantiles},
  booktitle = {Proc. of the 6th {NASA} Formal Methods Symposium (NFM)},
  series    = {Lecture Notes in Computer Science},
  volume    = {8430},
  publisher = {Springer},
  year      = {2014},
  pages     = {285--299},
  doi       = {10.1007/978-3-319-06200-6_24}
}