Analyzing Value Functions of States in Parametric Markov Chains
Kasper Engelen, Guillermo A. Pérez, Shrisha Rao
TL;DR
Parametric Markov chains (pMCs) model probabilistic systems with uncertain probabilities via polynomial transitions in parameters $\boldsymbol{x}$. The paper connects reachability analysis to two key properties—monotonicity and the never-worse relation (NWR)—and shows how monotonicity can be reduced to NWR, enabling efficient tools to detect and exploit monotone behavior. It develops a quasi-polynomial framework for representing value functions and their derivatives using arithmetic circuits, division-free Gaussian elimination, and algebraic branching programs, culminating in a derivative pMC construction that links derivatives to NWR. Empirically, the authors implement an NWR equivalence-class collapse in Storm, show substantial size reductions on several benchmarks, and demonstrate that this preprocessing speeds up monotonicity checks and parameter lifting in many cases, while noting mixed results on some existing benchmarks. Overall, the work provides both theoretical reductions and practical preprocessing techniques that improve parametrized reachability verification and synthesis workflows for pMCs.
Abstract
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.