Energy-Utility Quantiles

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

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 languageEnglish
Title of host publicationNASA Formal Methods
EditorsJulia M. Badger, Kristin Yvonne Rozier
PublisherSpringer, Cham
Pages285-299
Number of pages15
ISBN (print)978-3-319-06199-3
Publication statusPublished - 2014
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 8430
ISSN0302-9743

Conference

Title6th NASA Formal Methods Symposium
Abbreviated titleNFM 2014
Conference number6
Duration29 April - 1 May 2014
Degree of recognitionInternational event
CityHouston
CountryUnited States of America

External IDs

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

Keywords

Keywords

  • energy-utility, quantiles

Library keywords