{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:39Z","timestamp":1740107979355,"version":"3.37.3"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,2,22]],"date-time":"2024-02-22T00:00:00Z","timestamp":1708560000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,2,22]],"date-time":"2024-02-22T00:00:00Z","timestamp":1708560000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005855","name":"Universidade Nova de Lisboa","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005855","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":[[2024,4]]},"abstract":"Abstract<\/jats:title>The automotive industry is increasingly dependent on computing systems with different critical requirements. The verification and validation methods for these systems are now leveraging complex AI methods, for which the decision algorithms introduce non-determinism, especially in autonomous driving. This paper presents a runtime verification technique agnostic to the target system, which focuses on monitoring spatio-temporal properties that abstract the evolution of objects\u2019 behavior in their spatial and temporal flow. First, a formalization of three known traffic rules (from the Vienna convention on road traffic) is presented, where a spatio-temporal logic fragment is used. Then, these logical expressions are translated to a monitoring model written in first-order logic, where they are processed by a non-linear satisfiability solver. Finally, the translation allows the solver to check the validity of the encoded properties according to an instance of a specific traffic scenario (a trace). The results obtained from our tool, which automatically generates a monitor from a formula, show that our approach is feasible for online monitoring in a real-world environment.<\/jats:p>","DOI":"10.1007\/s10009-024-00740-7","type":"journal-article","created":{"date-parts":[[2024,2,22]],"date-time":"2024-02-22T09:07:00Z","timestamp":1708592820000},"page":"169-188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Monitoring of spatio-temporal properties with nonlinear SAT solvers"],"prefix":"10.1007","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9452-0995","authenticated-orcid":false,"given":"Andr\u00e9","family":"Matos\u00a0Pedro","sequence":"first","affiliation":[]},{"given":"Tom\u00e1s","family":"Silva","sequence":"additional","affiliation":[]},{"given":"Tiago","family":"Sequeira","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8495-6442","authenticated-orcid":false,"given":"Jo\u00e3o","family":"Louren\u00e7o","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2840-3966","authenticated-orcid":false,"given":"Jo\u00e3o Costa","family":"Seco","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3680-7634","authenticated-orcid":false,"given":"Carla","family":"Ferreira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,2,22]]},"reference":[{"key":"740_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5587-4","volume-title":"Handbook of Spatial Logics","author":"M. Aiello","year":"2007","unstructured":"Aiello, M., Pratt-Hartmann, I., van Benthem, J.: Handbook of Spatial Logics. Springer, Berlin (2007)"},{"issue":"1","key":"740_CR2","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/s10458-021-09529-3","volume":"36","author":"M.E. Akintunde","year":"2022","unstructured":"Akintunde, M.E., Botoeva, E., Kouvaros, P., Lomuscio, A.: Formal verification of neural agents in non-deterministic environments. Auton. Agents Multi-Agent Syst. 36(1), 6 (2022)","journal-title":"Auton. Agents Multi-Agent Syst."},{"key":"740_CR3","series-title":"LNCS","first-page":"217","volume-title":"FM Workshops 2019. Proceedings","author":"G.V. Alves","year":"2019","unstructured":"Alves, G.V., Dennis, L.A., Fisher, M.: Formalisation and implementation of road junction rules on an autonomous vehicle modelled as an agent. In: FM Workshops 2019. Proceedings, Porto, Portugal, October, 2019. LNCS, vol.\u00a012232, pp.\u00a0217\u2013232. Springer, Berlin (2019)"},{"issue":"3","key":"740_CR4","doi-asserted-by":"publisher","first-page":"41","DOI":"10.3390\/jsan10030041","volume":"10","author":"G.V. Alves","year":"2021","unstructured":"Alves, G.V., Dennis, L.A., Fisher, M.: A double-level model checking approach for an agent-based autonomous vehicle and road junction regulations. J. Sens. Actuator Netw. 10(3), 41 (2021)","journal-title":"J. Sens. Actuator Netw."},{"key":"740_CR5","first-page":"58","volume-title":"2019 IEEE Intelligent Vehicles Symposium, IV 2019","author":"N. Ar\u00e9chiga","year":"2019","unstructured":"Ar\u00e9chiga, N.: Specifying safety of autonomous vehicles in signal temporal logic. In: 2019 IEEE Intelligent Vehicles Symposium, IV 2019, Paris, France, June 9-12, 2019, pp.\u00a058\u201363. IEEE, Los Alamitos (2019)"},{"key":"740_CR6","unstructured":"Association for Standardisation of Automation and Measuring Systems. https:\/\/www.asam.net\/standards\/. Retrieved 2022-04-11"},{"key":"740_CR7","first-page":"146","volume-title":"Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE \u201917","author":"E. Bartocci","year":"2017","unstructured":"Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE \u201917, pp.\u00a0146\u2013155. Assoc. Comput. Mach., New York (2017)"},{"issue":"1","key":"740_CR8","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., Belta, C.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans. Control Netw. Syst. 5(1), 308\u2013320 (2018)","journal-title":"IEEE Trans. Control Netw. Syst."},{"issue":"3","key":"740_CR9","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)","journal-title":"Appl. Intell."},{"key":"740_CR10","series-title":"Frontiers in Artificial Intellig and Applications","first-page":"3","volume-title":"JURIX 2020","author":"H. Bhuiyan","year":"2020","unstructured":"Bhuiyan, H., Governatori, G., Bond, A., Demmel, S., Islam, M.B., Rakotonirainy, A.: Traffic rules encoding using defeasible deontic logic. In: JURIX 2020, Brno, Czech Republic, December, 2020. Frontiers in Artificial Intellig and Applications, vol.\u00a0334, pp.\u00a03\u201312. IOS Press, Amsterdam (2020)"},{"key":"740_CR11","first-page":"12","volume":"1","author":"M. Borg","year":"2018","unstructured":"Borg, M., Englund, C., Wnuk, K., Duran, B., Levandowski, C., Gao, S., Tan, Y., Kaijser, H., L\u00f6nn, H., T\u00f6rnqvist, J.: Safely entering the deep: a review of verification and validation for machine learning and a challenge elicitation in the automotive industry. J. Autom. Softw. Eng. 1, 12 (2018)","journal-title":"J. Autom. Softw. Eng."},{"key":"740_CR12","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1109\/TIME.2010.22","volume-title":"TIME 2010\u201317th International Symposium on Temporal Representation and Reasoning","author":"D. Bresolin","year":"2010","unstructured":"Bresolin, D., Sala, P., Monica, D.D., Montanari, A., Sciavicco, G.: A decidable spatial generalization of metric interval temporal logic. In: Markey, N., Wijsen, J. (eds.) TIME 2010\u201317th International Symposium on Temporal Representation and Reasoning, Paris, France, 6\u20138 September 2010, pp.\u00a095\u2013102. IEEE Comput. Soc., Los Alamitos (2010)"},{"issue":"2","key":"740_CR13","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-019-00511-9","volume":"22","author":"F.B. Buonamici","year":"2020","unstructured":"Buonamici, F.B., Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Spatial logics and model checking for medical imaging. Int. J. Softw. Tools Technol. Transf. 22(2), 195\u2013217 (2020)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"740_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/s43154-021-00058-1","volume":"2","author":"R. Cardoso","year":"2021","unstructured":"Cardoso, R., Kourtis, G., Dennis, L., Dixon, C., Farrell, M., Fisher, M., Webster, M.: A review of verification and validation for space autonomous systems. Curr. Robot. Rep. 2, 09 (2021)","journal-title":"Curr. Robot. Rep."},{"key":"740_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-3-662-44602-7_18","volume-title":"Proceedings","author":"V. Ciancia","year":"2014","unstructured":"Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: D\u00edaz, J., Lanese, I., Sangiorgi, D. (eds.) Proceedings, Theoretical Computer Science \u2013 8th IFIP TC 1\/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Lecture Notes in Computer Science, vol.\u00a08705, pp.\u00a0222\u2013235. Springer, Berlin (2014)"},{"key":"740_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-3-662-49224-6_24","volume-title":"Software Engineering and Formal Methods \u2013 SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART","author":"V. Ciancia","year":"2015","unstructured":"Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) Software Engineering and Formal Methods \u2013 SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART, York, UK, September 7-8, 2015, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a09509, pp.\u00a0297\u2013311. Springer, Berlin (2015)"},{"key":"740_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/978-3-319-34096-8_6","volume-title":"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, SFM 2016, Advanced Lectures","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.) 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, SFM 2016, Advanced Lectures, Bertinoro, Italy, June 20-24, 2016. Lecture Notes in Computer Science, vol.\u00a09700, pp.\u00a0156\u2013201. Springer, Berlin (2016)"},{"key":"740_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1007\/978-3-319-47166-2_46","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques \u2013 7th International Symposium, ISoLA 2016, Imperial, Proceedings, Part I","author":"V. Ciancia","year":"2016","unstructured":"Ciancia, V., Latella, D., Massink, M., Paskauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques \u2013 7th International Symposium, ISoLA 2016, Imperial, Proceedings, Part I, Corfu, Greece, October 10-14, 2016. Lecture Notes in Computer Science, vol.\u00a09952, pp.\u00a0657\u2013673 (2016)"},{"issue":"3","key":"740_CR19","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10009-018-0483-8","volume":"20","author":"V. Ciancia","year":"2018","unstructured":"Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Int. J. Softw. Tools Technol. Transf. 20(3), 289\u2013311 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"740_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/978-3-031-15008-1_11","volume-title":"Formal Methods for Industrial Critical Systems \u2013 27th International Conference, FMICS 2022","author":"A. de Matos Pedro","year":"2022","unstructured":"de Matos Pedro, A., Silva, T., Sequeira, T.F., Louren\u00e7o, J., Seco, J.C., Ferreira, C.: Monitoring of spatio-temporal properties with nonlinear SAT solvers. In: Groote, J.F., Huisman, M. (eds.) Formal Methods for Industrial Critical Systems \u2013 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022. Lecture Notes in Computer Science, vol.\u00a013487, pp.\u00a0155\u2013171. Springer, Berlin (2022)"},{"key":"740_CR21","series-title":"LNCS","first-page":"337","volume-title":"TACAS 2008, Proceedings","author":"L. de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008, Proceedings, Budapest, Hungary, March, 2008. LNCS, vol.\u00a04963, pp.\u00a0337\u2013340. Springer, Berlin (2008)"},{"key":"740_CR22","series-title":"Machine Learning Research","first-page":"1","volume-title":"CoRL 2017. Proceedings","author":"A. Dosovitskiy","year":"2017","unstructured":"Dosovitskiy, A., Ros, G., Codevilla, F., L\u00f3pez, A.M., Koltun, V.: CARLA: an open urban driving simulator. In: CoRL 2017. Proceedings, Mountain View, California, USA, November, 2017. Machine Learning Research, vol.\u00a078, pp.\u00a01\u201316. PMLR (2017)"},{"key":"740_CR23","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp.\u00a0995\u20131072. MIT Press, Cambridge (1990)"},{"key":"740_CR24","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1613\/jair.1537","volume":"23","author":"D. Gabelaia","year":"2005","unstructured":"Gabelaia, D., Kontchakov, R., Kurucz, \u00c1., Wolter, F., Zakharyaschev, M.: Combining spatial and temporal logics: expressiveness vs. complexity. J. Artif. Intell. Res. 23, 167\u2013243 (2005)","journal-title":"J. Artif. Intell. Res."},{"key":"740_CR25","series-title":"Proceedings","first-page":"312","volume-title":"ECAI\u20192002","author":"A. Gerevini","year":"2002","unstructured":"Gerevini, A., Nebel, B.: Qualitative spatio-temporal reasoning with RCC-8 and Allen\u2019s interval calculus: computational complexity. In: ECAI\u20192002, Lyon, France, July 2002. Proceedings, pp.\u00a0312\u2013316. IOS Press, Amsterdam (2002)"},{"issue":"3","key":"740_CR26","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)","journal-title":"Commun. ACM"},{"key":"740_CR27","series-title":"Proceedings","first-page":"189","volume-title":"HSCC\u201915","author":"I. Haghighi","year":"2015","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: HSCC\u201915, Seattle, WA, USA, April, 2015. Proceedings, pp.\u00a0189\u2013198. ACM, New York (2015)"},{"key":"740_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1007\/978-3-642-24559-6_28","volume-title":"Formal Methods and Software Engineering \u2013 13th International Conference on Formal Engineering Methods, ICFEM 2011. Proceedings","author":"M. Hilscher","year":"2011","unstructured":"Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering \u2013 13th International Conference on Formal Engineering Methods, ICFEM 2011. Proceedings, Durham, UK, October 26-28, 2011. Lecture Notes in Computer Science, vol.\u00a06991, pp.\u00a0404\u2013419. Springer, Berlin (2011)"},{"key":"740_CR29","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2020.100270","volume":"37","author":"X. Huang","year":"2020","unstructured":"Huang, X., Kroening, D., Ruan, W., Sharp, J., Sun, Y., Thamo, E., Wu, M., Yi, X.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020)","journal-title":"Comput. Sci. Rev."},{"key":"740_CR30","unstructured":"Kane, A.: Runtime Monitoring for Safety-Critical Embedded Systems. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (2015)"},{"key":"740_CR31","first-page":"193","volume-title":"We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two","author":"A. Kurucz","year":"2005","unstructured":"Kurucz, A., Wolter, F., Zakharyaschev, M.: Modal logics for metric spaces: open problems. In: We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two, pp.\u00a0193\u2013108. College Pub., London (2005)"},{"issue":"2","key":"740_CR32","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/635499.635504","volume":"4","author":"O. Kutz","year":"2003","unstructured":"Kutz, O., Wolter, F., Sturm, H., Suzuki, N.-Y., Zakharyaschev, M.: Logics of metric spaces. ACM Trans. Comput. Log. 4(2), 260\u2013294 (2003)","journal-title":"ACM Trans. Comput. Log."},{"issue":"5","key":"740_CR33","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M. Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Program. 78(5), 293\u2013303 (2009)","journal-title":"J. Log. Algebraic Program."},{"key":"740_CR34","first-page":"309","volume-title":"QRS 2020","author":"T. Li","year":"2020","unstructured":"Li, T., Liu, J., Kang, J., Yin, H., Yin, W., Chen, X., Stsl, H.W.: A novel spatio-temporal specification language for cyber-physical systems. In: QRS 2020, pp.\u00a0309\u2013319. IEEE, Los Alamitos (2020)"},{"key":"740_CR35","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1186\/s13677-020-00209-3","volume":"9","author":"T. Li","year":"2020","unstructured":"Li, T., Liu, J., Sun, H., Chen, X., Zhang, L., Sun, J.: A spatio-temporal specification language and its completeness & decidability. J. Cloud Comput. 9, 65 (2020)","journal-title":"J. Cloud Comput."},{"issue":"6","key":"740_CR36","doi-asserted-by":"publisher","first-page":"2392","DOI":"10.1007\/s11036-021-01779-5","volume":"26","author":"T. Li","year":"2021","unstructured":"Li, T., Liu, J., Sun, H., Chen, X., Yin, L., Mao, X., Sun, J.: Runtime verification of spatio-temporal specification language. Mob. Netw. Appl. 26(6), 2392\u20132406 (2021)","journal-title":"Mob. Netw. Appl."},{"key":"740_CR37","doi-asserted-by":"crossref","unstructured":"Linker, S., Hilscher, M.: Proof theory of a multi-lane spatial logic. Log. Methods Comput. Sci. 11(3) (2015)","DOI":"10.2168\/LMCS-11(3:4)2015"},{"key":"740_CR38","first-page":"51","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., Stankovic, J.A., Sastl, L.F.: 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, Los Alamitos (2020)"},{"key":"740_CR39","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1109\/IV47402.2020.9304549","volume-title":"IEEE Intelligent Vehicles Symposium, IV 2020","author":"S. Maierhofer","year":"2020","unstructured":"Maierhofer, S., Rettinger, A.-K., Mayer, E.C., Althoff, M.: Formalization of interstate traffic rules in temporal logic. In: IEEE Intelligent Vehicles Symposium, IV 2020, Las Vegas, NV, USA, October 19 \u2013 November 13, 2020, pp.\u00a0752\u2013759. IEEE, Los Alamitos (2020)"},{"key":"740_CR40","unstructured":"Mehmed, A.: Runtime monitoring for safe automated driving systems. PhD thesis, M\u00e4lardalen University (2020)"},{"key":"740_CR41","first-page":"131","volume-title":"KR\u201998","author":"P. Muller","year":"1998","unstructured":"Muller, P.: A qualitative theory of motion based on spatio-temporal primitives. In: KR\u201998, Trento, June, 1998, pp.\u00a0131\u2013143. Kaufmann, Los Altos (1998)"},{"key":"740_CR42","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)"},{"issue":"3","key":"740_CR43","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s10506-017-9210-0","volume":"25","author":"H. Prakken","year":"2017","unstructured":"Prakken, H.: On the problem of making autonomous vehicles conform to traffic law. Artif. Intell. Law 25(3), 341\u2013363 (2017)","journal-title":"Artif. Intell. Law"},{"issue":"1","key":"740_CR44","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/0022-0000(85)90003-0","volume":"30","author":"J.H. Reif","year":"1985","unstructured":"Reif, J.H., Sistla, A.P.: A multiprocess network logic with temporal and spatial modalities. J. Comput. Syst. Sci. 30(1), 41\u201353 (1985)","journal-title":"J. Comput. Syst. Sci."},{"key":"740_CR45","doi-asserted-by":"publisher","first-page":"87456","DOI":"10.1109\/ACCESS.2020.2993730","volume":"8","author":"S. Riedmaier","year":"2020","unstructured":"Riedmaier, S., Ponn, T., Ludwig, D., Schick, B., Diermeyer, F.: Survey on scenario-based safety assessment of automated vehicles. IEEE Access 8, 87456\u201387477 (2020)","journal-title":"IEEE Access"},{"key":"740_CR46","series-title":"LNCS","first-page":"50","volume-title":"IFM 2017","author":"A. Rizaldi","year":"2017","unstructured":"Rizaldi, A., Keinholz, J., Huber, M., Feldle, J., Immler, F., Althoff, M., Hilgendorf, E., Nipkow, T.: Formalising and monitoring traffic rules for autonomous vehicles in Isabelle\/hol. In: IFM 2017, Turin, Italy, September, 2017. LNCS, vol.\u00a010510, pp.\u00a050\u201366. Springer, Berlin (2017)"},{"key":"740_CR47","doi-asserted-by":"publisher","first-page":"454","DOI":"10.23919\/ACC45564.2020.9147917","volume-title":"2020 American Control Conference (ACC)","author":"Y.E. Sahin","year":"2020","unstructured":"Sahin, Y.E., Quirynen, R., Di Cairano, S.: Autonomous vehicle decision-making and monitoring based on signal temporal logic and mixed-integer programming. In: 2020 American Control Conference (ACC), pp.\u00a0454\u2013459 (2020)"},{"issue":"3","key":"740_CR48","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10703-019-00337-w","volume":"54","author":"C. S\u00e1nchez","year":"2019","unstructured":"S\u00e1nchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Falcone, Y., Francalanza, A., Krstic, S., Louren\u00e7o, J.M., Nickovic, D., Pace, G.J., Rufino, J., Signoles, J., Traytel, D., Weiss, A.: A survey of challenges for runtime verification from advanced application domains (beyond software). Form. Methods Syst. Des. 54(3), 279\u2013335 (2019)","journal-title":"Form. Methods Syst. Des."},{"key":"740_CR49","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.tcs.2018.05.028","volume":"744","author":"M. Schwammberger","year":"2018","unstructured":"Schwammberger, M.: An abstract model for proving safety of autonomous urban traffic. Theor. Comput. Sci. 744, 143\u2013169 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"740_CR50","series-title":"EPTCS","first-page":"1","volume-title":"Proceedings Third Workshop on Formal Methods for Autonomous Systems","author":"M. Schwammberger","year":"2021","unstructured":"Schwammberger, M., Vaz Alves, G.: Extending urban multi-lane spatial logic to formalise road junction rules. In: Farrell, M., Luckcuck, M. (eds.) Proceedings Third Workshop on Formal Methods for Autonomous Systems, FMAS 2021, Virtual, October 21-22, 2021. EPTCS, vol.\u00a0348, pp.\u00a01\u201319 (2021)"},{"key":"740_CR51","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1109\/ICECCS.2013.23","volume-title":"2013 18th International Conference on Engineering of Complex Computer Systems","author":"Z. Shao","year":"2013","unstructured":"Shao, Z., Liu, J., Ding, Z., Chen, M., Jiang, N.: Spatio-temporal properties analysis for cyber-physical systems. In: 2013 18th International Conference on Engineering of Complex Computer Systems, Singapore, July 17\u201319, 2013, pp.\u00a0101\u2013110. IEEE Comput. Soc., Los Alamitos (2013)"},{"key":"740_CR52","first-page":"254","volume-title":"2015 Asia-Pacific Software Engineering Conference, APSEC 2015","author":"H. Sun","year":"2015","unstructured":"Sun, H., Liu, J., Chen, X., Du, D.: Specifying cyber physical system safety properties with metric temporal spatial logic. In: Sun, J., Reddy, Y.R., Bahulkar, A., Pasala, A. (eds.) 2015 Asia-Pacific Software Engineering Conference, APSEC 2015, New Delhi, India, December 1-4, 2015, pp.\u00a0254\u2013260. IEEE Comput. Soc., Los Alamitos (2015)"},{"key":"740_CR53","series-title":"LNI","first-page":"113","volume-title":"Software Engineering und Software Management 2018, Fachtagung des GI-Fachbereichs Softwaretechnik, SE 2018, 5.-9. M\u00e4rz 2018, Ulm, Germany","author":"C. Tsigkanos","year":"2018","unstructured":"Tsigkanos, C., Kehrer, T., Ghezzi, C.: Modeling and verification of evolving cyber-physical spaces. In: Tichy, M., Bodden, E., Kuhrmann, M., Wagner, S., Stegh\u00f6fer, J.-P. (eds.) Software Engineering und Software Management 2018, Fachtagung des GI-Fachbereichs Softwaretechnik, SE 2018, 5.-9. M\u00e4rz 2018, Ulm, Germany. LNI, vol.\u00a0P\u2013279, pp.\u00a0113\u2013114. Gesellschaft f\u00fcr Informatik (2018)"},{"key":"740_CR54","unstructured":"United Nations: Vienna convention on road traffic (1968). https:\/\/unece.org\/DAM\/trans\/conventn\/Conv_road_traffic_eN.pdf. Retrieved 2022-04-11"},{"key":"740_CR55","first-page":"1481","volume-title":"2017 IEEE International Conference on Robotics and Automation, ICRA 2017","author":"C.I. Vasile","year":"2017","unstructured":"Vasile, C.I., Tumova, J., Karaman, S., Belta, C., Rus, D.: Minimum-violation scltl motion planning for mobility-on-demand. In: 2017 IEEE International Conference on Robotics and Automation, ICRA 2017, Singapore, Singapore, May 29 \u2013 June 3, 2017, pp.\u00a01481\u20131488. IEEE, Los Alamitos (2017)"},{"key":"740_CR56","first-page":"244","volume-title":"Proceedings of the 14th European Conference on Artificial Intelligence, ECAI\u201900","author":"F. Wolter","year":"2000","unstructured":"Wolter, F., Zakharyaschev, M.: Spatial reasoning in rcc-8 with Boolean region terms. In: Proceedings of the 14th European Conference on Artificial Intelligence, ECAI\u201900, pp.\u00a0244\u2013248, NLD. IOS Press, Amsterdam (2000)"},{"key":"740_CR57","series-title":"Proceedings","first-page":"1275","volume-title":"IJCAI\u201903","author":"F. Wolter","year":"2003","unstructured":"Wolter, F., Zakharyaschev, M.: Reasoning about distances. In: Gottlob, G., Walsh, T. (eds.) IJCAI\u201903, Acapulco, Mexico, August 9-15, 2003. Proceedings, pp.\u00a01275\u20131282. Kaufmann, San Mateo (2003)"},{"key":"740_CR58","series-title":"Proceedings","first-page":"33","volume-title":"ICECCS 2016","author":"B. Xu","year":"2016","unstructured":"Xu, B., Li, Q.: A spatial logic for modeling and verification of collision-free control of vehicles. In: ICECCS 2016, Dubai, United Arab Emirates, November, 2016. Proceedings, pp.\u00a033\u201342. IEEE Comput. Soc., Los Alamitos (2016)"}],"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-024-00740-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00740-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00740-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,21]],"date-time":"2024-03-21T16:05:26Z","timestamp":1711037126000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00740-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,22]]},"references-count":58,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["740"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00740-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2024,2,22]]},"assertion":[{"value":"6 February 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}