# Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination

arXiv: https://arxiv.org/abs/1709.02093 · HTML: https://mlsanity.com/paper/1709.02093/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Sep 2017.

## Built on by (most cited first, 11 of 11)

- [Convex Optimization for Parameter Synthesis in MDPs](https://mlsanity.com/paper/2107.00108/) (2021)
- [Fine-Tuning the Odds in Bayesian Networks](https://mlsanity.com/paper/2105.14371/) (2021)
- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [Data-Efficient Safe Policy Improvement Using Parametric Structure](https://mlsanity.com/paper/2507.15532/) (2025)
- [Lecture Notes on Partially Known MDPs](https://mlsanity.com/paper/2112.02976/) (2021)
- [Analyzing Value Functions of States in Parametric Markov Chains](https://mlsanity.com/paper/2504.17020/) (2025)
- [Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI](https://mlsanity.com/paper/2604.19431/) (2026)
- [Robustness Analysis of POMDP Policies to Observation Perturbations](https://mlsanity.com/paper/2604.21256/) (2026)
- [PAC Approximation and DIRECT Optimization for Parametric Markov Models](https://mlsanity.com/paper/2608.02184/) (2026)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)

## Abstract (arXiv)

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.