Skip to main content
Top

2018 | OriginalPaper | Chapter

Neural State Classification for Hybrid Systems

Authors : Dung Phan, Nicola Paoletti, Timothy Zhang, Radu Grosu, Scott A. Smolka, Scott D. Stoller

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
Technically, for v non-injective, \(\overleftarrow{v}\) is in general a nondeterministic reset: \(\overleftarrow{v}: X \xrightarrow {} 2^X\).
 
2
Statistical learning theory [29] provides statistical bounds on the generalization error of learn models, but these bounds are very conservative and thus of little use in practice. We use these bounds, however, in the proof of Theorem 2.
 
Literature
3.
go back to reference Bak, S., et al.: Hybrid automata: from verification to implementation. Int. J. Softw. Tools Technol. Transf. 1–18 (2017) Bak, S., et al.: Hybrid automata: from verification to implementation. Int. J. Softw. Tools Technol. Transf. 1–18 (2017)
14.
go back to reference Garg, P.: Learning invariants using decision trees and implication counterexamples. ACM Sigplan Not. 51(1), 499–512 (2016)CrossRef Garg, P.: Learning invariants using decision trees and implication counterexamples. ACM Sigplan Not. 51(1), 499–512 (2016)CrossRef
16.
go back to reference Henzinger, T.A., et al.: What’s decidable about hybrid automata? In: STOC, pp. 373–382. ACM Press (1995) Henzinger, T.A., et al.: What’s decidable about hybrid automata? In: STOC, pp. 373–382. ACM Press (1995)
17.
go back to reference Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Netw. 2(5), 359–366 (1989)CrossRef Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Netw. 2(5), 359–366 (1989)CrossRef
19.
go back to reference Jin, X., et al.: Powertrain control verification benchmark. In: HSCC, pp. 253–262. ACM Press (2014) Jin, X., et al.: Powertrain control verification benchmark. In: HSCC, pp. 253–262. ACM Press (2014)
20.
go back to reference Kannan, R., Lovász, L., Simonovits, M.: Random walks and an \(o^*(n^5)\) volume algorithm for convex bodies. Random Struct. Algorithms 11(1), 1–50 (1997)MathSciNetCrossRef Kannan, R., Lovász, L., Simonovits, M.: Random walks and an \(o^*(n^5)\) volume algorithm for convex bodies. Random Struct. Algorithms 11(1), 1–50 (1997)MathSciNetCrossRef
23.
go back to reference LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521(7553), 436 (2015)CrossRef LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521(7553), 436 (2015)CrossRef
25.
go back to reference Mitchell, M.: An Introduction to Genetic Algorithms. MIT press, Cambridge (1998) Mitchell, M.: An Introduction to Genetic Algorithms. MIT press, Cambridge (1998)
26.
go back to reference Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S.A., Stoller, S.D.: Neural state classification for hybrid systems. arXiv:1807.09901 (2018) Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S.A., Stoller, S.D.: Neural state classification for hybrid systems. arXiv:​1807.​09901 (2018)
29.
go back to reference Vapnik, V.: The Nature of Statistical Learning Theory. Springer, New York (2013) Vapnik, V.: The Nature of Statistical Learning Theory. Springer, New York (2013)
30.
go back to reference Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multi-layer neural networks. arXiv:1708.03322 (2017) Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multi-layer neural networks. arXiv:​1708.​03322 (2017)
Metadata
Title
Neural State Classification for Hybrid Systems
Authors
Dung Phan
Nicola Paoletti
Timothy Zhang
Radu Grosu
Scott A. Smolka
Scott D. Stoller
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_25

Premium Partner