Skip to main content
SpringerLink
Log in

TeLEx: Passive STL Learning Using Only Positive Examples

  • Conference paper
  • First Online:
Runtime Verification (RV 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10548))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

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

  2. 2.

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

  3. 3.

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

References

  1. 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)

    Google Scholar 

  2. 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)

    Google Scholar 

  3. 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

    Chapter  Google Scholar 

  4. 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)

    Google Scholar 

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

    Google Scholar 

  6. 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

    Chapter  Google Scholar 

  7. 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

    Google Scholar 

  8. 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

    Chapter  Google Scholar 

  9. 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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Article  MathSciNet  MATH  Google Scholar 

  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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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  Google Scholar 

  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

    Google Scholar 

  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)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgement

This work is supported in part by DARPA under contract FA8750-16-C-0043 and NSF grant CNS-1423298.

Author information

Authors and Affiliations

  1. CSL, SRI International, Menlo Park, USA

    Susmit Jha, Ashish Tiwari & Natarajan Shankar

  2. EECS, UC Berkeley, Berkeley, USA

    Sanjit A. Seshia

  3. United Technologies Research Center, East Hartford, USA

    Tuhin Sahai

Authors
  1. Susmit Jha
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ashish Tiwari
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sanjit A. Seshia
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tuhin Sahai
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Natarajan Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Susmit Jha .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Shuvendu Lahiri

  2. The University of Manchester, Manchester, United Kingdom

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Jha, S., Tiwari, A., Seshia, S.A., Sahai, T., Shankar, N. (2017). TeLEx: Passive STL Learning Using Only Positive Examples. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation