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.

翻译：马尔可夫链分析是形式化验证中的关键技术。一个实际障碍在于马尔可夫模型中的所有概率需已知。然而，系统参数如故障率或丢包率等常常未知——或仅部分已知。这促使我们考虑参数化模型，其转移标注有参数函数。传统马尔可夫链分析依赖于单一固定的概率集，而分析参数化马尔可夫模型则聚焦于综合满足给定安全或性能规约$\varphi$的参数值。例如：何种组件故障率能保证系统崩溃概率低于0.00000001？或何种故障率能最大化系统性能（如吞吐量）？本文提出了面向参数化离散时间马尔可夫链和马尔可夫决策过程的多种分析算法。我们重点关注三个问题：(a)给定区域内所有参数值是否满足$\varphi$？(b)哪些区域满足$\varphi$，哪些不满足？以及(c)问题(b)的近似版本，侧重于覆盖尽可能多的参数值。我们详细阐述了各类算法，介绍了实现这些技术的软件工具，并报告了在涵盖广泛应用的基准测试上的大量实验评估结果。