Energy-Utility Quantiles

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

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

OriginalspracheEnglisch
TitelNASA Formal Methods
Redakteure/-innenJulia M. Badger, Kristin Yvonne Rozier
Herausgeber (Verlag)Springer, Cham
Seiten285-299
Seitenumfang15
ISBN (Print)978-3-319-06199-3
PublikationsstatusVeröffentlicht - 2014
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 8430
ISSN0302-9743

Konferenz

Titel6th NASA Formal Methods Symposium
KurztitelNFM 2014
Veranstaltungsnummer6
Dauer29 April - 1 Mai 2014
BekanntheitsgradInternationale Veranstaltung
StadtHouston
LandUSA/Vereinigte Staaten

Externe IDs

Scopus 84901649717
ORCID /0000-0002-5321-9343/work/142236742

Schlagworte

Schlagwörter

  • energy-utility, quantiles

Bibliotheksschlagworte