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

Elizabeth Polgreen, Viraj B. Wijesuriya, Sofie Haesaert, Alessandro Abate

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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
EditorsNathalie Bertrand, Luca Bortolussi
Place of PublicationCham
PublisherSpringer
Pages259-274
Number of pages16
ISBN (Electronic)978-3-319-66335-7
ISBN (Print)978-3-319-66334-0
DOIs
Publication statusPublished - 11 Aug 2017
Event14th International Conference on Quantitative Evaluation of Systems - Berlin, Germany
Duration: 5 Sept 20177 Sept 2017
http://www.qest.org/qest2017/

Publication series

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

Conference

Conference14th International Conference on Quantitative Evaluation of Systems
Abbreviated titleQEST 2017
Country/TerritoryGermany
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