Skip to main content
SpringerLink
Log in

Monitoring, Learning and Control of Cyber-Physical Systems with STL (Tutorial)

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

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

Included in the following conference series:

Abstract

Signal Temporal Logic (STL) is a popular specification language to reason about continuous-time trajectories of dynamical systems. STL was originally employed to specify and to monitor requirements over the temporal evolution of physical quantities and discrete states characterizing the behavior of cyber-physical systems (CPS). More recently, this formalism plays a key role in several approaches for the automatic design of safe systems and controllers satisfying an STL specification. However, requirements for CPS may include behavioral properties about the physical plant that are not always fully known a-priori and indeed cannot be completely manually specified. This has opened a new research direction on efficient methods for automatically mining and learning STL properties from measured data. In this tutorial we provide an overview of the state-of-the-art approaches available for monitoring, learning and control of CPS behaviors with STL focusing on some recent applications.

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 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.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

References

  1. Ackermann, C., Cleaveland, R., Huang, S., Ray, A., Shelton, C., Latronico, E.: Automatic requirement extraction from test cases. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 1–15. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_1

    Chapter  Google Scholar 

  2. Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of HSCC 2013: The 16th International Conference on Hybrid Systems: Computation and Control, pp. 173–182. ACM (2013)

    Google Scholar 

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

    Chapter  MATH  Google Scholar 

  4. Asarin, E., Donzé, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 147–160. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_12

    Chapter  Google Scholar 

  5. Aydin-Gol, E., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: Proceedings of CDC 2014: The 53rd IEEE Conference on Decision and Control, pp. 108–113. IEEE (2014)

    Google Scholar 

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

    Chapter  MATH  Google Scholar 

  7. Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587, 3–25 (2015)

    Article  MathSciNet  Google Scholar 

  8. Bartocci, E., Deshmukh, J., Donzé, A., Fainekos, G., Maler, O., Ničković, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification - Introductory and Advanced Topics. LNCS, vol. 10457, pp. 135–175. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_5

    Chapter  Google Scholar 

  9. Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification - Introductory and Advanced Topics. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_1

    Chapter  Google Scholar 

  10. Belta, C., Yordanov, B., Aydin Gol, E.: Formal Methods for Discrete-Time Dynamical Systems. SSDC, vol. 89. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-50763-7

    Book  MATH  Google Scholar 

  11. Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A decision tree approach to data classification using signal temporal logic. In: Proceedings of HSCC 2016: The 19th International Conference on Hybrid Systems: Computation and Control, pp. 1–10. ACM (2016)

    Google Scholar 

  12. Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 391–403. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45231-8_30

    Chapter  Google Scholar 

  13. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_18

    Chapter  Google Scholar 

  14. Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Garvit, J., Seshia, S.A.: Robust online monitoring of signal temporal logic. Form. Methods Syst. Des. 51, 5–30 (2017)

    Article  Google Scholar 

  15. Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231–246. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_19

    Chapter  Google Scholar 

  16. Dokhanchi, A., Zutshi, A., Sriniva, R.T., Sankaranarayanan, S., Fainekos, G.: Requirements driven falsification with coverage metrics. In: Proceedings of EMSOFT: The 12th International Conference on Embedded Software, pp. 31–40. IEEE (2015)

    Google Scholar 

  17. 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). https://doi.org/10.1007/978-3-642-14295-6_17

    Chapter  Google Scholar 

  18. Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264–279. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_19

    Chapter  Google Scholar 

  19. Donzé, A., Krogh, B., Rajhans, A.: Parameter synthesis for hybrid systems with an application to simulink models. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 165–179. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00602-9_12

    Chapter  MATH  Google Scholar 

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

    Chapter  MATH  Google Scholar 

  21. Donzé, A., Raman, V.: BluSTL: Controller synthesis from signal temporal logic specifications. In: Proceedings of 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems. EPiC Series in Computing, vol. 34, pp. 160–168. EasyChair (2015)

    Google Scholar 

  22. Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: A verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68–82. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_5

    Chapter  Google Scholar 

  23. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)

    Article  MathSciNet  Google Scholar 

  24. Fan, C., Meng, Y., Maier, J., Bartocci, E., Mitra, S., Schmid, U.: Verifying nonlinear analog and mixed-signal circuits with inputs. In: Proceedings of ADHS 2018 - IFAC Conference on Analysis and Design of Hybrid Systems, vol. 51(16), pp. 241–246 (2018)

    Article  Google Scholar 

  25. Fränzle, M., Herde, C.: Hysat: an efficient proof engine for bounded model checking of hybrid systems. Form. Methods Syst. Des. 30(3), 179–198 (2007)

    Article  Google Scholar 

  26. Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: 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_30

    Chapter  Google Scholar 

  27. Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: Spatel: A novel spatial-temporal logic and its applications to networked systems. In: Proceedings of HSCC 2015: The 18th International Conference on Hybrid Systems: Computation and Control, pp. 189–198. ACM (2015)

    Google Scholar 

  28. Haghighi, I., Sadraddini, S., Belta, C.: Robotic swarm control from spatio-temporal specifications. In: Proceedings of CDC 2016: The 55th IEEE Conference on Decision and Control, pp. 5708–5713. IEEE (2016)

    Google Scholar 

  29. Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of IEEE Symposium on Logic in Computer Science, pp. 278–292 (1996)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  31. Hoxha, B., Dokhanchi, A., Fainekos, G.E.: Mining parametric temporal logic properties in model-based design for cyber-physical systems. STTT 20(1), 79–93 (2018)

    Article  Google Scholar 

  32. Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ničković, D.: From signal temporal logic to FPGA monitors. In: Proceedings of MEMOCODE 2015: The 13th ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp. 218–227. IEEE (2015)

    Google Scholar 

  33. 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). https://doi.org/10.1007/978-3-319-46982-9_13

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  35. Karaman, S., Sanfelice, R.G., Frazzoli, E.: Optimal control of mixed logical dynamical systems with linear temporal logic specifications. In: Proceedings of CDC 2008: The 47th IEEE Conference on Decision and Control, pp. 2117–2122. IEEE (2008)

    Google Scholar 

  36. Kim, E.S., Sadraddini, S., Belta, C., Arcak, M., Seshia, S.A.: Dynamic contracts for distributed temporal logic control of traffic networks. In: IEEE 56th Annual Conference on Decision and Control (CDC) 2017, pp. 3640–3645. IEEE (2017)

    Google Scholar 

  37. Kong, H., Bartocci, E., Henzinger, T.A.: Reachable set over-approximation for nonlinear systems using piecewise barrier tubes. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 449–467. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_24

    Chapter  Google Scholar 

  38. Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \({\delta }\)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_15

    Chapter  Google Scholar 

  39. Kong, Z., Jones, A., Belta, C.: Temporal logics for learning and detection of anomalous behavior. IEEE Trans. Autom. Control. 62(3), 1210–1222 (2017)

    Article  MathSciNet  Google Scholar 

  40. Lee, E.A., Seshia, S.A.: An introductory textbook on cyber-physical systems. In: Proceedings of the 2010 Workshop on Embedded Systems Education, WESE 2010, pp. 1:1–1:6. ACM, New York (2010)

    Google Scholar 

  41. 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). https://doi.org/10.1007/978-3-540-30206-3_12

    Chapter  MATH  Google Scholar 

  42. Nenzi, L., Silvetti, S., Bartocci, E., Bortolussi, L.: A robust genetic algorithm for learning temporal specifications from data. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 323–338. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99154-2_20

    Chapter  Google Scholar 

  43. Nguyen, L., Kapinski, J., Jin, X., Deshmukh, J., Butts, K., Johnson, T.: Abnormal data classification using time-frequency temporal logic. In: Proceedings of HSCC 2017: The 20th ACM International Conference on Hybrid Systems: Computation and Control, pp. 237–242. ACM (2017)

    Google Scholar 

  44. Ničković, D., Lebeltel, O., Maler, O., Ferrère, T., Ulus, D.: AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 303–319. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_18

    Chapter  Google Scholar 

  45. Pant, Y.V., Abbas, H., Mangharam, R.: Smooth operator: control using the smooth robustness of temporal logic. In: Proceedings of CCTA 2017: The IEEE Conference on Control Technology and Applications, pp. 1235–1240. IEEE (2017)

    Google Scholar 

  46. Rajkumar, R.: A cyber-physical future. In: Proceedings of the IEEE 100 (Special Centennial Issue), pp. 1309–1312 (2012)

    Article  Google Scholar 

  47. Rajkumar, R.R., Lee, I., Sha, L., Stankovic, J.: Cyber-physical systems: the next computing revolution. In: Proceedings of DAC 2010: The 47th Design Automation Conference, pp. 731–736. ACM, New York (2010)

    Google Scholar 

  48. 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: Proceedings of CDC 2014: The 53rd IEEE Conference on Decision and Control, pp. 81–87. IEEE (2014)

    Google Scholar 

  49. Raman, V., Donzé, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 239–248. ACM (2015)

    Google Scholar 

  50. Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., Grosu, R.: XSpeed: accelerating reachability analysis on multi-core processors. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 3–18. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26287-1_1

    Chapter  Google Scholar 

  51. Sadraddini, S., Belta, C.: Model predictive control of urban traffic networks with temporal logic constraints. In: Proceedings of ACC 2016: The 2016 American Control Conference, p. 881. IEEE (2016)

    Google Scholar 

  52. Selyunin, K., Jaksic, S., Nguyen, T., Reidl, C., Hafner, U., Bartocci, E., Nickovic, D., Grosu, R.: Runtime monitoring with recovery of the SENT communication protocol. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 336–355. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_17

    Chapter  Google Scholar 

  53. Srinivas, N., Krause, A., Kakade, S.M., Seeger, M.W.: Information-theoretic regret bounds for gaussian process optimization in the bandit setting. IEEE Trans. Inf. Theory 58(5), 3250–3265 (2012)

    Article  MathSciNet  Google Scholar 

  54. Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning. IEEE Trans. Automat. Contr. 57(11), 2817–2830 (2012)

    Article  MathSciNet  Google Scholar 

  55. Xu, Z., Julius, A.A.: Census signal temporal logic inference for multiagent group behavior analysis. IEEE Trans. Autom. Sci. Eng. 15(1), 264–277 (2018)

    Article  Google Scholar 

  56. Yaghoubi, S., Fainekos, G.: Hybrid approximate gradient and stochastic descent for falsification of nonlinear systems. In: Proceedings of ACC 2017: The 2017 American Control Conference, pp. 529–534. IEEE (2017)

    Google Scholar 

  57. Zhou, J., Ramanathan, R., Wong, W.-F., Thiagarajan, P.S.: Automated property synthesis of ODEs based bio-pathways models. In: Feret, J., Koeppl, H. (eds.) CMSB 2017. LNCS, vol. 10545, pp. 265–282. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67471-1_16

    Chapter  Google Scholar 

Download references

Acknowledgements

The author acknowledges the partial support of the ICT COST Action IC1402 Runtime Verification beyond Monitoring (ARVI).

Author information

Authors and Affiliations

  1. Technische Universität Wien, Vienna, Austria

    Ezio Bartocci

Authors
  1. Ezio Bartocci
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ezio Bartocci .

Editor information

Editors and Affiliations

  1. University of Malta, Msida, Malta

    Christian Colombo

  2. University of Lübeck, Lübeck, Germany

    Martin Leucker

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bartocci, E. (2018). Monitoring, Learning and Control of Cyber-Physical Systems with STL (Tutorial). In: Colombo, C., Leucker, M. (eds) Runtime Verification. RV 2018. Lecture Notes in Computer Science(), vol 11237. Springer, Cham. https://doi.org/10.1007/978-3-030-03769-7_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03769-7_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03768-0

  • Online ISBN: 978-3-030-03769-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation