Abstract: Probabilistic model checking is a verification technique that has been the focus of intensive research for over a decade. One important issue with probabilistic model checking, which is crucial for its practical significance but is overlooked by the state-of-the-art largely, is the potential discrepancy between a stochastic model and the real-world system it represents when the model is built from statistical data. In the worst case, a tiny but nontrivial change to some model quantities might lead to misleading or even invalid verification results. To address this issue, we present a mathematical characterisation of the consequence of model perturbations on the verification results. The formal model is a parametric variant of discrete-time Markov chains equipped with a vector norm to measure the perturbation. Our main contributions include algorithms and tight complexity bounds for calculating both non-asymptotic bounds and asymptotic bounds with respect to three perturbation distances. This talk is based on a paper presented at Concur’14 and another one conditionally accepted by IEEE Transactions on Software Engineering.

Date: 19 August 2015