Parameter Synthesis for Markov Models: Covering the Parameter Space

TL;DR

This paper develops algorithms and a software tool for analyzing parametric Markov models to synthesize parameter values that meet safety or performance specifications, addressing the challenge of uncertain or partially known probabilities.

Contribution

It introduces new analysis algorithms for parametric Markov models, including methods for parameter space coverage and synthesis, with an extensive experimental evaluation.

Findings

Algorithms effectively identify parameter regions satisfying specifications.

The software tool successfully applies techniques to diverse benchmarks.

Results demonstrate practical applicability in system safety and performance analysis.

Abstract

Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not -- or only partially -- known. This motivates considering parametric models with transitions labeled with functions over parameters. Whereas traditional Markov chain analysis relies on a single, fixed set of probabilities, analysing parametric Markov models focuses on synthesising parameter values that establish a given safety or performance specification $\varphi$. Examples are: what component failure rates ensure the probability of a system breakdown to be below 0.00000001?, or which failure rates maximise the performance, for instance the throughput, of the system? This paper presents various analysis algorithms for parametric discrete-time Markov chains and Markov decision processes. We focus on three problems: (a) do all parameter values within a given region satisfy $\varphi$?, (b) which regions satisfy $\varphi$ and which ones do not?, and (c) an approximate version of (b) focusing on covering a large fraction of all possible parameter values. We give a detailed account of the various algorithms, present a software tool realising these techniques, and report on an extensive experimental evaluation on benchmarks that span a wide range of applications.