Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems

TL;DR

This paper develops a method to compute asymptotic bounds on reachability probabilities in perturbed parametric probabilistic models, aiding in understanding the robustness of such systems under small distributional changes.

Contribution

It introduces a novel approach to calculate condition numbers for reachability probabilities in parametric Markov chains with respect to distribution perturbations.

Findings

Method effectively computes bounds for real systems

Experiments demonstrate practical applicability

Provides insights into system robustness under perturbations

Abstract

The majority of existing probabilistic model checking case studies are based on well understood theoretical models and distributions. However, real-life probabilistic systems usually involve distribution parameters whose values are obtained by empirical measurements and thus are subject to small perturbations. In this paper, we consider perturbation analysis of reachability in the parametric models of these systems (i.e., parametric Markov chains) equipped with the norm of absolute distance. Our main contribution is a method to compute the asymptotic bounds in the form of condition numbers for constrained reachability probabilities against perturbations of the distribution parameters of the system. The adequacy of the method is demonstrated through experiments with the Zeroconf protocol and the hopping frog problem.