Abstract
From the formation of traffic jams to the development of troublesome, whirlpool-like spirals in the heart’s electrical activity, spatio-temporal patterns are key in understanding how complex behaviors can emerge in a network of locally interacting dynamical systems. One of the most important and intriguing questions is how to specify spatio-temporal behaviors in a formal and human-understandable specification language and how to monitor their onset efficiently. In this tutorial, we present the spatio-temporal logic STREL and its expressivity to specify and monitor spatio-temporal behaviors over complex dynamical and spatially distributed systems. We demonstrate our formalism’s applicability to different scenarios considering static or dynamic spatial configurations and systems with deterministic or stochastic dynamics.
This research has been partially supported by the Austrian FWF projects ZK-35 and W1255-N23, by the Italian PRIN project “SEDUCE” n. 2017TWRCNB and by the Italian PRIN project “IT-MaTTerS” n, 2017FTXR7S.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
We restrict here only to the tropical semiring, a more general definition can be found in [13].
References
Abbas, H., Fainekos, G.E., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 12(s2), 95:1–95:30 (2013). https://doi.org/10.1145/2465787.2465797
Abelson, H., et al.: Amorphous computing. Commun. ACM 43(5), 74–82 (2000). https://doi.org/10.1145/332833.332842
Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.): Handbook of Spatial Logics. Springer, Heidelberg (2007). https://doi.org/10.1007/978-1-4020-5587-4
Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: A survey on sensor networks. IEEE Commun. Mag. 40(8), 102–114 (2002). https://doi.org/10.1109/MCOM.2002.1024422
Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. J. ACM 43, 116–146 (1996)
Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002). https://doi.org/10.1145/506147.506151
Aurenhammer, F.: Voronoi diagrams—a survey of a fundamental geometric data structure. ACM Comput. Surv. 23(3), 345–405 (1991). https://doi.org/10.1145/116873.116880
Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. Electron. Notes Theoret. Comput. Sci. 290, 19–36 (2012). https://doi.org/10.1016/j.entcs.2012.11.009
Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theoret. Comp. Sci. 587, 3–25 (2015). https://doi.org/10.1016/j.tcs.2015.02.046
Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135–175. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_5
Bartocci, E., Fenton, F.H.: Teaching cardiac electrophysiology modeling to undergraduate students: laboratory exercises and GPU programming for the study of arrhythmias and spiral wave dynamics. Adv. Physiol. Educ. 35(4), 427–437 (2011). https://doi.org/10.1152/advan.00034.2011
Bartocci, E., Bloem, R., Nickovic, D., Roeck, F.: A counting semantics for monitoring LTL specifications over finite traces. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 547–564. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_29
Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Proceedings of MEMOCODE 2017: The 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 146–155. ACM (2017). https://doi.org/10.1145/3127041.3127050
Bartocci, E., Bortolussi, L., Milios, D., Nenzi, L., Sanguinetti, G.: Studying emergent behaviours in morphogenesis using signal spatio-temporal logic. In: Abate, A., Šafránek, D. (eds.) HSB 2015. LNCS, vol. 9271, pp. 156–172. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26916-0_9
Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_1
Bartocci, E., Ferrère, T., Manjunath, N., Nickovic, D.: Localizing faults in simulink/stateflow models with STL. In: Proceedings of HSCC 2018: The 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), pp. 197–206. ACM (2018). https://doi.org/10.1145/3178126
Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Ničković, D.: Automatic failure explanation in CPS models. In: Ölveczky, P.C., Salaün, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 69–86. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30446-1_4
Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Nickovic, D., Pastore, F.: CPSDebug: a tool for explanation of failures in cyber-physical systems. In: Proceedings of ISSTA 2020: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, USA, 18–22 July 2020, pp. 569–572. ACM (2020). https://doi.org/10.1145/3395363
Belongie, S., Malik, J., Puzicha, J.: Shape matching and object recognition using shape contexts. IEEE Trans. Pattern Anal. Mach. Intell. 24(4), 509–522 (2002). https://doi.org/10.1109/34.993558
Bennett, B., Cohn, A.G., Wolter, F., Zakharyaschev, M.: Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Appl. Intell. 17(3), 239–251 (2002). https://doi.org/10.1023/A:1020083231504
Bhattacharyya, A.: Morphogenesis as an amorphous computation. In: Proceedings of the Third Conference on Computing Frontiers, 2006, Ischia, Italy, 3–5 May 2006, pp. 53–64. ACM (2006). https://doi.org/10.1145/1128022.1128032
Bortolussi, L., Galpin, V., Hillston, J.: Hybrid performance modelling of opportunistic networks. In: Proceedings of QAPL 2012: The 10th Workshop on Quantitative Aspects of Programming Languages and Systems, pp. 106–121 (2012). https://doi.org/10.4204/EPTCS.85.8
Bortolussi, L., Milios, D., Sanguinetti, G.: U-check: model checking and parameter synthesis under uncertainty. In: Campos, J., Haverkort, B.R. (eds.) QEST 2015. LNCS, vol. 9259, pp. 89–104. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22264-6_6
Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time markov chains. Inf. Comput. 247, 235–253 (2016)
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_23
Bresolin, D., Sala, P., Monica, D.D., Montanari, A., Sciavicco, G.: A decidable spatial generalization of metric interval temporal logic. In: 2010 17th International Symposium on Temporal Representation and Reasoning, pp. 95–102 (2010). https://doi.org/10.1109/TIME.2010.22
Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. Comput. 186(2), 194–235 (2003). https://doi.org/10.1016/S0890-5401(03)00137-8
Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: Proceedings of POPL 2000: the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 365–377. ACM, New York (2000). https://doi.org/10.1145/325694.325742
Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 222–235. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44602-7_18
Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model-checking of vehicular movement in public transport systems (2015, Submitted)
Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 156–201. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34096-8_6
Dalal, N., Triggs, B.: Histograms of oriented gradients for human detection. In: Proceedings of CVPR 2005: The IEEE Computer Society Conference on Computer Vision and Pattern Recognition, vol. 1, pp. 886–893, June 2005
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_27
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
Donzé, A., Clermont, G., Legay, A., Langmead, C.J.: Parameter synthesis in nonlinear dynamical systems: application to systems biology. In: Batzoglou, S. (ed.) RECOMB 2009. LNCS, vol. 5541, pp. 155–169. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02008-7_11
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
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
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time. In: Wright, J.R., Landweber, L., Demers, A.J., Teitelbaum, T. (eds.) Proceedings of POPL 83: The Tenth Annual ACM Symposium on Principles of Programming Languages, pp. 127–140. ACM Press (1983). https://doi.org/10.1145/567067.567081
Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262–4291 (2009). https://doi.org/10.1016/j.tcs.2009.06.021
Feng, C., Hillston, J., Reijsbergen, D.: Moment-based probabilistic prediction of bike availability for bike-sharing systems. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 139–155. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43425-4_9
Finkel, R.A., Bentley, J.L.: Quad trees: a data structure for retrieval on composite keys. Acta Informatica 4, 1–9 (1974). https://doi.org/10.1007/BF00288933
Fishman, E.: Bikeshare: a review of recent literature. Transp. Rev. 36(1), 92–113 (2016). https://doi.org/10.1080/01441647.2015.1033036
Galton, A.: The mereotopology of discrete space. In: Freksa, C., Mark, D.M. (eds.) COSIT 1999. LNCS, vol. 1661, pp. 251–266. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48384-5_17
Gol, E.A., 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). https://doi.org/10.1109/CDC.2014.7039367
Golden, J.W., Yoon, H.S.: Heterocyst formation in anabaena. Curr. Opin. Microbiol. 1(6), 623–629 (1998). https://doi.org/10.1016/S1369-5274(98)80106-9
Grosu, R., et al.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_31
Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009). https://doi.org/10.1145/1467247.1467271
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. IEEE (2015). https://doi.org/10.1145/2728606.2728633
Jaksic, S., Bartocci, E., Grosu, R., Nguyen, T., Nickovic, D.: Quantitative monitoring of STL with edit distance. Formal Methods Syst. Des. 53(1), 83–112 (2018). https://doi.org/10.1007/s10703-018-0319-x
Jaksic, S., Bartocci, E., Grosu, R., Nickovic, D.: An algebraic framework for runtime verification. IEEE Trans. CAD Integr. Circuits Syst. 37(11), 2233–2243 (2018). https://doi.org/10.1109/TCAD.2018.2858460
Julesz, B.: Textons, the elements of texture perception, and their interactions. Nature 290, 91–97 (1981)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990). https://doi.org/10.1007/BF01995674
Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems, A Cyber-Physical Systems Approach, 2nd edn. MIT Press, Berlin (2017)
Loreti, M., Hillston, J.: Modelling and analysis of collective adaptive systems with CARMA and its tools. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 83–119. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34096-8_4
Lowe, D.G.: Object recognition from local scale-invariant features. In: Proceedings of the International Conference on Computer Vision, vol. 2, pp. 1150–1157 (1999)
Ma, M., Bartocci, E., Lifland, E., Stankovic, J.A., Feng, L.: SaSTL: spatial aggregation signal temporal logic for runtime monitoring in smart cities. In: Proceedings of ICCPS 2020: The 11th ACM/IEEE International Conference on Cyber-Physical Systems, pp. 51–62. IEEE (2020). https://doi.org/10.1109/ICCPS48487.2020.00013
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
Maler, O., Ničković, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247–268 (2013)
Marx, M., Reynolds, M.: Undecidability of compass logic. J. Logic Comput. 9(6), 897–914 (1999). https://doi.org/10.1093/logcom/9.6.897
Murthy, A., et al.: Curvature analysis of cardiac excitation wavefronts. IEEE/ACM Trans. Comput. Biol. Bioinform. 10(2), 323–336 (2013). https://doi.org/10.1109/TCBB.2012.125
Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 21–37. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_2
Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Log. Methods Comput. Sci. 14(4) (2018). https://doi.org/10.23638/LMCS-14(4:2)2018
Olver, P.J.: Finite differences. Introduction to Partial Differential Equations. UTM, pp. 181–214. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-02099-0_5
Ratasich, D., Khalid, F., Geissler, F., Grosu, R., Shafique, M., Bartocci, E.: A roadmap toward the resilient Internet of Things for cyber-physical systems. IEEE Access 7, 13260–13283 (2019). https://doi.org/10.1109/ACCESS.2019.2891969
Rodionova, A., Bartocci, E., Ničković, D., Grosu, R.: Temporal logic as filtering. In: Proceedings of HSCC 2016, pp. 11–20. ACM (2016). https://doi.org/10.1145/2883817.2883839
Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice Hall, Upper Saddle River (2002)
Sankaranarayanan, S., Kumar, S.A., Cameron, F., Bequette, B.W., Fainekos, G., Maahs, D.M.: Model-based falsification of an artificial pancreas control system. SIGBED Rev. 14(2), 24–33 (2017). https://doi.org/10.1145/3076125.3076128
Silvetti, S., Policriti, A., Bortolussi, L.: An active learning approach to the falsification of black box cyber-physical systems. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 3–17. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_1
Talcott, C.: Cyber-physical systems and events. In: Wirsing, M., Banâtre, J.-P., Hölzl, M., Rauschmayer, A. (eds.) Software-Intensive Systems and New Computing Paradigms. LNCS, vol. 5380, pp. 101–115. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89437-7_6
Tan, Y., Vuran, M.C., Goddard, S.: Spatio-temporal event model for cyber-physical systems. In: 2009 29th IEEE International Conference on Distributed Computing Systems Workshops, pp. 44–50. IEEE (2009). https://doi.org/10.1109/ICDCSW.2009.82
Turing, A.M.: The chemical basis of morphogenesis. Philos. Trans. R. So. London B: Biol. Sci. 237, 37–72 (1952)
Weiss, R.: Synthetic biology: from modules to systems. In: Proceedings of the 20th ACM Great Lakes Symposium on VLSI 2009, Providence, Rhode Island, USA, 16–18 May 2010, pp. 171–172. ACM (2010). https://doi.org/10.1145/1785481
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). https://doi.org/10.23919/ACC.2017.7963007
Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: an empirical study. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 46–60. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_4
Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368–1409 (2006). https://doi.org/10.1016/j.ic.2006.05.002
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Nenzi, L., Bartocci, E., Bortolussi, L., Loreti, M., Visconti, E. (2020). Monitoring Spatio-Temporal Properties (Invited Tutorial). In: Deshmukh, J., Ničković, D. (eds) Runtime Verification. RV 2020. Lecture Notes in Computer Science(), vol 12399. Springer, Cham. https://doi.org/10.1007/978-3-030-60508-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-60508-7_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-60507-0
Online ISBN: 978-3-030-60508-7
eBook Packages: Computer ScienceComputer Science (R0)