Analyzing Value Functions of States in Parametric Markov Chains
This is an incremental improvement for researchers and practitioners working on probabilistic system verification, offering a preprocessing step to enhance efficiency.
The paper tackles the problem of verifying parametric Markov chains by developing an algorithm to collapse states with identical reachability probabilities, which reduces model size and speeds up existing verification algorithms. Empirical results show significant reductions on custom benchmarks and faster monotonicity checking.
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.