We introduce the State Classification Problem (SCP) for continuous and 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.
In Proc. of ATVA'18, the 16th International Symposium on Automated Technology for Verification and Analysis, Los Angeles, California, USA, October, 2018, LNCS.
*This work was partially supported by the NSF-Frontiers Cyber-Cardia
Award, the US-AFOSR Arrive Award, the EU-Artemis EMC2 Award, the
EU-Ecsel Semi40 Award, the EU-Ecsel Productive 4.0 Award, the
AT-FWF-NFN RiSE Award, the AT-FWF-LogicCS-DC Award, the AT-FFG
Harmonia Award, the AT-FFG Em2Apps Award, and the TUW-CPPS-DK Award.