Automated experiment design for data-efficient verification of parametric Markov decision processes

E. Polgreen, V. Wijesuriya, S. Haesaert, A. Abate

Research output: Contribution to journalArticleAcademic

75 Downloads (Pure)


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.
Original languageEnglish
Article number1707.01322
Number of pages18, e-Print Archive, Physics
Issue number1707.01322v1
Publication statusPublished - 5 Jul 2017

Fingerprint Dive into the research topics of 'Automated experiment design for data-efficient verification of parametric Markov decision processes'. Together they form a unique fingerprint.

  • Cite this