Aktiviteter pr. år
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 realvalued 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 quantifierfree firstorder 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.
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 realvalued 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 quantifierfree firstorder 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.
Originalsprog  Engelsk 

Titel  Quantitative Evaluation of Systems  16th International Conference, QEST 2019, Proceedings 
Redaktører  David Parker, Verena Wolf 
Antal sider  15 
Forlag  Springer 
Publikationsdato  1 sep. 2019 
Sider  3751 
ISBN (Trykt)  9783030302801 
ISBN (Elektronisk)  9783030302818 
DOI  
Status  Udgivet  1 sep. 2019 
Begivenhed  16th International Conference on Quantitative Evaluation of Systems, QEST 2019  Glasgow, Storbritannien Varighed: 10 sep. 2019 → 12 sep. 2019 
Konference
Konference  16th International Conference on Quantitative Evaluation of Systems, QEST 2019 

Land/Område  Storbritannien 
By  Glasgow 
Periode  10/09/2019 → 12/09/2019 
Navn  Lecture Notes in Computer Science 

Vol/bind  11785 
ISSN  03029743 
Fingeraftryk
Dyk ned i forskningsemnerne om 'Model checking constrained markov reward models with uncertainties'. Sammen danner de et unikt fingeraftryk.Aktiviteter
 1 Konferenceoplæg

Quantitative Evaluation of Systems (QEST) 2019
Mikkel Hansen (Oplægsholder)
10 sep. 2019 → 12 sep. 2019Aktivitet: Foredrag og mundtlige bidrag › Konferenceoplæg