Top

Published in:

2017 | Supplement | Chapter

TeLEx: Passive STL Learning Using Only Positive Examples

Authors : Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai, Natarajan Shankar

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

We propose a novel passive learning approach, TeLEx, to infer signal temporal logic formulas that characterize the behavior of a dynamical system using only observed signal traces of the system. The approach requires two inputs: a set of observed traces and a template Signal Temporal Logic (STL) formula. The unknown parameters in the template can include time-bounds of the temporal operators, as well as the thresholds in the inequality predicates. TeLEx finds the value of the unknown parameters such that the synthesized STL property is satisfied by all the provided traces and it is tight. This requirement of tightness is essential to generating interesting properties when only positive examples are provided and there is no option to actively query the dynamical system to discover the boundaries of legal behavior. We propose a novel quantitative semantics for satisfaction of STL properties which enables TeLEx to learn tight STL properties without multidimensional optimization. The proposed new metric is also smooth. This is critical to enable use of gradient-based numerical optimization engines and it produces a 30\(\times \)–100\(\times \) speed-up with respect to the state-of-art gradient-free optimization. The approach is implemented in a publicly available tool.

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 Monitoring Hyperproperties

next chapter From Model Checking to Runtime Verification and Back

https://github.com/susmitjha/TeLEX.

https://github.com/susmitjha/TeLEX/blob/master/tests/twoagent.py.

https://github.com/udacity/self-driving-car/tree/master/challenges/challenge-2.

Abbas, H., Hoxha, B., Fainekos, G., Ueda, K.: Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems. In: 2014 IEEE 4th Annual International Conference on Cyber Technology in Automation, Control, and Intelligent Systems (CYBER), pp. 1–6. IEEE (2014)

Abbas, H., Winn, A., Fainekos, G., Julius, A.A.: Functional gradient descent method for metric temporal logic specifications. In: 2014 American Control Conference (ACC), pp. 2312–2317. IEEE (2014)

Akazaki, T.: Falsification of conditional safety properties for cyber-physical systems with Gaussian process regression. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 439–446. Springer, Cham (2016). doi:10.1007/978-3-319-46982-9_27 CrossRef

Aksaray, D., Jones, A., Kong, Z., Schwager, M., Belta, C.: Q-learning for robust satisfaction of signal temporal logic specifications. In: 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 6565–6570. IEEE (2016)

Angluin, D.: Identifying languages from stochastic examples. Technical report, YALEU/DCS/RR-614, Yale University, Department of Computer Science (1988)

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). doi:10.1007/978-3-642-19835-9_21 CrossRef

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). doi:10.1007/978-3-319-10512-3_3

Deshmukh, J.V., Majumdar, R., Prabhu, V.S.: Quantifying conformance using the Skorokhod metric. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 234–250. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_14 CrossRef

Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_17 CrossRef

10.

Donzé, A.: On signal temporal logic. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 382–383. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40787-1_27 CrossRef

11.

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). doi:10.1007/978-3-642-15297-9_9 CrossRef

12.

Facchinei, F., Lucidi, S., Palagi, L.: A truncated newton algorithm for large scale box constrained optimization. SIAM J. Optim. 12(4), 1100–1125 (2002)MathSciNetCrossRefMATH

13.

Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES/RV -2006. LNCS, vol. 4262, pp. 178–192. Springer, Heidelberg (2006). doi:10.1007/11940197_12 CrossRef

14.

Fu, J., Topcu, U.: Synthesis of joint control and active sensing strategies under temporal logic constraints. IEEE Trans. Autom. Control 61(11), 3464–3476 (2016). doi:10.1109/TAC.2016.2518639 MathSciNetCrossRefMATH

15.

Giuseppe, B., Cristian Ioan, V., Francisco, P.A., Hirotoshi, Y., Calin, B.: A decision tree approach to data classification using signal temporal logic. In: Hybrid Systems: Computation and Control (HSCC), Vienna, Austria, pp. 1–10, April 2016

16.

Gold, E.M.: Language identification in the limit. Inf. Control 10(5), 447–474 (1967)MathSciNetCrossRefMATH

17.

Horning, J.J.: A study of grammatical inference. Technical report, DTIC Document (1969)

18.

Hoxha, B., Dokhanchi, A., Fainekos, G.: Mining parametric temporal logic properties in model based design for cyber-physical systems. arXiv preprint arXiv:1512.07956 (2015)

19.

Jakšić, S., Bartocci, E., Grosu, R., Ničković, D.: Quantitative monitoring of STL with edit distance. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 201–218. Springer, Cham (2016). doi:10.1007/978-3-319-46982-9_13 CrossRef

20.

Jha, S., Raman, V.: Automated synthesis of safe autonomous vehicle control under perception uncertainty. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 117–132. Springer, Cham (2016). doi:10.1007/978-3-319-40648-0_10 CrossRef

21.

Jha, S., Raman, V.: On optimal control of stochastic linear hybrid systems. In: Fränzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 69–84. Springer, Cham (2016). doi:10.1007/978-3-319-44878-7_5 CrossRef

22.

Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Inform. (2017). doi:10.1007/s00236-017-0294-5

23.

Jin, X., Donzé, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 34(11), 1704–1717 (2015)CrossRefMATH

24.

Kong, Z., Jones, A., Medina Ayala, A., Aydin Gol, E., Belta, C.: Temporal logic inference for classification and prediction from data. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 273–282. ACM (2014)

25.

Lindemann, L., Dimarogonas, D.V.: Robust control for signal temporal logic specifications using average space robustness. arXiv preprint arXiv:1607.07019 (2016)

26.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_12 CrossRef

27.

Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 475–505. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78127-1_26 CrossRef

28.

Muggleton, S.: Learning from positive data. In: Muggleton, S. (ed.) ILP 1996. LNCS, vol. 1314, pp. 358–376. Springer, Heidelberg (1997). doi:10.1007/3-540-63494-0_65 CrossRef

29.

Price, K., Storn, R.M., Lampinen, J.A.: Differential Evolution: A Practical Approach to Global Optimization. Springer Science & Business Media, New York (2006)MATH

30.

Raman, V., Donzé, A., Maasoumy, M., Murray, R.M., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Model predictive control with signal temporal logic specifications. In: CDC, pp. 81–87, December 2014

31.

Sadraddini, S., Belta, C.: Robust temporal logic model predictive control. In: 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton), pp. 772–779. IEEE (2015)

32.

Valiant, L.G.: A theory of the learnable. Commun. ACM 27(11), 1134–1142 (1984)CrossRefMATH

33.

Yang, H., Hoxha, B., Fainekos, G.: Querying parametric temporal logic properties on embedded systems. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol. 7641, pp. 136–151. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34691-0_11 CrossRef

34.

Zhu, C., Byrd, R.H., Lu, P., Nocedal, J.: Algorithm 778: fortran subroutines for large-scale bound-constrained optimization. ACM Trans. Math. Softw. (TOMS) 23(4), 550–560 (1997)MathSciNetCrossRefMATH

Title: TeLEx: Passive STL Learning Using Only Positive Examples
Authors: Susmit Jha
Ashish Tiwari
Sanjit A. Seshia
Tuhin Sahai
Natarajan Shankar
Publisher: Springer International Publishing
Book: Runtime Verification
Print ISBN: 978-3-319-67530-5

Electronic ISBN: 978-3-319-67531-2

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-67531-2_13

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