Advertisement

Neural State Classification for Hybrid Systems

  • Dung Phan
  • Nicola Paoletti
  • Timothy Zhang
  • Radu Grosu
  • Scott A. SmolkaEmail author
  • Scott D. Stoller
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

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.

References

  1. 1.
    Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19835-9_21CrossRefzbMATHGoogle Scholar
  2. 2.
    Bak, S., Duggirala, P.S.: Rigorous simulation-based analysis of linear hybrid systems. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 555–572. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54577-5_32CrossRefGoogle Scholar
  3. 3.
    Bak, S., et al.: Hybrid automata: from verification to implementation. Int. J. Softw. Tools Technol. Transf. 1–18 (2017)Google Scholar
  4. 4.
    Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 23–37. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10512-3_3CrossRefzbMATHGoogle Scholar
  5. 5.
    Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 396–413. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89963-3_23CrossRefGoogle Scholar
  6. 6.
    Brázdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98–114. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11936-6_8CrossRefGoogle Scholar
  7. 7.
    Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: On reachability for hybrid automata over bounded time. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 416–427. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22012-8_33CrossRefzbMATHGoogle Scholar
  8. 8.
    Chen, X., Schupp, S., Makhlouf, I.B., Ábrahám, E., Frehse, G., Kowalewski, S.: A benchmark suite for hybrid systems reachability analysis. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 408–414. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-17524-9_29CrossRefGoogle Scholar
  9. 9.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000).  https://doi.org/10.1007/10722167_15CrossRefGoogle Scholar
  10. 10.
    Dreossi, T., Donzé, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 357–372. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-57288-8_26CrossRefGoogle Scholar
  11. 11.
    Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269–286. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-68167-2_19CrossRefGoogle Scholar
  12. 12.
    Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_30CrossRefGoogle Scholar
  13. 13.
    Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38574-2_14CrossRefGoogle Scholar
  14. 14.
    Garg, P.: Learning invariants using decision trees and implication counterexamples. ACM Sigplan Not. 51(1), 499–512 (2016)CrossRefGoogle Scholar
  15. 15.
    Gibiansky, A.: Quadcopter dynamics and simulation (2012). http://andrew.gibiansky.com/blog/physics/quadcopter-dynamics/
  16. 16.
    Henzinger, T.A., et al.: What’s decidable about hybrid automata? In: STOC, pp. 373–382. ACM Press (1995)Google Scholar
  17. 17.
    Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Netw. 2(5), 359–366 (1989)CrossRefGoogle Scholar
  18. 18.
    Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3–29. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63387-9_1CrossRefGoogle Scholar
  19. 19.
    Jin, X., et al.: Powertrain control verification benchmark. In: HSCC, pp. 253–262. ACM Press (2014)Google Scholar
  20. 20.
    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)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97–117. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63387-9_5CrossRefGoogle Scholar
  22. 22.
    Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-72522-0_6CrossRefGoogle Scholar
  23. 23.
    LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521(7553), 436 (2015)CrossRefGoogle Scholar
  24. 24.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16612-9_11CrossRefGoogle Scholar
  25. 25.
    Mitchell, M.: An Introduction to Genetic Algorithms. MIT press, Cambridge (1998)Google Scholar
  26. 26.
    Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S.A., Stoller, S.D.: Neural state classification for hybrid systems. arXiv:1807.09901 (2018)
  27. 27.
    Sen, K., Roşu, G., Agha, G.: Online efficient predictive safety analysis of multithreaded programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 123–138. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24730-2_9CrossRefzbMATHGoogle Scholar
  28. 28.
    Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574–592. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_31CrossRefGoogle Scholar
  29. 29.
    Vapnik, V.: The Nature of Statistical Learning Theory. Springer, New York (2013)Google Scholar
  30. 30.
    Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multi-layer neural networks. arXiv:1708.03322 (2017)

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Dung Phan
    • 1
  • Nicola Paoletti
    • 1
  • Timothy Zhang
    • 1
  • Radu Grosu
    • 2
  • Scott A. Smolka
    • 1
    Email author
  • Scott D. Stoller
    • 1
  1. 1.Department of Computer ScienceStony Brook UniversityStony BrookUSA
  2. 2.Department of Computer EngineeringTechnische Universitat WienViennaAustria

Personalised recommendations