{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:52:59Z","timestamp":1743087179264,"version":"3.40.3"},"publisher-location":"Cham","reference-count":75,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030605070"},{"type":"electronic","value":"9783030605087"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-60508-7_2","type":"book-chapter","created":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T04:33:06Z","timestamp":1602045186000},"page":"21-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Monitoring Spatio-Temporal Properties (Invited Tutorial)"],"prefix":"10.1007","author":[{"given":"Laura","family":"Nenzi","sequence":"first","affiliation":[]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Bortolussi","sequence":"additional","affiliation":[]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[]},{"given":"Ennio","family":"Visconti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,10,2]]},"reference":[{"issue":"s2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"95:1","DOI":"10.1145\/2465787.2465797","volume":"12","author":"H Abbas","year":"2013","unstructured":"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\u201395:30 (2013). https:\/\/doi.org\/10.1145\/2465787.2465797","journal-title":"ACM Trans. Embed. Comput. Syst."},{"issue":"5","key":"2_CR2","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/332833.332842","volume":"43","author":"H Abelson","year":"2000","unstructured":"Abelson, H., et al.: Amorphous computing. Commun. ACM 43(5), 74\u201382 (2000). https:\/\/doi.org\/10.1145\/332833.332842","journal-title":"Commun. ACM"},{"key":"2_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5587-4","volume-title":"Handbook of Spatial Logics","year":"2007","unstructured":"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"},{"issue":"8","key":"2_CR4","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1109\/MCOM.2002.1024422","volume":"40","author":"IF Akyildiz","year":"2002","unstructured":"Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: A survey on sensor networks. IEEE Commun. Mag. 40(8), 102\u2013114 (2002). https:\/\/doi.org\/10.1109\/MCOM.2002.1024422","journal-title":"IEEE Commun. Mag."},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. J. ACM 43, 116\u2013146 (1996)","journal-title":"J. ACM"},{"issue":"2","key":"2_CR6","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/506147.506151","volume":"49","author":"E Asarin","year":"2002","unstructured":"Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172\u2013206 (2002). https:\/\/doi.org\/10.1145\/506147.506151","journal-title":"J. ACM"},{"issue":"3","key":"2_CR7","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/116873.116880","volume":"23","author":"F Aurenhammer","year":"1991","unstructured":"Aurenhammer, F.: Voronoi diagrams\u2014a survey of a fundamental geometric data structure. ACM Comput. Surv. 23(3), 345\u2013405 (1991). https:\/\/doi.org\/10.1145\/116873.116880","journal-title":"ACM Comput. Surv."},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2012.11.009","volume":"290","author":"K Bae","year":"2012","unstructured":"Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. Electron. Notes Theoret. Comput. Sci. 290, 19\u201336 (2012). https:\/\/doi.org\/10.1016\/j.entcs.2012.11.009","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2015.02.046","volume":"587","author":"E Bartocci","year":"2015","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theoret. Comp. Sci. 587, 3\u201325 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.02.046","journal-title":"Theoret. Comp. Sci."},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"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\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5"},{"issue":"4","key":"2_CR11","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1152\/advan.00034.2011","volume":"35","author":"E Bartocci","year":"2011","unstructured":"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\u2013437 (2011). https:\/\/doi.org\/10.1152\/advan.00034.2011","journal-title":"Adv. Physiol. Educ."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-319-96145-3_29","volume-title":"Computer Aided Verification","author":"E Bartocci","year":"2018","unstructured":"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\u2013564. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_29"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"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\u2013155. ACM (2017). https:\/\/doi.org\/10.1145\/3127041.3127050","DOI":"10.1145\/3127041.3127050"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-26916-0_9","volume-title":"Hybrid Systems Biology","author":"E Bartocci","year":"2015","unstructured":"Bartocci, E., Bortolussi, L., Milios, D., Nenzi, L., Sanguinetti, G.: Studying emergent behaviours in\u00a0morphogenesis using signal spatio-temporal\u00a0logic. In: Abate, A., \u0160afr\u00e1nek, D. (eds.) HSB 2015. LNCS, vol. 9271, pp. 156\u2013172. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26916-0_9"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"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\u201333. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Ferr\u00e8re, 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\u2013206. ACM (2018). https:\/\/doi.org\/10.1145\/3178126","DOI":"10.1145\/3178126"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-30446-1_4","volume-title":"Software Engineering and Formal Methods","author":"E Bartocci","year":"2019","unstructured":"Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Ni\u010dkovi\u0107, D.: Automatic failure explanation in CPS models. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 69\u201386. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_4"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"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\u201322 July 2020, pp. 569\u2013572. ACM (2020). https:\/\/doi.org\/10.1145\/3395363","DOI":"10.1145\/3395363"},{"issue":"4","key":"2_CR19","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/34.993558","volume":"24","author":"S Belongie","year":"2002","unstructured":"Belongie, S., Malik, J., Puzicha, J.: Shape matching and object recognition using shape contexts. IEEE Trans. Pattern Anal. Mach. Intell. 24(4), 509\u2013522 (2002). https:\/\/doi.org\/10.1109\/34.993558","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"issue":"3","key":"2_CR20","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1020083231504","volume":"17","author":"B Bennett","year":"2002","unstructured":"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\u2013251 (2002). https:\/\/doi.org\/10.1023\/A:1020083231504","journal-title":"Appl. Intell."},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Bhattacharyya, A.: Morphogenesis as an amorphous computation. In: Proceedings of the Third Conference on Computing Frontiers, 2006, Ischia, Italy, 3\u20135 May 2006, pp. 53\u201364. ACM (2006). https:\/\/doi.org\/10.1145\/1128022.1128032","DOI":"10.1145\/1128022.1128032"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"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\u2013121 (2012). https:\/\/doi.org\/10.4204\/EPTCS.85.8","DOI":"10.4204\/EPTCS.85.8"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-319-22264-6_6","volume-title":"Quantitative Evaluation of Systems","author":"L Bortolussi","year":"2015","unstructured":"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\u2013104. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22264-6_6"},{"key":"2_CR24","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.ic.2016.01.004","volume":"247","author":"L Bortolussi","year":"2016","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time markov chains. Inf. Comput. 247, 235\u2013253 (2016)","journal-title":"Inf. Comput."},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-89963-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Bortolussi","year":"2018","unstructured":"Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of\u00a0stochastic models. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 396\u2013413. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_23"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"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\u2013102 (2010). https:\/\/doi.org\/10.1109\/TIME.2010.22","DOI":"10.1109\/TIME.2010.22"},{"issue":"2","key":"2_CR27","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/S0890-5401(03)00137-8","volume":"186","author":"L Caires","year":"2003","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. Comput. 186(2), 194\u2013235 (2003). https:\/\/doi.org\/10.1016\/S0890-5401(03)00137-8","journal-title":"Inf. Comput."},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"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\u2013377. ACM, New York (2000). https:\/\/doi.org\/10.1145\/325694.325742","DOI":"10.1145\/325694.325742"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-662-44602-7_18","volume-title":"Theoretical Computer Science","author":"V Ciancia","year":"2014","unstructured":"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\u2013235. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44602-7_18"},{"key":"2_CR30","unstructured":"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)"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-34096-8_6","volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems","author":"V Ciancia","year":"2016","unstructured":"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\u2013201. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-34096-8_6"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"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\u2013893, June 2005","DOI":"10.1109\/CVPR.2005.177"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Computer Aided Verification","author":"A David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, 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\u2013355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_27"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, 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\u2013106. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-02008-7_11","volume-title":"Research in Computational Molecular Biology","author":"A Donz\u00e9","year":"2009","unstructured":"Donz\u00e9, 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\u2013169. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02008-7_11"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-39799-8_19","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264\u2013279. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-00602-9_12","volume-title":"Hybrid Systems: Computation and Control","author":"A Donz\u00e9","year":"2009","unstructured":"Donz\u00e9, 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\u2013179. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00602-9_12"},{"key":"2_CR38","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d 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\u2013140. ACM Press (1983). https:\/\/doi.org\/10.1145\/567067.567081","DOI":"10.1145\/567067.567081"},{"issue":"42","key":"2_CR39","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-319-43425-4_9","volume-title":"Quantitative Evaluation of Systems","author":"C Feng","year":"2016","unstructured":"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\u2013155. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43425-4_9"},{"key":"2_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00288933","volume":"4","author":"RA Finkel","year":"1974","unstructured":"Finkel, R.A., Bentley, J.L.: Quad trees: a data structure for retrieval on composite keys. Acta Informatica 4, 1\u20139 (1974). https:\/\/doi.org\/10.1007\/BF00288933","journal-title":"Acta Informatica"},{"issue":"1","key":"2_CR42","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1080\/01441647.2015.1033036","volume":"36","author":"E Fishman","year":"2016","unstructured":"Fishman, E.: Bikeshare: a review of recent literature. Transp. Rev. 36(1), 92\u2013113 (2016). https:\/\/doi.org\/10.1080\/01441647.2015.1033036","journal-title":"Transp. Rev."},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/3-540-48384-5_17","volume-title":"Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science","author":"A Galton","year":"1999","unstructured":"Galton, A.: The mereotopology of discrete space. In: Freksa, C., Mark, D.M. (eds.) COSIT 1999. LNCS, vol. 1661, pp. 251\u2013266. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48384-5_17"},{"key":"2_CR44","doi-asserted-by":"publisher","unstructured":"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\u2013113. IEEE (2014). https:\/\/doi.org\/10.1109\/CDC.2014.7039367","DOI":"10.1109\/CDC.2014.7039367"},{"issue":"6","key":"2_CR45","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1016\/S1369-5274(98)80106-9","volume":"1","author":"JW Golden","year":"1998","unstructured":"Golden, J.W., Yoon, H.S.: Heterocyst formation in anabaena. Curr. Opin. Microbiol. 1(6), 623\u2013629 (1998). https:\/\/doi.org\/10.1016\/S1369-5274(98)80106-9","journal-title":"Curr. Opin. Microbiol."},{"key":"2_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","volume-title":"Computer Aided Verification","author":"R Grosu","year":"2011","unstructured":"Grosu, R., et al.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396\u2013411. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_31"},{"issue":"3","key":"2_CR47","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1467247.1467271","volume":"52","author":"R Grosu","year":"2009","unstructured":"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\u2013105 (2009). https:\/\/doi.org\/10.1145\/1467247.1467271","journal-title":"Commun. ACM"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"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\u2013198. IEEE (2015). https:\/\/doi.org\/10.1145\/2728606.2728633","DOI":"10.1145\/2728606.2728633"},{"issue":"1","key":"2_CR49","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-018-0319-x","volume":"53","author":"S Jaksic","year":"2018","unstructured":"Jaksic, S., Bartocci, E., Grosu, R., Nguyen, T., Nickovic, D.: Quantitative monitoring of STL with edit distance. Formal Methods Syst. Des. 53(1), 83\u2013112 (2018). https:\/\/doi.org\/10.1007\/s10703-018-0319-x","journal-title":"Formal Methods Syst. Des."},{"issue":"11","key":"2_CR50","doi-asserted-by":"publisher","first-page":"2233","DOI":"10.1109\/TCAD.2018.2858460","volume":"37","author":"S Jaksic","year":"2018","unstructured":"Jaksic, S., Bartocci, E., Grosu, R., Nickovic, D.: An algebraic framework for runtime verification. IEEE Trans. CAD Integr. Circuits Syst. 37(11), 2233\u20132243 (2018). https:\/\/doi.org\/10.1109\/TCAD.2018.2858460","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"2_CR51","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1038\/290091a0","volume":"290","author":"B Julesz","year":"1981","unstructured":"Julesz, B.: Textons, the elements of texture perception, and their interactions. Nature 290, 91\u201397 (1981)","journal-title":"Nature"},{"issue":"4","key":"2_CR52","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990). https:\/\/doi.org\/10.1007\/BF01995674","journal-title":"Real-Time Syst."},{"key":"2_CR53","volume-title":"Introduction to Embedded Systems, A Cyber-Physical Systems Approach","author":"EA Lee","year":"2017","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems, A Cyber-Physical Systems Approach, 2nd edn. MIT Press, Berlin (2017)","edition":"2"},{"key":"2_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-34096-8_4","volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems","author":"M Loreti","year":"2016","unstructured":"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\u2013119. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-34096-8_4"},{"key":"2_CR55","doi-asserted-by":"crossref","unstructured":"Lowe, D.G.: Object recognition from local scale-invariant features. In: Proceedings of the International Conference on Computer Vision, vol. 2, pp. 1150\u20131157 (1999)","DOI":"10.1109\/ICCV.1999.790410"},{"key":"2_CR56","doi-asserted-by":"publisher","unstructured":"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\u201362. IEEE (2020). https:\/\/doi.org\/10.1109\/ICCPS48487.2020.00013","DOI":"10.1109\/ICCPS48487.2020.00013"},{"key":"2_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"issue":"3","key":"2_CR58","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler, O., Ni\u010dkovi\u0107, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247\u2013268 (2013)","journal-title":"STTT"},{"issue":"6","key":"2_CR59","doi-asserted-by":"publisher","first-page":"897","DOI":"10.1093\/logcom\/9.6.897","volume":"9","author":"M Marx","year":"1999","unstructured":"Marx, M., Reynolds, M.: Undecidability of compass logic. J. Logic Comput. 9(6), 897\u2013914 (1999). https:\/\/doi.org\/10.1093\/logcom\/9.6.897","journal-title":"J. Logic Comput."},{"issue":"2","key":"2_CR60","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1109\/TCBB.2012.125","volume":"10","author":"A Murthy","year":"2013","unstructured":"Murthy, A., et al.: Curvature analysis of cardiac excitation wavefronts. IEEE\/ACM Trans. Comput. Biol. Bioinform. 10(2), 323\u2013336 (2013). https:\/\/doi.org\/10.1109\/TCBB.2012.125","journal-title":"IEEE\/ACM Trans. Comput. Biol. Bioinform."},{"key":"2_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-23820-3_2","volume-title":"Runtime Verification","author":"L Nenzi","year":"2015","unstructured":"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\u201337. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_2"},{"key":"2_CR62","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.23638\/LMCS-14(4:2)2018"},{"key":"2_CR63","series-title":"Undergraduate Texts in Mathematics","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-319-02099-0_5","volume-title":"Introduction to Partial Differential Equations","author":"PJ Olver","year":"2014","unstructured":"Olver, P.J.: Finite differences. Introduction to Partial Differential Equations. UTM, pp. 181\u2013214. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-02099-0_5"},{"key":"2_CR64","doi-asserted-by":"publisher","first-page":"13260","DOI":"10.1109\/ACCESS.2019.2891969","volume":"7","author":"D Ratasich","year":"2019","unstructured":"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\u201313283 (2019). https:\/\/doi.org\/10.1109\/ACCESS.2019.2891969","journal-title":"IEEE Access"},{"key":"2_CR65","doi-asserted-by":"publisher","unstructured":"Rodionova, A., Bartocci, E., Ni\u010dkovi\u0107, D., Grosu, R.: Temporal logic as filtering. In: Proceedings of HSCC 2016, pp. 11\u201320. ACM (2016). https:\/\/doi.org\/10.1145\/2883817.2883839","DOI":"10.1145\/2883817.2883839"},{"key":"2_CR66","volume-title":"Artificial Intelligence: A Modern Approach","author":"SJ Russell","year":"2002","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice Hall, Upper Saddle River (2002)"},{"issue":"2","key":"2_CR67","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/3076125.3076128","volume":"14","author":"S Sankaranarayanan","year":"2017","unstructured":"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\u201333 (2017). https:\/\/doi.org\/10.1145\/3076125.3076128","journal-title":"SIGBED Rev."},{"key":"2_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-66845-1_1","volume-title":"Integrated Formal Methods","author":"S Silvetti","year":"2017","unstructured":"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\u201317. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_1"},{"key":"2_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-540-89437-7_6","volume-title":"Software-Intensive Systems and New Computing Paradigms","author":"C Talcott","year":"2008","unstructured":"Talcott, C.: Cyber-physical systems and events. In: Wirsing, M., Ban\u00e2tre, J.-P., H\u00f6lzl, M., Rauschmayer, A. (eds.) Software-Intensive Systems and New Computing Paradigms. LNCS, vol. 5380, pp. 101\u2013115. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89437-7_6"},{"key":"2_CR70","doi-asserted-by":"publisher","unstructured":"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\u201350. IEEE (2009). https:\/\/doi.org\/10.1109\/ICDCSW.2009.82","DOI":"10.1109\/ICDCSW.2009.82"},{"key":"2_CR71","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1098\/rstb.1952.0012","volume":"237","author":"AM Turing","year":"1952","unstructured":"Turing, A.M.: The chemical basis of morphogenesis. Philos. Trans. R. So. London B: Biol. Sci. 237, 37\u201372 (1952)","journal-title":"Philos. Trans. R. So. London B: Biol. Sci."},{"key":"2_CR72","doi-asserted-by":"publisher","unstructured":"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\u201318 May 2010, pp. 171\u2013172. ACM (2010). https:\/\/doi.org\/10.1145\/1785481","DOI":"10.1145\/1785481"},{"key":"2_CR73","doi-asserted-by":"publisher","unstructured":"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\u2013534. IEEE (2017). https:\/\/doi.org\/10.23919\/ACC.2017.7963007","DOI":"10.23919\/ACC.2017.7963007"},{"key":"2_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-24730-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"HLS Younes","year":"2004","unstructured":"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\u201360. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_4"},{"issue":"9","key":"2_CR75","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"HLS Younes","year":"2006","unstructured":"Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368\u20131409 (2006). https:\/\/doi.org\/10.1016\/j.ic.2006.05.002","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-60508-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T16:23:06Z","timestamp":1723738986000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-60508-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030605070","9783030605087"],"references-count":75,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-60508-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"2 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv20.ait.ac.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.95","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.82","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Also accepted and included: an invited paper, 5 tutorial, 6 tool papers, and a benchmark paper. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}