Robust Policy Optimization and Verification with Moment-Based Distributional Constraints

Verification and adaptation methods based on probabilistic model checking for self-adaptive systems traditionally focus on expected values of system properties, which can mask rare but critical outcomes and lead to control policies that optimize average performance but behave poorly in the tail. Existing distributional probabilistic model checking methods typically rely on arbitrary discretization of reward distributions, with limited guarantees for continuous-valued rewards and poor scalability when propagating full distributions for policy optimization in MDPs. Building upon our prior moment-based verification framework for DTMCs [26], we introduce a robust policy optimization method for MDPs that uses moment-based bounds on distributional tail probabilities to enforce chance constraints while optimizing expected cumulative reward. Our approach computes analytical moments of cumulative rewards via first-step analysis and MGF-based recurrences. We then use the moment-based Cantelli bound to obtain a conservative and differentiable surrogate for the non-smooth chance constraint using only a finite number of moments, and use this surrogate to guide policy optimization with conservative probabilistic guarantees. Experimental evaluation on PRISM MDP benchmarks demonstrates that our Cantelli-based value iteration achieves risk-sensitive performance comparable to distributional baselines while reducing runtime by up to 100 \(\times\) and supporting continuous-valued rewards without binning.