Parametric Markov chains (pMCs) are Markov chains (MCs) with symbolic probabilities. A pMC encodes a family of MCs, where each member is obtained by replacing parameters with constants. The parameters allow encoding dependencies between transitions, which sets pMCs apart from interval MCs. The verification problem for pMCs asks whether each MC in the corresponding family satisfies a given temporal specification. The state-of-the-art approach for this problem is parameter lifting (PL) -- an abstraction-refinement loop that abstracts the pMC to a non-parametric model analyzed with standard probabilistic model checking techniques. This paper presents two key improvements to tackle the main limitations of PL. First, we introduce generalized parameter lifting (GPL) to lift various restrictive assumptions made by PL. Second, we present a big-step transformation algorithm that reduces parameter dependencies in pMCs and, therefore, results in tighter approximations. Experiments show that GPL is widely applicable and that the big-step transformation accelerates pMC verification by up to orders of magnitude.

翻译：参数化马尔可夫链（pMC）是带有符号概率的马尔可夫链（MC）。一个pMC编码了一个MC族，其中每个成员通过将参数替换为常数得到。参数允许编码转移之间的依赖关系，这使pMC区别于区间MC。pMC的验证问题询问对应族中的每个MC是否满足给定的时序规约。该问题的最先进方法是参数提升（PL）——一种抽象-精化循环，它将pMC抽象为非参数模型，并使用标准概率模型检验技术进行分析。本文提出了两项关键改进以应对PL的主要局限。首先，我们引入广义参数提升（GPL）以解除PL所作的各种限制性假设。其次，我们提出一种大步变换算法，该算法能减少pMC中的参数依赖，从而得到更紧致的近似。实验表明，GPL具有广泛适用性，且大步变换能将pMC验证速度提升高达数个数量级。