Ecole d'ingénieur et centre de recherche en Sciences du numérique

Probabilistic model checking for continuous-time Markov chains via sequential bayesian inference

Milios, Dimitrios; Sanguinetti, Guido; Schnoerr, David

QEST 2018, 15th International Conference on Quantitative Evaluation of Systems, September 4-7, 2018, Beijing, China / Also published in LNCS, Vol.11024

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.

Document Doi Arxiv Bibtex

Titre:Probabilistic model checking for continuous-time Markov chains via sequential bayesian inference
Mots Clés:Bayesian inference, Model checking, Moment closure
Type:Conférence
Langue:English
Ville:Beijing
Pays:CHINE
Date:
Département:Data Science
Eurecom ref:5729
Copyright: © Springer. Personal use of this material is permitted. The definitive version of this paper was published in QEST 2018, 15th International Conference on Quantitative Evaluation of Systems, September 4-7, 2018, Beijing, China / Also published in LNCS, Vol.11024 and is available at : https://doi.org/10.1007/978-3-319-99154-2_18
Bibtex: @inproceedings{EURECOM+5729, doi = {https://doi.org/10.1007/978-3-319-99154-2_18}, year = {2018}, title = {{P}robabilistic model checking for continuous-time {M}arkov chains via sequential bayesian inference}, author = {{M}ilios, {D}imitrios and {S}anguinetti, {G}uido and {S}chnoerr, {D}avid}, booktitle = {{QEST} 2018, 15th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems, {S}eptember 4-7, 2018, {B}eijing, {C}hina / {A}lso published in {LNCS}, {V}ol.11024}, address = {{B}eijing, {CHINE}}, month = {09}, url = {http://www.eurecom.fr/publication/5729} }
Voir aussi: