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 contribution

Abstract

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
EditorsGul Agha, Benny Van Houdt
Place of PublicationCham
PublisherSpringer International Publishing
Pages35-51
Number of pages17
ISBN (Electronic)978-3-319-43425-4
ISBN (Print)978-3-319-43424-7
DOIs
Publication statusPublished - 3 Aug 2016
Event13th International Conference on Quantitative Evaluation of SysTems - Quebec City, Canada
Duration: 23 Aug 201625 Aug 2016
http://www.qest.org/qest2016/

Publication series

Name Lecture Notes in Computer Science
Volume9826
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Conference on Quantitative Evaluation of SysTems
Abbreviated titleQEST 2016
CountryCanada
CityQuebec City
Period23/08/1625/08/16
Internet address

Fingerprint Dive into the research topics of 'Data-Efficient Bayesian Verification of Parametric Markov Chains'. Together they form a unique fingerprint.

Cite this