Parameter Synthesis in Markov Models: A Gentle Survey

TL;DR

This survey reviews methods for analyzing parametric Markov models, focusing on logical specifications, complexity results, and algorithms that enable automated analysis of large models with many parameters.

Contribution

It provides a comprehensive overview of recent advances in parameter synthesis for Markov models, highlighting new algorithms and complexity insights.

Findings

Algorithms enable analysis of models with millions of states

New complexity results clarify problem difficulty

Automated tools now handle thousands of parameters

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.