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

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)
1 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems
Subtitle of host publication14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings
EditorsN. Bertrand, L. Bortolussi
Place of PublicationDordrecht
PublisherSpringer
Pages259-274
Number of pages16
ISBN (Print)9783319663340
DOIs
Publication statusPublished - 2017
Event14th International Conference on Quantitative Evaluation of Systems (QEST 2017), September 5-7, 2017, Berlin, Germany - Harnack House, Berlin, Germany
Duration: 5 Sep 20177 Sep 2017
http://www.qest.org/qest2017/

Publication series

NameLecture Notes in Computer Science
Volume10503
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Conference on Quantitative Evaluation of Systems (QEST 2017), September 5-7, 2017, Berlin, Germany
Abbreviated titleQEST 2017
CountryGermany
CityBerlin
Period5/09/177/09/17
Internet address

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

    Polgreen, E., Wijesuriya, V. B., Haesaert, S., & Abate, A. (2017). Automated experiment design for data-efficient verification of parametric Markov decision processes. In N. Bertrand, & L. Bortolussi (Eds.), Quantitative Evaluation of Systems: 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings (pp. 259-274). (Lecture Notes in Computer Science; Vol. 10503). Springer. https://doi.org/10.1007/978-3-319-66335-7_16