Reachability Design Through Approximate Bayesian Computation

摘要

Time-bounded reachability problems are concerned with assessing whether a model's trajectories traverse a given region of the state-space within given time-bounds. In the case of stochastic models reachability is associated with a measure of probability which depends on the model's parameters. In this paper we propose a methodology that, given a reachability specification (for a parametric stochastic model), allows for computing a reachability related probability distribution on the parameter space, i.e. a distribution that allows for identifying regions of the parameter space for which there is a non-null probability to match the considered reachability specification. The methodology relies on the characterisation of distance between a model's trajectory and a reachability specification which we show being assessable by using a hybrid automaton as a monitor of a model's trajectory. An automata-based adaptation of the Approximated Bayesian Computation method is then introduced to estimate the reachability distribution on the parameter space.