Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes

TL;DR

This paper introduces an efficient data-driven method for verifying properties of systems modeled as parametric Markov decision processes, combining parameter synthesis and active experiment design to improve confidence in verification results.

Contribution

It presents a novel approach that integrates parameter synthesis with active experiment design for data-efficient verification of parametric MDPs.

Findings

Method effectively uses data to verify system properties.

Approach improves confidence with fewer experiments.

Robust to limited data availability.

Abstract

We present a new method for statistical verification of quantitative properties over a partially unknown system with actions, utilising a parameterised model (in this work, a parametric Markov decision process) and data collected from experiments performed on the underlying system. We obtain the confidence that the underlying system satisfies a given property, and show that the method uses data efficiently and thus is robust to the amount of data available. These characteristics are achieved by firstly exploiting parameter synthesis to establish a feasible set of parameters for which the underlying system will satisfy the property; secondly, by actively synthesising experiments to increase amount of information in the collected data that is relevant to the property; and finally propagating this information over the model parameters, obtaining a confidence that reflects our belief whether or not the system parameters lie in the feasible set, thereby solving the verification problem.