2022/07/14 by Jansen, Nils, Junges, Sebastian, Katoen, Joost-Pieter · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2207.06801
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.