Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes
This addresses the challenge of reliable verification with limited data for researchers and practitioners working with complex systems modeled as parametric Markov decision processes.
The paper tackles the problem of verifying quantitative properties in partially unknown systems with actions using parametric Markov decision processes, achieving data-efficient verification through automated experiment design that provides confidence measures about property satisfaction.
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.