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

摘要

We present a new method for statistical verification of quantitativeproperties over a partially unknown system with actions, utilising aparameterised model (in this work, a parametric Markov decision process) anddata collected from experiments performed on the underlying system. We obtainthe confidence that the underlying system satisfies a given property, and showthat the method uses data efficiently and thus is robust to the amount of dataavailable. These characteristics are achieved by firstly exploiting parametersynthesis to establish a feasible set of parameters for which the underlyingsystem will satisfy the property; secondly, by actively synthesisingexperiments to increase amount of information in the collected data that isrelevant to the property; and finally propagating this information over themodel parameters, obtaining a confidence that reflects our belief whether ornot the system parameters lie in the feasible set, thereby solving theverification problem.