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 language | English |
---|---|
Title of host publication | Quantitative Evaluation of Systems |
Editors | Nathalie Bertrand, Luca Bortolussi |
Place of Publication | Cham |
Publisher | Springer |
Pages | 259-274 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-319-66335-7 |
ISBN (Print) | 978-3-319-66334-0 |
DOIs | |
Publication status | Published - 11 Aug 2017 |
Event | 14th International Conference on Quantitative Evaluation of Systems - Berlin, Germany Duration: 5 Sept 2017 → 7 Sept 2017 http://www.qest.org/qest2017/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer, Cham |
Volume | 10503 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 14th International Conference on Quantitative Evaluation of Systems |
---|---|
Abbreviated title | QEST 2017 |
Country/Territory | Germany |
City | Berlin |
Period | 5/09/17 → 7/09/17 |
Internet address |