Parameter Synthesis in Markov Models: A Gentle Survey

arXiv (Cornell University)

Abstract

This paper surveys the analysis of parametric Markov models whose transitions are labelled with functions over a finite set of parameters. These models are symbolic representations of uncountable many concrete probabilistic models, each obtained by instantiating the parameters. We consider various analysis problems for a given logical specification $φ$: do all parameter instantiations within a given region of parameter values satisfy $φ$?, which instantiations satisfy $φ$ and which ones do not?, and how can all such instantiations be characterised, either exactly or approximately? We address theoretical complexity results and describe the main ideas underlying state-of-the-art algorithms that established an impressive leap over the last decade enabling the fully automated analysis of models with millions of states and thousands of parameters.

Authors 3

1. Nils Jansen

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University , Nijmegen , The Netherlands

2. Sebastian Junges

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University , Nijmegen , The Netherlands

3. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany