Model checking constrained markov reward models with uncertainties

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

Abstrakt

We study the problem of analysing Markov reward models (MRMs) in the presence of imprecise or uncertain rewards. Properties of interests for their analysis are (i) probabilistic bisimilarity, and (ii) specifications expressed as probabilistic reward CTL formulae.

We consider two extensions of the notion of MRM, namely (a) constrained Markov reward models, i.e., MRMs with rewards parametric on a set variables subject to some constraints, and (b) stochastic Markov reward models, i.e., MRMs with rewards modelled as real-valued random variables as opposed to precise rewards. Our approach is based on quantifier elimination for linear real arithmetic. Differently from existing solutions for parametric Markov chains, we avoid the manipulation of rational functions in favour of a symbolic representation of the set or parameter valuations satisfying a given property in the form of a quantifier-free first-order formula in the linear theory of the reals.

Our work finds applications in model repair, where parameters need to be tuned so as to satisfy the desired specification, as well as in robustness analysis in the presence of stochastic perturbations.
OriginalsprogEngelsk
TitelQuantitative Evaluation of Systems - 16th International Conference, QEST 2019, Proceedings
RedaktørerDavid Parker, Verena Wolf
Antal sider15
ForlagSpringer
Publikationsdato1 sep. 2019
Sider37-51
ISBN (Trykt)9783030302801
ISBN (Elektronisk)978-3-030-30281-8
DOI
StatusUdgivet - 1 sep. 2019
Begivenhed16th International Conference on Quantitative Evaluation of Systems, QEST 2019 - Glasgow, Storbritannien
Varighed: 10 sep. 201912 sep. 2019

Konference

Konference16th International Conference on Quantitative Evaluation of Systems, QEST 2019
LandStorbritannien
ByGlasgow
Periode10/09/201912/09/2019
NavnLecture Notes in Computer Science
Vol/bind11785
ISSN0302-9743

    Fingerprint

Citationsformater

Bacci, G., Hansen, M., & Larsen, K. G. (2019). Model checking constrained markov reward models with uncertainties. I D. Parker, & V. Wolf (red.), Quantitative Evaluation of Systems - 16th International Conference, QEST 2019, Proceedings (s. 37-51). Springer. Lecture Notes in Computer Science, Bind. 11785 https://doi.org/10.1007/978-3-030-30281-8_3