Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference

Dimitrios Milios, Guido Sanguinetti, David Schnoerr

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

Abstract / Description of output

Probabilistic model checking for systems with large or unbounded state space is a challenging computational problem in formal modelling and its applications. Numerical algorithms require an explicit representation of the state space, while statistical approaches require a large number of samples to estimate the desired properties with high confidence. Here, we show how model checking of time-bounded path properties can be recast exactly as a Bayesian inference problem. In this novel formulation the problem can be efficiently approximated using techniques from machine learning. Our approach is inspired by a recent result in statistical physics which derived closed-form differential equations for the first-passage time distribution of stochastic processes. We show on a number of non-trivial case studies that our method achieves both high accuracy and significant computational gains compared to statistical model checking.
Original languageEnglish
Title of host publication15th International Conference on Quantitative Evaluation of SysTems (QEST 2018)
Place of PublicationBeijing, China
PublisherSpringer, Cham
Pages289-305
Number of pages17
ISBN (Electronic)978-3-319-99154-2
ISBN (Print)978-3-319-99153-5
DOIs
Publication statusPublished - 2018
Event15th International Conference on Quantitative Evaluation of SysTems - Beijing, China
Duration: 4 Sept 20187 Sept 2018
http://www.qest.org/qest2018/index.html

Publication series

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

Conference

Conference15th International Conference on Quantitative Evaluation of SysTems
Abbreviated titleQEST 2018
Country/TerritoryChina
CityBeijing
Period4/09/187/09/18
Internet address

Fingerprint

Dive into the research topics of 'Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference'. Together they form a unique fingerprint.

Cite this