I will present a novel tool, U-check, that performs statistical model checking of uncertain Continuous Time Markov Chains. The focus will be mostly on the theoretical ideas underpinning it, which are based on combining state-of-the-art Machine Learning statistical tools with verification.

Uncertain CTMC are Markov Chains whose rates depend on some fixed parameter, whose precise value is unknown, but is assumed to lie in a bounded interval. The first problem we face is how to estimate the satisfaction probability of a linear temporal logic property under such uncertainty. We will show how we can reconstruct the functional dependency of the satisfaction probability on unknown parameters using Machine Learning techniques based on Gaussian Processes, which offer a flexible framework for regression and classification. We dubbed this approach Smoothed Model Checking.