Top

Published in:

2019 | OriginalPaper | Chapter

Neural Predictive Monitoring

Authors : Luca Bortolussi, Francesca Cairoli, Nicola Paoletti, Scott A. Smolka, Scott D. Stoller

Published in: Runtime Verification

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Neural State Classification (NSC) is a recently proposed method for runtime predictive monitoring of Hybrid Automata (HA) using deep neural networks (DNNs). NSC trains a DNN as an approximate reachability predictor that labels a given HA state x as positive if an unsafe state is reachable from x within a given time bound, and labels x as negative otherwise. NSC predictors have very high accuracy, yet are prone to prediction errors that can negatively impact reliability. To overcome this limitation, we present Neural Predictive Monitoring (NPM), a technique based on NSC and conformal prediction that complements NSC predictions with statistically sound estimates of uncertainty. This yields principled criteria for the rejection of predictions likely to be incorrect, without knowing the true reachability values. We also present an active learning method that significantly reduces both the NSC predictor’s error rate and the percentage of rejected predictions. Our approach is highly efficient, with computation times on the order of milliseconds, and effective, managing in our experimental evaluation to successfully reject almost all incorrect predictions.

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!

inform now

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!

inform now

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!

inform now

previous chapter Accelerated Learning of Predictive Runtime Monitors for Rare Failure

next chapter Comparing Controlled System Synthesis and Suppression Enforcement

The only assumption is exchangeability, a weaker version of the independent and identically distributed assumption.

In [21], the PM problem is called “state classification problem”, and its solution a “state classifier”.

We will interchangeably use the term “predictor” for the function returning a vector of class likelihoods, and for the function returning the class with highest likelihood.

The choice of \(\varDelta \) is not very important, as long as it is symmetric.

As opposed to learning a linear combination of confidence and credibility, which is less interpretable.

Note indeed that the \(\alpha \)-score of a sample \((x_i,y_i)\) is zero only if h both correctly predicts \(y_i\) and the corresponding class likelihood \(P_h(y_i\mid x_i)\) is 1.

Evaluating our rejection criterion reduces to computing two p-values (confidence and credibility). Each p-value is derived by computing a nonconformity score, which requires one execution of the underlying predictor h, and one search over the array of calibration scores.

dReal - Networked Water Tank Controllers (2017). http://dreal.github.io/benchmarks/networks/water/

Alur, R.: Formal verification of hybrid systems. In: Proceedings of the Ninth ACM International Conference on Embedded Software (EMSOFT), pp. 273–278, October 2011

Babaee, R., Gurfinkel, A., Fischmeister, S.: Predictive run-time verification of discrete-time reachability properties in black-box systems using trace-level abstraction and statistical learning. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 187–204. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_11CrossRef

Bak, S., Johnson, T.T., Caccamo, M., Sha, L.: Real-time reachability for verified simplex design. In: Real-Time Systems Symposium (RTSS), 2014 IEEE, pp. 138–148. IEEE (2014)

Balasubramanian, V., Ho, S.S., Vovk, V.: Conformal prediction for reliable machine learning: theory, adaptations and applications. Newnes (2014)

Batuwita, R., Palade, V.: Class imbalance learning methods for support vector machines (2013)CrossRef

Bishop, C.M.: Pattern Recognition and Machine Learning. Information Science and Statistics. Springer, New York (2006)MATH

Bortolussi, L., Cairoli, F., Paoletti, N., Stoller, S.D.: Conformal predictions for hybrid system state classification. In: From Reactive Systems to Cyber-Physical Systems, to appear (2019)

Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time Markov chains. Inf. Comput. 247, 235–253 (2016)MathSciNetCrossRef

10.

Chen, X., Sankaranarayanan, S.: Model predictive real-time monitoring of linear systems. In: Real-Time Systems Symposium (RTSS), 2017 IEEE, pp. 297–306. IEEE (2017)

11.

Djeridane, B., Lygeros, J.: Neural approximation of PDE solutions: an application to reachability computations. In: Proceedings of the 45th IEEE Conference on Decision and Control, pp. 3034–3039. IEEE (2006)

12.

Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9_9CrossRefMATH

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_14CrossRef

14.

Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNetCrossRef

15.

Lehmann, E.L., Romano, J.P.: Testing Statistical Hypotheses. Springer Texts in Statistics. Springer, New York (2006)MATH

16.

Makili, L.E., Sánchez, J.A.V., Dormido-Canto, S.: Active learning using conformal predictors: application to image classification. Fusion Sci. Technol. 62(2), 347–355 (2012)CrossRef

17.

Melluish, T., Saunders, C., Nouretdinov, I., Vovk, V.: The typicalness framework: a comparison with the bayesian approach. University of London, Royal Holloway (2001)

18.

Paoletti, N., Liu, K.S., Smolka, S.A., Lin, S.: Data-driven robust control for type 1 diabetes under meal and exercise uncertainties. In: Feret, J., Koeppl, H. (eds.) CMSB 2017. LNCS, vol. 10545, pp. 214–232. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67471-1_13CrossRef

19.

Papadopoulos, H.: Inductive conformal prediction: Theory and application to neural networks. In: Tools in artificial intelligence. InTech (2008)

20.

Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S.A., Stoller, S.D.: Neural state classification for hybrid systems. ArXiv e-prints, July 2018

21.

Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S.A., Stoller, S.D.: Neural state classification for hybrid systems. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 422–440. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_25CrossRef

22.

Qin, X., Deshmukh, J.V.: Predictive monitoring for signal temporal logic with probabilistic guarantees. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 266–267. ACM (2019)

23.

Rasmussen, C.E., Williams, C.K.: Gaussian Processes for Machine Learning, vol. 1. MIT press, Cambridge (2006)MATH

24.

Royo, V.R., Fridovich-Keil, D., Herbert, S., Tomlin, C.J.: Classification-based approximate reachability with guarantees applied to safe trajectory tracking. arXiv preprint arXiv:1803.03237 (2018)

25.

Sauter, G., Dierks, H., Fränzle, M., Hansen, M.R.: Lightweight hybrid model checking facilitating online prediction of temporal properties. In: Proceedings of the 21st Nordic Workshop on Programming Theory, pp. 20–22 (2009)

26.

Sha, L.: Using simplicity to control complexity. IEEE Softw. 4, 20–28 (2001)

27.

Vovk, V., Gammerman, A., Shafer, G.: Algorithmic learning in a random world. Springer, Heidelberg (2005)MATH

Title: Neural Predictive Monitoring
Authors: Luca Bortolussi
Francesca Cairoli
Nicola Paoletti
Scott A. Smolka
Scott D. Stoller
Publisher: Springer International Publishing
Book: Runtime Verification
Print ISBN: 978-3-030-32078-2

Electronic ISBN: 978-3-030-32079-9

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-32079-9_8

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner