Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
| Autor: | David Schnoerr, Guido Sanguinetti, Dimitrios Milios |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Model checking
Markov chain Computer science business.industry 0102 computer and information sciences Bayesian inference Machine learning computer.software_genre 01 natural sciences Variable-order Bayesian network Bayesian statistics 010201 computation theory & mathematics 0103 physical sciences Variable elimination Artificial intelligence Graphical model Computational problem 010306 general physics business Algorithm computer |
| Zdroj: | Quantitative Evaluation of Systems ISBN: 9783319991535 QEST |
| DOI: | 10.1007/978-3-319-99154-2_18 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|