Artificial states generation in state spaces using kernel density estimation

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Abstract

The objective is to improve Spot, a model checking library. Spot deals with a specific kind of graph in which each state is a set of variables with given values. These values can be seen as coordinates and a state can therefore be seen as a N-dimensional point. The state space is then a N-dimensional cloud and Spot does a depth first search on it. We want to generate states on the fly to improve the performances. For that, we use a kernel probability density estimation. The generated states are then used as starting points for threads which will explore the state space in parallel.