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.
CITATION STYLE
Milios, D., Sanguinetti, G., & Schnoerr, D. (2018). Probabilistic model checking for continuous-time markov chains via sequential bayesian inference. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11024 LNCS, pp. 289–305). Springer Verlag. https://doi.org/10.1007/978-3-319-99154-2_18
Mendeley helps you to discover research relevant for your work.