Verification of Markov chains with ML-computed probabilities and rewards becomes a global optimization problem that a decomposition and bound propagation scheme solves, often hundreds of times faster than direct solving.
Exact sensitivity analysis of Markov reward processes via algebraic geometry
1 Pith paper cite this work. Polarity classification is still indexing.
abstract
We introduce a new approach for deterministic sensitivity analysis of Markov reward processes, commonly used in cost-effectiveness analyses, via reformulation into a polynomial system. Our approach leverages cylindrical algebraic decomposition (CAD), a technique arising from algebraic geometry that provides an exact description of all solutions to a polynomial system. While it is typically intractable to build a CAD for systems with more than a few variables, we show that a special class of polynomial systems, which includes the polynomials arising from Markov reward processes, can be analyzed much more tractably. We establish several theoretical results about such systems and develop a specialized algorithm to construct their CAD, which allows us to perform exact, multi-way sensitivity analysis for common health economic analyses. We develop an open-source software package that implements our algorithm. Finally, we apply it to two case studies, one with synthetic data and one that re-analyzes a previous cost-effectiveness analysis from the literature, demonstrating advantages of our approach over standard techniques. Our software and code are available at: \url{https://github.com/mmaaz-git/markovag}.
citation-role summary
citation-polarity summary
fields
cs.LG 1years
2025 1verdicts
CONDITIONAL 1roles
background 1polarities
background 1representative citing papers
citing papers explorer
-
Formal Verification of Markov Processes with Learned Parameters
Verification of Markov chains with ML-computed probabilities and rewards becomes a global optimization problem that a decomposition and bound propagation scheme solves, often hundreds of times faster than direct solving.