Data-efficient Bayesian verification of parametric Markov chains

Obtaining complete and accurate models for the formal verification of systems is often hard or impossible. We present a data-based verification approach, for properties expressed in a probabilistic logic, that addresses incomplete model knowledge. We obtain experimental data from a system that can be modelled as a parametric Markov chain. We propose a novel verification algorithm to quantify the confidence the underlying system satisfies a given property of interest by using this data. Given a parameterised model of the system, the procedure first generates a feasible set of parameters corresponding to model instances satisfying a given probabilistic property. Simultaneously, we use Bayesian inference to obtain a probability distribution over the model parameter set from data sampled from the underlying system. The results of both steps are combined to compute a confidence the underlying system satisfies the property. The amount of data required is minimised by exploiting partial knowledge of the system. Our approach offers a framework to integrate Bayesian inference and formal verification, and in our experiments our new approach requires one order of magnitude less data than standard statistical model checking to achieve the same confidence.