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

TL;DR

This paper introduces a novel Bayesian inference approach to probabilistic model checking of continuous-time Markov chains, enabling efficient and accurate analysis of time-bounded properties with significant computational improvements.

Contribution

It reformulates model checking as a Bayesian inference problem and applies machine learning techniques for efficient approximation, outperforming traditional statistical methods.

Findings

Achieves high accuracy in verifying time-bounded properties.

Provides significant computational speed-ups over existing methods.

Demonstrates effectiveness on complex case studies.

Abstract

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.