Parameter synthesis for Markov models: covering the parameter space
Formal Methods in System Design, vol. 62, pp. 181–259
Abstract
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.
Authors 7
-
Affiliation as printed
Radboud University, Nijmegen, The Netherlands
-
Affiliation as printed
Department of Computer Science, RWTH Aachen University, Aachen, Germany
-
Affiliation as printed
Department of Computer Science, RWTH Aachen University, Aachen, Germany
-
Nils Jansen corresponding
Radboud University Nijmegen · Ruhr University Bochum
Affiliation as printed
Radboud University, Nijmegen, The Netherlands
Ruhr-University, Bochum, Germany
-
Affiliation as printed
Department of Computer Science, RWTH Aachen University, Aachen, Germany
-
Affiliation as printed
Department of Computer Science, RWTH Aachen University, Aachen, Germany
-
Eindhoven University of Technology
Affiliation as printed
Eindhoven University of Technology, Eindhoven, The Netherlands
Cited by 20 stored of 20
20 results
No patents citing this paper on Lens.org (checked 2026-10-06).