Browse wiki
From International Center for Computational Logic
The concept of quantiles is well-known in … 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.until properties with upper reward bounds. +
@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}
}
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}
}
Baier +
Christel +
Christel Baier, Marcus Daum, Clemens Dubsl … Christel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz<br/> '''[[Inproceedings3777721029|<b>Energy-Utility Quantiles</b>]]''' <br/>__NOTOC__<i>Proc. of the 6th NASA Formal Methods Symposium (NFM)</i>, volume 8430 of Lecture Notes in Computer Science, 285--299, 2014. Springer<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Inproceedings3777721029|Details]]ngs3777721029|Details]] +
Christel Baier, Marcus Daum, Clemens Dubsl … Christel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz<br/> '''[[Inproceedings3777721029/en|<b>Energy-Utility Quantiles</b>]]''' <br/>__NOTOC__<i>Proc. of the 6th NASA Formal Methods Symposium (NFM)</i>, volume 8430 of Lecture Notes in Computer Science, 285--299, 2014. Springer<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Inproceedings3777721029|Details]]ngs3777721029|Details]] +
Display title of"Display title of" is a predefined property that can assign a distinct display title to an entity and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
Energy-Utility Quantiles +
Modification date"Zuletzt geändert <span style="font-size:small;">(Modification date)</span>" is a predefined property that corresponds to the date of the last modification of a subject and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
5. März 2025, 13:43:16 +
Has query"Hat Abfrage <span style="font-size:small;">(Has query)</span>" is a predefined property that represents meta information (in form of a <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">subobject</a>) about individual queries and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
