Skip to main content

Neural State Classification for Hybrid Systems

Seminar by Nicola Paoletti

  • Date 04 Jun 2019
  • Time 3.00pm-4.00pm
  • Category

Neural State Classification for Hybrid Systems

Hybrid Automata (HA) are applied to the design of numerous safety-critical cyber-physical systems, from avionics to medical devices. Formal reachability checking of HAs is thus crucial to derive rigorous proofs of correctness, but current algorithms are computationally very expensive, and therefore, limited to design-time (offline) analysis. This work is motivated by the need to make HA reachability checking more efficient and suitable for online analysis. This is an example of how machine learning can be employed to speed-up complex verification tasks if we are willing to trade strong correctness guarantees (which nevertheless are often only valid at design-time but not at runtime) with approximate verification methods, as long as their error can be formally established.

In the first part of the talk, I will discuss a recently published method called Neural State Classifications (NSC) [1], an approach for approximating reachability checking using deep neural networks (DNNs). In NSC, we train, using examples computed via HA model checkers, DNN-based state classifiers that approximate the result of reachability checking with very high accuracy, classifying an HA state as positive or negative depending on whether or not it satisfies a given bounded reachability specification. DNN-based state classifiers are computationally efficient and suitable for online analysis but may be subject to classification errors, the most important being false negatives (positive states classified as negative). To quantify and mitigate such errors, the approach comprises techniques for certifying, with statistical guarantees, that an NSC classifier meets given accuracy levels; and a newly introduced method for reducing false negatives, based on retraining the network with inputs found by adversarial sampling. In our experiments on six nonlinear HA benchmarks, NSC achieved an accuracy of 99.25% to 99.98%, and a false-negative rate of 0.0033 to 0, further reduced to 0.0015 to 0 after adversarial sampling-based retraining.

In the second part of the talk, I will discuss ongoing research that extends NSC to provide a priori estimates of single-point prediction uncertainty. This is crucial at runtime to flag potential prediction errors without knowing the true reachability value of the inspected state. For this purpose, we apply inductive conformal prediction (iCP), a method that provides statistical guarantees on the predictions of machine learning models. Through iCP, we show how to derive a principled criterion to reject potentially erroneous predictions. This criterion is highly efficient (and thus, applicable at runtime) and effective, managing in our experiments to successfully reject almost all the wrong NSC predictions.

I will conclude the talk with some open problems in NSC.

[1] Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S. A., & Stoller, S. D. (2018). Neural state classification for hybrid systems. In International Symposium on Automated Technology for Verification and Analysis (pp. 422-440).


Nicola Paoletti

Related topics

Explore Royal Holloway

Get help paying for your studies at Royal Holloway through a range of scholarships and bursaries.

There are lots of exciting ways to get involved at Royal Holloway. Discover new interests and enjoy existing ones

Heading to university is exciting. Finding the right place to live will get you off to a good start

Whether you need support with your health or practical advice on budgeting or finding part-time work, we can help

Discover more about our 21 departments and schools

Find out why Royal Holloway is in the top 25% of UK universities for research rated ‘world-leading’ or ‘internationally excellent’

Royal Holloway is a research intensive university and our academics collaborate across disciplines to achieve excellence.

Discover world-class research at Royal Holloway

Discover more about who we are today, and our vision for the future

Royal Holloway began as two pioneering colleges for the education of women in the 19th century, and their spirit lives on today

We’ve played a role in thousands of careers, some of them particularly remarkable

Find about our decision-making processes and the people who lead and manage Royal Holloway today