{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T15:20:24Z","timestamp":1774365624992,"version":"3.50.1"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,6,22]],"date-time":"2023-06-22T00:00:00Z","timestamp":1687392000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,6,22]],"date-time":"2023-06-22T00:00:00Z","timestamp":1687392000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100012306","name":"Universit\u00e0 degli Studi di Trieste","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100012306","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present <jats:sc>MoonLight<\/jats:sc>, a tool for monitoring temporal and spatio-temporal properties of mobile, spatially distributed, and interacting entities such as biological and cyber-physical systems. In <jats:sc>MoonLight<\/jats:sc> the space is represented as a weighted graph describing the topological configuration in which the single entities are arranged. Both nodes and edges have attributes modeling physical quantities and logical states of the system evolving in time. <jats:sc>MoonLight<\/jats:sc> is implemented in Java and supports the monitoring of Spatio-Temporal Reach and Escape Logic (STREL). <jats:sc>MoonLight<\/jats:sc> can be used as a standalone command line tool, such as Java API, or via <jats:sc>Matlab<\/jats:sc>\u2122 and <jats:sc>Python<\/jats:sc> interfaces. We provide here the description of the tool, its interfaces, and its scripting language using a sensor network and a bike sharing example. We evaluate the tool performances both by comparing it with other tools specialized in monitoring only temporal properties and by monitoring spatio-temporal requirements considering different sizes of dynamical and spatial graphs.<\/jats:p>","DOI":"10.1007\/s10009-023-00710-5","type":"journal-article","created":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T04:19:11Z","timestamp":1687493951000},"page":"503-517","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["MoonLight: a lightweight tool for monitoring spatio-temporal properties"],"prefix":"10.1007","volume":"25","author":[{"given":"Laura","family":"Nenzi","sequence":"first","affiliation":[]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Bortolussi","sequence":"additional","affiliation":[]},{"given":"Simone","family":"Silvetti","sequence":"additional","affiliation":[]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,22]]},"reference":[{"issue":"s2","key":"710_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., et al.: 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":"8","key":"710_CR2","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1109\/MCOM.2002.1024422","volume":"40","author":"I.F. Akyildiz","year":"2002","unstructured":"Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., et al.: 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":"710_CR3","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Proc. of TACAS 2011: The 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G.E., et al.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Proc. of TACAS 2011: The 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0254\u2013257 (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21"},{"issue":"2","key":"710_CR4","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":"4","key":"710_CR5","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1152\/advan.00034.2011","volume":"35","author":"E. Bartocci","year":"2011","unstructured":"Bartocci, E., et al.: 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":"710_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-26916-0_9","volume-title":"Proc. of HSB 2015","author":"E. Bartocci","year":"2015","unstructured":"Bartocci, E., Bortolussi, L., Milios, D., et al.: Studying emergent behaviours in morphogenesis using signal spatio-temporal logic. In: Proc. of HSB 2015. LNCS, vol.\u00a09271, pp.\u00a0156\u2013172. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-26916-0_9"},{"key":"710_CR7","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., et al.: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587, 3\u201325 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.02.046","journal-title":"Theor. Comput. Sci."},{"key":"710_CR8","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1145\/3127041.3127050","volume-title":"Proc. of MEMOCODE 2017: The 15th ACM-IEEE International Conference on Formal Methods and Models for System Design","author":"E. Bartocci","year":"2017","unstructured":"Bartocci, E., Bortolussi, L., Loreti, M., et al.: Monitoring mobile and spatially distributed cyber-physical systems. In: Proc. of MEMOCODE 2017: The 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp.\u00a0146\u2013155. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3127041.3127050"},{"key":"710_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-319-96145-3","volume-title":"Proc. of CAV 2018: The 30th International Conference on Computer Aided Verification","author":"E. Bartocci","year":"2018","unstructured":"Bartocci, E., Bloem, R., Nickovic, D., et al.: A counting semantics for monitoring LTL specifications over finite traces. In: Proc. of CAV 2018: The 30th International Conference on Computer Aided Verification. LNCS, vol.\u00a010981, pp.\u00a0547\u2013564. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3"},{"key":"710_CR10","series-title":"LNCS","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., Deshmukh, J., Donz\u00e9, A., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Lectures on Runtime Verification. LNCS, vol.\u00a010457, pp.\u00a0135\u2013175. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5"},{"key":"710_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5","volume-title":"Lectures on Runtime Verification \u2013 Introductory and Advanced Topics","author":"E. Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., et al.: Introduction to runtime verification. In: Lectures on Runtime Verification \u2013 Introductory and Advanced Topics. LNCS, vol.\u00a010457, pp.\u00a01\u201333. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5"},{"key":"710_CR12","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1145\/3178126.3178131","volume-title":"Proc. of HSCC 2018 the 21st International Conference on Hybrid Systems: Computation and Control","author":"E. Bartocci","year":"2018","unstructured":"Bartocci, E., Ferr\u00e8re, T., Manjunath, N., et al.: Localizing faults in simulink\/stateflow models with STL. In: Prandini, M., Deshmukh, J.V. (eds.) Proc. of HSCC 2018 the 21st International Conference on Hybrid Systems: Computation and Control, pp.\u00a0197\u2013206. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3178126.3178131"},{"issue":"1","key":"710_CR13","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1109\/TCNS.2016.2609138","volume":"5","author":"E. Bartocci","year":"2018","unstructured":"Bartocci, E., Gol, E.A., Haghighi, I., et al.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans. Control Netw. Syst. 5(1), 308\u2013320 (2018). https:\/\/doi.org\/10.1109\/TCNS.2016.2609138","journal-title":"IEEE Trans. Control Netw. Syst."},{"key":"710_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-30446-1_4","volume-title":"Proc. of SEFM 2019: The 17th International Conference on Software Engineering and Formal Methods","author":"E. Bartocci","year":"2019","unstructured":"Bartocci, E., Manjunath, N., Mariani, L., et al.: Automatic failure explanation in CPS models. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) Proc. of SEFM 2019: The 17th International Conference on Software Engineering and Formal Methods. LNCS, vol.\u00a011724, pp.\u00a069\u201386. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_4"},{"key":"710_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-030-60508-7_23","volume-title":"Proc. of RV 2020: The 20th International Conference on Runtime Verification","author":"E. Bartocci","year":"2020","unstructured":"Bartocci, E., Bortolussi, L., Loreti, M., et al.: Moonlight: a lightweight tool for monitoring spatio-temporal properties. In: Deshmukh, J., Nickovic, D. (eds.) Proc. of RV 2020: The 20th International Conference on Runtime Verification. LNCS, vol.\u00a012399, pp.\u00a0417\u2013428. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_23"},{"key":"710_CR16","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1145\/3395363.3404369","volume-title":"Proc. of ISSTA \u201920: The 29th ACM SIGSOFT International Symposium on Software Testing and Analysis","author":"E. Bartocci","year":"2020","unstructured":"Bartocci, E., Manjunath, N., Mariani, L., et al.: CPSDebug: a tool for explanation of failures in cyber-physical systems. In: Khurshid, S., Pasareanu, C.S. (eds.) Proc. of ISSTA \u201920: The 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp.\u00a0569\u2013572. ACM, New York (2020). https:\/\/doi.org\/10.1145\/3395363.3404369"},{"issue":"5s","key":"710_CR17","doi-asserted-by":"publisher","first-page":"88:1","DOI":"10.1145\/3358220","volume":"18","author":"J. Baumeister","year":"2019","unstructured":"Baumeister, J., Finkbeiner, B., Schwenger, M., et al.: FPGA stream-monitoring of real-time properties. ACM Trans. Embed. Comput. Syst. 18(5s), 88:1\u201388:24 (2019). https:\/\/doi.org\/10.1145\/3358220","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"710_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-030-17462-0_16","volume-title":"Proc. of TACAS 2019: The 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Belmonte","year":"2019","unstructured":"Belmonte, G., Ciancia, V., Latella, D., et al.: Voxlogica: a spatial model checker for declarative image analysis. In: Proc. of TACAS 2019: The 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol.\u00a011427, pp.\u00a0281\u2013298. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_16"},{"key":"710_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-319-22264-6_6","volume-title":"Proc. of QEST 2015: 12th Inter. Conf. on 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: Proc. of QEST 2015: 12th Inter. Conf. on Quantitative Evaluation of Systems. LNCS, vol.\u00a09259, pp.\u00a089\u2013104. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-22264-6_6"},{"key":"710_CR20","unstructured":"City of Melbourne: Melbourne Bike Share Station Readings 2011-2017 [Dataset]. https:\/\/www.opendatanetwork.com\/dataset\/data.melbourne.vic.gov.au\/74id-aqj9 (2018)"},{"key":"710_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6","volume-title":"Proc. of CAV 2010: The 22nd International Conference on Computer Aided Verification","author":"A. Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proc. of CAV 2010: The 22nd International Conference on Computer Aided Verification. LNCS, vol.\u00a06174, pp.\u00a0167\u2013170. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6"},{"key":"710_CR22","first-page":"92","volume-title":"Proc. of FORMATS","author":"A. Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Proc. of FORMATS, pp.\u00a092\u2013106. Springer, Berlin (2010)"},{"key":"710_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-02008-7_11","volume-title":"Proc. of RECOMB 2009: The 13th Annual International Conference on Research in Computational Molecular Biology","author":"A. Donz\u00e9","year":"2009","unstructured":"Donz\u00e9, A., Clermont, G., Legay, A., et al.: Parameter synthesis in nonlinear dynamical systems: application to systems biology. In: Proc. of RECOMB 2009: The 13th Annual International Conference on Research in Computational Molecular Biology. LNCS, vol.\u00a05541, pp.\u00a0155\u2013169. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-02008-7_11"},{"key":"710_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-00602-9_12","volume-title":"Proc. of HSCC 2009: The 12th International Conference on 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: Proc. of HSCC 2009: The 12th International Conference on Hybrid Systems: Computation and Control. LNCS, vol.\u00a05469, pp.\u00a0165\u2013179. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-00602-9_12"},{"key":"710_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-39799-8_19","volume-title":"Proc. of CAV 2013: The 25th International Conference on Computer Aided Verification","author":"A. Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Proc. of CAV 2013: The 25th International Conference on Computer Aided Verification. LNCS, vol.\u00a08044, pp.\u00a0264\u2013279. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19"},{"issue":"42","key":"710_CR26","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"G.E. Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"710_CR27","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., et al.: 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":"710_CR28","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1145\/2728606.2728633","volume-title":"Proc. of HSCC\u201915: The 18th International Conference on Hybrid Systems: Computation and Control","author":"I. Haghighi","year":"2015","unstructured":"Haghighi, I., Jones, A., Kong, Z., et al.: SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In: Proc. of HSCC\u201915: The 18th International Conference on Hybrid Systems: Computation and Control, pp.\u00a0189\u2013198. IEEE, New York (2015). https:\/\/doi.org\/10.1145\/2728606.2728633"},{"key":"710_CR29","series-title":"EPiC Series in Computing","doi-asserted-by":"publisher","first-page":"25","DOI":"10.29007\/xwrs","volume-title":"Proc. of ARCH@CPSWeek 2014: The 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems","author":"B. Hoxha","year":"2015","unstructured":"Hoxha, B., Abbas, H., Fainekos, G.E.: Benchmarks for temporal logic requirements for automotive systems. In: Proc. of ARCH@CPSWeek 2014: The 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a034, pp.\u00a025\u201330. EasyChair (2015). https:\/\/doi.org\/10.29007\/xwrs"},{"issue":"1","key":"710_CR30","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., et al.: Quantitative monitoring of STL with edit distance. Form. Methods Syst. Des. 53(1), 83\u2013112 (2018). https:\/\/doi.org\/10.1007\/s10703-018-0319-x","journal-title":"Form. Methods Syst. Des."},{"issue":"11","key":"710_CR31","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., et al.: An algebraic framework for runtime verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 37(11), 2233\u20132243 (2018). https:\/\/doi.org\/10.1109\/TCAD.2018.2858460","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"710_CR32","doi-asserted-by":"publisher","first-page":"175","DOI":"10.3354\/meps13386","volume":"646","author":"A. Kane","year":"2020","unstructured":"Kane, A., Pirotta, E., Wischnewski, S., et al.: Spatio-temporal patterns of foraging behaviour in a wide-ranging seabird reveal the role of primary productivity in locating prey. Mar. Ecol. Prog. Ser. 646, 175\u2013188 (2020). https:\/\/doi.org\/10.3354\/meps13386","journal-title":"Mar. Ecol. Prog. Ser."},{"issue":"4","key":"710_CR33","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."},{"issue":"4","key":"710_CR34","first-page":"328","volume":"13","author":"D. Lemire","year":"2006","unstructured":"Lemire, D.: Streaming maximum-minimum filter using no more than three comparisons per element. Nord. J. Comput. 13(4), 328\u2013339 (2006)","journal-title":"Nord. J. Comput."},{"key":"710_CR35","doi-asserted-by":"publisher","first-page":"1925","DOI":"10.1145\/3167132.3167338","volume-title":"Proc. of SAC 2018: The 33rd Annual ACM Symposium on Applied Computing","author":"M. Leucker","year":"2018","unstructured":"Leucker, M., S\u00e1nchez, C., Scheffel, T., et al.: Tessla: runtime verification of non-synchronized real-time streams. In: Proc. of SAC 2018: The 33rd Annual ACM Symposium on Applied Computing, pp.\u00a01925\u20131933. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3167132.3167338"},{"key":"710_CR36","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-34096-8","volume-title":"Proc. of SFM 2016: Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems \u2013 16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems","author":"M. Loreti","year":"2016","unstructured":"Loreti, M., Hillston, J.: Modelling and analysis of collective adaptive systems with CARMA and its tools. In: Proc. of SFM 2016: Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems \u2013 16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. LNCS, vol.\u00a09700, pp.\u00a083\u2013119. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-319-34096-8"},{"key":"710_CR37","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-662-54580-5_17","volume-title":"Proc. of TACAS 2017: The 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Lukina","year":"2017","unstructured":"Lukina, A., Esterle, L., Hirsch, C., et al.: ARES: adaptive receding-horizon synthesis of optimal plans. In: Proc. of TACAS 2017: The 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0286\u2013302 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_17"},{"key":"710_CR38","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1109\/ICCPS48487.2020.00013","volume-title":"11th ACM\/IEEE International Conference on Cyber-Physical Systems, ICCPS 2020","author":"M. Ma","year":"2020","unstructured":"Ma, M., Bartocci, E., Lifland, E., et al.: SaSTL: spatial aggregation signal temporal logic for runtime monitoring in smart cities. In: 11th ACM\/IEEE International Conference on Cyber-Physical Systems, ICCPS 2020, Sydney, Australia, April 21\u201325, 2020, pp.\u00a051\u201362. IEEE, New York (2020). https:\/\/doi.org\/10.1109\/ICCPS48487.2020.00013"},{"key":"710_CR39","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":"Proc. of FORMATS\/FTRTFT","author":"O. Maler","year":"2004","unstructured":"Maler, O., Ni\u010dkovi\u0107, D.: Monitoring temporal properties of continuous signals. In: Proc. of FORMATS\/FTRTFT. Lecture Notes in Computer Science, vol.\u00a03253, pp.\u00a0152\u2013166. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"issue":"3","key":"710_CR40","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. Int. J. Softw. Tools Technol. Transf. 15(3), 247\u2013268 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0247-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"710_CR41","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10703-017-0275-x","volume":"51","author":"P. Moosbrugger","year":"2017","unstructured":"Moosbrugger, P., Rozier, K.Y., Schumann, J.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. Form. Methods Syst. Des. 51(1), 31\u201361 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0275-x","journal-title":"Form. Methods Syst. Des."},{"key":"710_CR42","doi-asserted-by":"publisher","DOI":"10.4108\/eai.25-10-2016.2266978","volume-title":"Proc. of VALUETOOLS 2016: The 10th EAI International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2016","author":"L. Nenzi","year":"2016","unstructured":"Nenzi, L., Bortolussi, L., Loreti, M.: jSSTL \u2013 a tool to monitor spatio-temporal properties. In: Proc. of VALUETOOLS 2016: The 10th EAI International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2016. ACM, New York (2016). https:\/\/doi.org\/10.4108\/eai.25-10-2016.2266978"},{"issue":"4","key":"710_CR43","doi-asserted-by":"publisher","first-page":"1","DOI":"10.23638\/LMCS-14(4:2)2018","volume":"14","author":"L. Nenzi","year":"2018","unstructured":"Nenzi, L., Bortolussi, L., Ciancia, V., et al.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Log. Methods Comput. Sci. 14(4), 1\u201338 (2018). https:\/\/doi.org\/10.23638\/LMCS-14(4:2)2018","journal-title":"Log. Methods Comput. Sci."},{"key":"710_CR44","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-60508-7_2","volume-title":"Proc. of RV 2020: The 20th International Conference on Runtime Verification","author":"L. Nenzi","year":"2020","unstructured":"Nenzi, L., Bartocci, E., Bortolussi, L., et al.: Monitoring spatio-temporal properties (invited tutorial). In: Proc. of RV 2020: The 20th International Conference on Runtime Verification. LNCS, vol.\u00a012399, pp.\u00a021\u201346. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_2"},{"issue":"1","key":"710_CR45","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.46298\/lmcs-18(1:4)2022","volume":"18","author":"L. Nenzi","year":"2022","unstructured":"Nenzi, L., Bartocci, E., Bortolussi, L., et al.: A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems. Log. Methods Comput. Sci. 18(1), 4:1\u20134:30 (2022). https:\/\/lmcs.episciences.org\/8936. https:\/\/doi.org\/10.46298\/lmcs-18(1:4)2022","journal-title":"Log. Methods Comput. Sci."},{"key":"710_CR46","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-030-59152-6","volume-title":"Proc. of ATVA 2020: The 18th International Symposium on Automated Technology for Verification and Analysis \u2013 18th International Symposium","author":"D. Nickovic","year":"2020","unstructured":"Nickovic, D., Yamaguchi, T.: RTAMT: online robustness monitors from STL. In: Proc. of ATVA 2020: The 18th International Symposium on Automated Technology for Verification and Analysis \u2013 18th International Symposium. LNCS, vol.\u00a012302, pp.\u00a0564\u2013571. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6"},{"key":"710_CR47","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-319-89963-3","volume-title":"Proc. of TACAS 2018: The 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Nickovic","year":"2018","unstructured":"Nickovic, D., Lebeltel, O., Maler, O., et al.: AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. In: Proc. of TACAS 2018: The 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol.\u00a010806, pp.\u00a0303\u2013319. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3"},{"key":"710_CR48","volume-title":"The Definitive ANTLR 4 Reference","author":"T. Parr","year":"2013","unstructured":"Parr, T.: The Definitive ANTLR 4 Reference, 2nd edn. Pragmatic Bookshelf, Raleigh (2013)","edition":"2"},{"key":"710_CR49","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., et al.: A roadmap towards 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":"710_CR50","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/2883817.2883839","volume-title":"Proc. of HSCC 2016","author":"A. Rodionova","year":"2016","unstructured":"Rodionova, A., Bartocci, E., Ni\u010dkovi\u0107, D., et al.: Temporal logic as filtering. In: Proc. of HSCC 2016, pp.\u00a011\u201320. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2883817.2883839"},{"issue":"2","key":"710_CR51","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., et al.: 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":"710_CR52","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-66845-1","volume-title":"Proc. of IFM 2017: The 13th International Conference on 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: Proc. of IFM 2017: The 13th International Conference on Integrated Formal Methods. LNCS, vol.\u00a010510, pp.\u00a03\u201317. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1"},{"key":"710_CR53","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-319-63387-9","volume-title":"Proc. of CAV 2017: The 29th International Conference on Computer Aided Verification","author":"D. Ulus","year":"2017","unstructured":"Ulus, D.: Montre: a tool for monitoring timed regular expressions. In: Proc. of CAV 2017: The 29th International Conference on Computer Aided Verification. LNCS, vol.\u00a010426, pp.\u00a0329\u2013335. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9"},{"key":"710_CR54","doi-asserted-by":"publisher","first-page":"529","DOI":"10.23919\/ACC.2017.7963007","volume-title":"Proc. ACC 2017: The 2017 American Control Conference","author":"S. Yaghoubi","year":"2017","unstructured":"Yaghoubi, S., Fainekos, G.: Hybrid approximate gradient and stochastic descent for falsification of nonlinear systems. In: Proc. ACC 2017: The 2017 American Control Conference, pp.\u00a0529\u2013534. IEEE, New York (2017). https:\/\/doi.org\/10.23919\/ACC.2017.7963007"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00710-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-023-00710-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00710-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,9]],"date-time":"2023-11-09T09:04:59Z","timestamp":1699520699000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-023-00710-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,22]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["710"],"URL":"https:\/\/doi.org\/10.1007\/s10009-023-00710-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,22]]},"assertion":[{"value":"30 May 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 June 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}