### 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.

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.

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 | 37-51 |

ISBN (Trykt) | 9783030302801 |

ISBN (Elektronisk) | 978-3-030-30281-8 |

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 | Storbritannien |

By | Glasgow |

Periode | 10/09/2019 → 12/09/2019 |

Navn | Lecture Notes in Computer Science |
---|---|

Vol/bind | 11785 |

ISSN | 0302-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