Accelerating Parametric Probabilistic Verification
This work addresses a computational bottleneck in probabilistic verification for systems with uncertain parameters, offering significant performance improvements.
The paper tackles the problem of computing reachability probabilities for parametric discrete-time Markov chains by introducing a novel algorithm based on graph decomposition and polynomial factorization, achieving speed-ups of up to several orders of magnitude compared to existing methods.
We present a novel method for computing reachability probabilities of parametric discrete-time Markov chains whose transition probabilities are fractions of polynomials over a set of parameters. Our algorithm is based on two key ingredients: a graph decomposition into strongly connected subgraphs combined with a novel factorization strategy for polynomials. Experimental evaluations show that these approaches can lead to a speed-up of up to several orders of magnitude in comparison to existing approaches