Neural State Classification for Hybrid Systems

TL;DR

This paper introduces Neural State Classification (NSC), a machine learning approach for efficiently classifying states in hybrid systems with high accuracy and low false-negative rates, useful for model checking and safety verification.

Contribution

The paper presents NSC, a novel neural network-based method for state classification in hybrid systems, including techniques for certification and error mitigation.

Findings

Achieved up to 99.98% accuracy on benchmarks

Reduced false-negative rate to 0.0015 after tuning

Demonstrated efficiency and reliability of NSC in practical scenarios

Abstract

We introduce the State Classification Problem (SCP) for hybrid systems, and present Neural State Classification (NSC) as an efficient solution technique. SCP generalizes the model checking problem as it entails classifying each state $s$ of a hybrid automaton as either positive or negative, depending on whether or not $s$ satisfies a given time-bounded reachability specification. This is an interesting problem in its own right, which NSC solves using machine-learning techniques, Deep Neural Networks in particular. State classifiers produced by NSC tend to be very efficient (run in constant time and space), but may be subject to classification errors. To quantify and mitigate such errors, our approach comprises: i) techniques for certifying, with statistical guarantees, that an NSC classifier meets given accuracy levels; ii) tuning techniques, including a novel technique based on adversarial sampling, that can virtually eliminate false negatives (positive states classified as negative), thereby making the classifier more conservative. We have applied NSC to six nonlinear hybrid system benchmarks, achieving an accuracy of 99.25% to 99.98%, and a false-negative rate of 0.0033 to 0, which we further reduced to 0.0015 to 0 after tuning the classifier. We believe that this level of accuracy is acceptable in many practical applications, and that these results demonstrate the promise of the NSC approach.