Data-efficient Bayesian verification of parametric Markov chains

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

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

10 Citations (Scopus)


Obtaining complete and accurate models for the formal verification of systems is often hard or impossible. We present a data-based verification approach, for properties expressed in a probabilistic logic, that addresses incomplete model knowledge. We obtain experimental data from a system that can be modelled as a parametric Markov chain. We propose a novel verification algorithm to quantify the confidence the underlying system satisfies a given property of interest by using this data. Given a parameterised model of the system, the procedure first generates a feasible set of parameters corresponding to model instances satisfying a given probabilistic property. Simultaneously, we use Bayesian inference to obtain a probability distribution over the model parameter set from data sampled from the underlying system. The results of both steps are combined to compute a confidence the underlying system satisfies the property. The amount of data required is minimised by exploiting partial knowledge of the system. Our approach offers a framework to integrate Bayesian inference and formal verification, and in our experiments our new approach requires one order of magnitude less data than standard statistical model checking to achieve the same confidence.
Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems, QEST 2016
Subtitle of host publication13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings
EditorsG. Agha, B. Van Houdt
Place of PublicationDordrecht
ISBN (Electronic)978-3-319-43425-4
ISBN (Print)978-3-319-43424-7
Publication statusPublished - 2016

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'Data-efficient Bayesian verification of parametric Markov chains'. Together they form a unique fingerprint.

Cite this