hide
Free keywords:
cs.SY,Computer Science, Logic in Computer Science, cs.LO,Mathematics, Probability, math.PR,
Abstract:
We study statistical model checking of continuous-time stochastic hybrid
systems. The challenge in applying statistical model checking to these systems
is that one cannot simulate such systems exactly. We employ the multilevel
Monte Carlo method (MLMC) and work on a sequence of discrete-time stochastic
processes whose executions approximate and converge weakly to that of the
original continuous-time stochastic hybrid system with respect to satisfaction
of the property of interest. With focus on bounded-horizon reachability, we
recast the model checking problem as the computation of the distribution of the
exit time, which is in turn formulated as the expectation of an indicator
function. This latter computation involves estimating discontinuous
functionals, which reduces the bound on the convergence rate of the Monte Carlo
algorithm. We propose a smoothing step with tunable precision and formally
quantify the error of the MLMC approach in the mean-square sense, which is
composed of smoothing error, bias, and variance. We formulate a general
adaptive algorithm which balances these error terms. Finally, we describe an
application of our technique to verify a model of thermostatically controlled
loads.
