'Neural State Classification' Nicola Paoletti, University of London

Friday, October 12, 2018 - 14:30 to 15:30
NCS 120

Title:Neural State Classification for Hybrid Systems

Abstract:Hybrid automata (HA) are a formal model for systems with mixed continuous and discrete dynamics. As such, HAs are applied to the design of cyber-physical systems, i.e., systems characterized by digital components (discrete) that control and interact with the physical environment (continuous). Application areas include avionics, automotive, medical devices, and robotics. Formal verification of HAs is crucial for such safety-critical applications, as it provides mathematically rigorous proofs of correctness (whether or not the system satisfy a desired specification). This kind of analysis often boils down to reachability checking, that is, verifying whether an unsafe HA state can be reached from an initial set of states. Online reachability analysis of HAs is very important to ensure correctness at runtime. State-of-the-art reachability techniques are, however, not suitable for online analysis due to their large computational footprint (but only for offline, design-time, analysis).In this work, we present Neural State Classification (NSC), an efficient solution to the State Classification Problem (SCP), that is, the problem of classifying each state of an HA as either positive or negative, depending on whether or not it satisfies a given reachability specification.

In NSC, state classifiers are represented by Deep Neural Networks, which are computationally very efficient and thus, suitable for online analysis, 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 classifiers. We believe that this level of accuracy is acceptable in many practical applications, and that these results demonstrate the promise of the NSC approach.

This is a joint work with Dung Phan, Timothy Zhang, Scott A. Smolka, and Scott D. Stoller from Stony Brook University and Radu Grosu from TU Wien.

Bio:Nicola Paoletti is a lecturer at the Computer Science Department of Royal Holloway, University of London (UK). He was previously a post-doc in the Department of Computer Science of Stony Brook University (USA) working in Prof Scott Smolka's group. Prior to that, he was a post-doc in Prof Marta Kwiatkowska's group at the Department of Computer Science of Oxford University, following an internship in the Biological Computation group of Microsoft Research Cambridge. He obtained his PhD from the University of Camerino (Italy) in 2014.His research interests include verification, control, and synthesis of stochastic and hybrid systems, with application to safety assurance of medical devices and analysis of biological systems. On these topics, he co-authored 30+ papers, obtaining three best paper awards, the "best PhD student" award from the University of Camerino, and several presentation awards.

Computed Event Type: 
Event Title: 
'Neural State Classification' Nicola Paoletti, University of London