-A A +A

Bayes-Adaptive Planning for Data-Efficient Verification of Uncertain Markov Decision Processes

TitleBayes-Adaptive Planning for Data-Efficient Verification of Uncertain Markov Decision Processes
Publication TypeConference Paper
Year of Publication2019
AuthorsWijesuriya VBrian, Abate A
Conference NameQuantitative Evaluation of Systems
PublisherSpringer International Publishing
Conference LocationCham
ISBN Number978-3-030-30281-8

This work concerns discrete-time parametric Markov decision processes. These models encompass the uncertainty in the transitions of partially unknown probabilistic systems with input actions, by parameterising some of the entries in the stochastic matrix. Given a property expressed as a PCTL formula, we pursue a data-based verification approach that capitalises on the partial knowledge of the model and on experimental data obtained from the underlying system: after finding the set of parameters corresponding to model instances that satisfy the property, we quantify from data a measure (a confidence) on whether the system satisfies the property. The contribution of this work is a novel Bayes-Adaptive planning algorithm, which synthesises finite-memory strategies from the model allowing Bayes-Optimal selection of actions. Actions are selected for collecting data, with the goal of increasing its information content that is pertinent to the property of interest: this active learning goal aims at increasing the confidence on whether or not the system satisfies the given property.


Oxford Control and Verification (OXCAV) Group

C/O Department of Computer Science

Wolfson Building, Parks Rd, Oxford OX1 3QD

T: +44 (0) 18656 10767

Education - This is a contributing Drupal Theme
Design by WeebPal.