Reference

Parameter Synthesis in Markov Models: A Gentle Survey, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday(2022)

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 $$\varphi $$φ: do all parameter instantiations within a given region of parameter values satisfy $$\varphi $$φ?, which instantiations satisfy $$\varphi $$φ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.