参数马尔可夫链：PCTL复杂性和无分数高斯消去
Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination
摘要：
参数马尔可夫链已被引入作为依赖于相同的图结构，但在具体的转移概率不同的随机系统的家庭的模型。后者由参数的多项式约束指定。在参数马尔可夫链的分析中通常处理的任务是（1）计算可达性概率和其他定量度量的封闭形式的解决方案，以及（2）找到给定时间逻辑公式适用的参数赋值集的符号表示，以及（3）（2）的决策变量。它询问是否存在时间逻辑公式成立的参数赋值。我们对（1）的贡献是表明，在参数马尔可夫链中计算可达概率或期望成本的有理函数的现有实现可以通过使用无分数高斯消去法来改进，这是一种用于具有参数系数的线性方程系统的长期已知技术。我们对（2）和（3）的贡献是对参数马尔可夫链和概率计算树逻辑（PCTL）公式的模型检验问题的复杂性理论讨论。我们给出了（2）的指数时间算法和（3）的PSPACE上界。此外，我们确定片段的PCTL和子类的参数马尔可夫链（1）和（3）是可解的多项式时间和建立NP-硬度的其他PCTL片段。
英文摘要：
Parametric Markov chains have been introduced as a model for families of stochastic systems that rely on the same graph structure, but differ in the concrete transition probabilities. The latter are specified by polynomial constraints for the parameters. Among the tasks typically addressed in the analysis of parametric Markov chains are (1) the computation of closed-form solutions for reachabilty probabilities and other quantitative measures and (2) finding symbolic representations of the set of parameter valuations for which a given temporal logical formula holds as well as (3) the decision variant of (2) that asks whether there exists a parameter valuation where a temporal logical formula holds. Our contribution to (1) is to show that existing implementations for computing rational functions for reachability probabilities or expected costs in parametric Markov chains can be improved by using fraction-free Gaussian elimination, a long-known technique for linear equation systems with parametric coefficients. Our contribution to (2) and (3) is a complexity-theoretic discussion of the model checking problem for parametric Markov chains and probabilistic computation tree logic (PCTL) formulas. We present an exponential-time algorithm for (2) and a PSPACE upper bound for (3). Moreover, we identify fragments of PCTL and subclasses of parametric Markov chains where (1) and (3) are solvable in polynomial time and establish NP-hardness for other PCTL fragments.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
