Computing quantiles in Markov reward models

DOI10.1007/978-3-642-37075-5_23MaRDI QIDQ4910430zbMATH OpenOpenAlexFDO

Authors Michael Ummels, Christel Baier

Publication date 18 March 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1301.1818

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Abstract: Probabilistic model checking mainly concentrates on techniques for reasoning about the probabilities of certain path properties or expected values of certain random variables. For the quantitative system analysis, however, there is also another type of interesting performance measure, namely quantiles. A typical quantile query takes as input a lower probability bound p and a reachability property. The task is then to compute the minimal reward bound r such that with probability at least p the target set will be reached before the accumulated reward exceeds r. Quantiles are well-known from mathematical statistics, but to the best of our knowledge they have not been addressed by the model checking community so far. In this paper, we study the complexity of quantile queries for until properties in discrete-time finite-state Markov decision processes with non-negative rewards on states. We show that qualitative quantile queries can be evaluated in polynomial time and present an exponential algorithm for the evaluation of quantitative quantile queries. For the special case of Markov chains, we show that quantitative quantile queries can be evaluated in time polynomial in the size of the chain and the maximum reward.

Recommendations

• scientific article; zbMATH DE number 7297838
• Formal Modeling and Analysis of Timed Systems
• Percentile queries in multi-dimensional Markov decision processes
• Performability assessment by model checking of Markov reward models
• Multiphase until formulas over Markov reward models: an algebraic approach

Cited in

(18)

• Symbolically quantifying response time in stochastic models using moments and semirings
• Multi-cost bounded tradeoff analysis in MDP
• Ratio and weight quantiles
• Model Checking Exact Cost for Attack Scenarios
• The odds of staying on budget
• Quantile Markov Decision Processes
• scientific article; zbMATH DE number 7297838 (Why is no real title available?)
• Energy-utility analysis for resilient systems using probabilistic model checking
• Probabilistic model checking for energy-utility analysis
• Percentile queries in multi-dimensional Markov decision processes
• Percentile queries in multi-dimensional Markov decision processes
• Model Checking Constrained Markov Reward Models with Uncertainties
• Positivity-hardness results on Markov decision processes
• Entropic risk for turn-based stochastic games
• On Skolem-hardness and saturation points in Markov decision processes
• Risk-averse optimization of total rewards in Markovian models using deviation measures
• Demonic variance and a non-determinism score for Markov decision processes
• Multiphase until formulas over Markov reward models: an algebraic approach

This page was built for publication: Computing quantiles in Markov reward models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4910430)