  We show how machine-learning techniques, particularly neural networks, offer
a very effective and highly efficient solution to the approximate
model-checking problem for continuous and hybrid systems, a solution where the
general-purpose model checker is replaced by a model-specific classifier
trained by sampling model trajectories. To the best of our knowledge, we are
the first to establish this link from machine learning to model checking. Our
method comprises a pipeline of analysis techniques for estimating and obtaining
statistical guarantees on the classifier's prediction performance, as well as
tuning techniques to improve such performance. Our experimental evaluation
considers the time-bounded reachability problem for three well-established
benchmarks in the hybrid systems community. On these examples, we achieve an
accuracy of 99.82% to 100% and a false-negative rate (incorrectly predicting
that unsafe states are not reachable from a given state) of 0.0007 to 0. We
believe that this level of accuracy is acceptable in many practical
applications and we show how the approximate model checker can be made more
conservative by tuning the classifier through further training and selection of
the classification threshold.
