# Analyzing Value Functions of States in Parametric Markov Chains

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 33 references that are in the map.
- First posted on arXiv 23 Apr 2025.

## Builds on (most cited first, 8 of 8)

- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination](https://mlsanity.com/paper/1709.02093/) (2017)
- [The Complexity of Reachability in Parametric Markov Decision Processes](https://mlsanity.com/paper/2009.13128/) (2020)
- [Are Parametric Markov Chains Monotonic?](https://mlsanity.com/paper/1907.08491/) (2019)
- [Gradient-Descent for Randomized Controllers under Partial Observability](https://mlsanity.com/paper/2111.04407/) (2021)
- [Reachability in Augmented Interval Markov Chains](https://mlsanity.com/paper/1701.02996/) (2017)
- [The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes](https://mlsanity.com/paper/1710.07903/) (2017)
- [Graph-Based Reductions for Parametric and Weighted MDPs](https://mlsanity.com/paper/2305.05739/) (2023)

## Abstract (arXiv)

Parametric Markov chains (pMC) are used to model probabilistic systems with unknown or partially known probabilities. Although (universal) pMC verification for reachability properties is known to be coETR-complete, there have been efforts to approach it using potentially easier-to-check properties such as asking whether the pMC is monotonic in certain parameters. In this paper, we first reduce monotonicity to asking whether the reachability probability from a given state is never less than that of another given state. Recent results for the latter property imply an efficient algorithm to collapse same-value equivalence classes, which in turn preserves verification results and monotonicity. We implement our algorithm to collapse "trivial" equivalence classes in the pMC and show empirical evidence for the following: First, the collapse gives reductions in size for some existing benchmarks and significant reductions on some custom benchmarks; Second, the collapse speeds up existing algorithms to check monotonicity and parameter lifting, and hence can be used as a fast pre-processing step in practice.