Energy-Utility Quantiles
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
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.
Details
Original language | English |
---|---|
Title of host publication | NASA Formal Methods |
Editors | Julia M. Badger, Kristin Yvonne Rozier |
Publisher | Springer, Cham |
Pages | 285-299 |
Number of pages | 15 |
ISBN (print) | 978-3-319-06199-3 |
Publication status | Published - 2014 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 8430 |
---|---|
ISSN | 0302-9743 |
Conference
Title | 6th NASA Formal Methods Symposium |
---|---|
Abbreviated title | NFM 2014 |
Conference number | 6 |
Duration | 29 April - 1 May 2014 |
Degree of recognition | International event |
City | Houston |
Country | United States of America |
External IDs
Scopus | 84901649717 |
---|---|
ORCID | /0000-0002-5321-9343/work/142236742 |
ORCID | /0000-0003-1724-2586/work/165453606 |
Keywords
Keywords
- energy-utility, quantiles