{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T16:16:10Z","timestamp":1762272970080,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031150074"},{"type":"electronic","value":"9783031150081"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-15008-1_11","type":"book-chapter","created":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:02:47Z","timestamp":1662332567000},"page":"155-171","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Monitoring of\u00a0Spatio-Temporal Properties with\u00a0Nonlinear SAT Solvers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9452-0995","authenticated-orcid":false,"given":"Andr\u00e9 de","family":"Matos Pedro","sequence":"first","affiliation":[]},{"given":"Tom\u00e1s","family":"Silva","sequence":"additional","affiliation":[]},{"given":"Tiago","family":"Sequeira","sequence":"additional","affiliation":[]},{"given":"Jo\u00e3o","family":"Louren\u00e7o","sequence":"additional","affiliation":[]},{"given":"Jo\u00e3o","family":"Costa Seco","sequence":"additional","affiliation":[]},{"given":"Carla","family":"Ferreira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,9,5]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Aiello, M., Pratt-Hartmann, I., van Benthem, J.: Handbook of Spatial Logics. Springer, Dordrecht (2007). https:\/\/doi.org\/10.1007\/978-1-4020-5587-4","key":"11_CR1","DOI":"10.1007\/978-1-4020-5587-4"},{"doi-asserted-by":"publisher","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), 1\u201336 (2021). https:\/\/doi.org\/10.1007\/s10458-021-09529-3","key":"11_CR2","DOI":"10.1007\/s10458-021-09529-3"},{"doi-asserted-by":"crossref","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)","key":"11_CR3","DOI":"10.3390\/jsan10030041"},{"doi-asserted-by":"crossref","unstructured":"Ar\u00e9chiga, N.: Specifying safety of autonomous vehicles in signal temporal logic. In: 2019 IEEE Intelligent Vehicles Symposium, IV 2019, Paris, France, 9\u201312 June 2019, pp. 58\u201363. IEEE (2019)","key":"11_CR4","DOI":"10.1109\/IVS.2019.8813875"},{"doi-asserted-by":"crossref","unstructured":"Bhuiyan, H., Governatori, G., Bond, A., Demmel, S., Badiul Islam, M., Rakotonirainy, A.: Traffic rules encoding using defeasible deontic logic. In: JURIX 2020, Brno, Czech Republic, December 2020, volume 334 of Frontiers in Artificial Intelligence and Applications, pp. 3\u201312. IOS Press (2020)","key":"11_CR5","DOI":"10.3233\/FAIA200844"},{"doi-asserted-by":"crossref","unstructured":"Borg, M., et al.: 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)","key":"11_CR6","DOI":"10.2991\/jase.d.190131.001"},{"doi-asserted-by":"crossref","unstructured":"Cardoso, R., et al.: A review of verification and validation for space autonomous systems. Curr. Robot. Rep. 2, 09 (2021)","key":"11_CR7","DOI":"10.1007\/s43154-021-00058-1"},{"doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","key":"11_CR8","DOI":"10.1007\/978-3-540-78800-3_24"},{"unstructured":"Dosovitskiy, A., Ros, G., Codevilla, F., L\u00f3pez, A.M., Koltun, V.: CARLA: an open urban driving simulator. In: CoRL 2017, Mountain View, California, USA, November 2017, Proceedings, volume 78 of Machine Learning Research, pp. 1\u201316. PMLR (2017)","key":"11_CR9"},{"doi-asserted-by":"crossref","unstructured":"Allen Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 995\u20131072. Elsevier and MIT Press, London (1990)","key":"11_CR10","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"unstructured":"Association for Standardisation\u00a0of Automation and Measuring Systems. https:\/\/www.asam.net\/standards\/. Accessed 11 Apr 2022","key":"11_CR11"},{"doi-asserted-by":"crossref","unstructured":"Gabelaia, D., Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: Combining spatial and temporal logics: expressiveness vs. complexity. J. Artif. Intell. Res. 23, 167\u2013243 (2005)","key":"11_CR12","DOI":"10.1613\/jair.1537"},{"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. 312\u2013316. IOS Press (2002)","key":"11_CR13"},{"doi-asserted-by":"crossref","unstructured":"Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: SpaTeLl: a novel spatial-temporal logic and its applications to networked systems: a novel spatial-temporal logic and its applications to networked systems. In: HSCC 2015, Seattle, WA, USA, April 2015. Proceedings, pp. 189\u2013198. ACM (2015)","key":"11_CR14","DOI":"10.1145\/2728606.2728633"},{"doi-asserted-by":"crossref","unstructured":"Huang, X., et al.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020)","key":"11_CR15","DOI":"10.1016\/j.cosrev.2020.100270"},{"unstructured":"Kane, A.: Runtime monitoring for safety-critical embedded systems. Ph.D. thesis, Carnegie Mellon University, Pittsburgh (2015)","key":"11_CR16"},{"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, Vol. 2, pp. 193\u2013108. College Publications (2005)","key":"11_CR17"},{"doi-asserted-by":"crossref","unstructured":"Kutz, O., Wolter, F., Sturm, H., Suzuki, N.-Y., Zakharyaschev, M.: Logics of metric spaces. ACM Trans. Com. Log. 4(2), 260\u2013294 (2003)","key":"11_CR18","DOI":"10.1145\/635499.635504"},{"doi-asserted-by":"crossref","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293\u2013303 (2009)","key":"11_CR19","DOI":"10.1016\/j.jlap.2008.08.004"},{"doi-asserted-by":"crossref","unstructured":"Li, T., STSL: a novel spatio-temporal specification language for cyber-physical systems. In: QRS 2020, pp. 309\u2013319. IEEE (2020)","key":"11_CR20","DOI":"10.1109\/QRS51102.2020.00048"},{"doi-asserted-by":"crossref","unstructured":"Maierhofer, S., Rettinger, A., Charlotte Mayer, E., Althoff, M.: Formalization of interstate traffic rules in temporal logic. In: 2020 IEEE Intelligent Vehicles Symposium (IV), pp. 752\u2013759. IEEE (2020)","key":"11_CR21","DOI":"10.1109\/IV47402.2020.9304549"},{"unstructured":"Mehmed, A.: Runtime monitoring for safe automated driving systems. Ph.D. thesis, M\u00e4lardalen University (2020)","key":"11_CR22"},{"unstructured":"Muller, P.: A qualitative theory of motion based on spatio-temporal primitives. In: KR1998, Trento, June 1998, pp. 131\u2013143. Morgan Kaufmann (1998)","key":"11_CR23"},{"unstructured":"United Nations. Vienna convention on road traffic (1968). https:\/\/unece.org\/DAM\/trans\/conventn\/Conv_road_traffic_EN.pdf. Accessed 11 Apr 2022","key":"11_CR24"},{"doi-asserted-by":"crossref","unstructured":"Pek, C., Zahn, P., Althoff, M.: Verifying the safety of lane change maneuvers of self-driving vehicles based on formalized traffic rules. In: 2017 IEEE Intelligent Vehicles Symposium (IV), pp. 1477\u20131483 (2017)","key":"11_CR25","DOI":"10.1109\/IVS.2017.7995918"},{"doi-asserted-by":"publisher","unstructured":"Prakken, H.: On the problem of making autonomous vehicles conform to traffic law. Artif. Intell. Law 25(3), 341\u2013363 (2017). https:\/\/doi.org\/10.1007\/s10506-017-9210-0","key":"11_CR26","DOI":"10.1007\/s10506-017-9210-0"},{"doi-asserted-by":"crossref","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)","key":"11_CR27","DOI":"10.1109\/ACCESS.2020.2993730"},{"doi-asserted-by":"publisher","unstructured":"Rizald, A., et al.: Formalising and monitoring traffic rules for autonomous vehicles in Isabelle\/HOL. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 50\u201366. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_4","key":"11_CR28","DOI":"10.1007\/978-3-319-66845-1_4"},{"doi-asserted-by":"crossref","unstructured":"Sahin, Y.M., 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. 454\u2013459 (2020)","key":"11_CR29","DOI":"10.23919\/ACC45564.2020.9147917"},{"doi-asserted-by":"publisher","unstructured":"S\u00e1nchez, C., et al.: A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 54, 279\u2013335 (2019). https:\/\/doi.org\/10.1007\/s10703-019-00337-w","key":"11_CR30","DOI":"10.1007\/s10703-019-00337-w"},{"doi-asserted-by":"crossref","unstructured":"Schwammberger, M., Alves, G.V.: Extending urban multi-lane spatial logic to formalise road junction rules. In: FMAS 2021, Virtual, October 2021. Proceedings, volume 348 of EPTCS, pp. 1\u201319 (2021)","key":"11_CR31","DOI":"10.4204\/EPTCS.348.1"},{"doi-asserted-by":"crossref","unstructured":"Vasile, C.-I., Tumova, J., Karaman, S., Belta, C., Rus, D.: Minimum-violation scLTL motion planning for mobility-on-demand. In: ICRA 2017, pp. 1481\u20131488 (2017)","key":"11_CR32","DOI":"10.1109\/ICRA.2017.7989177"},{"unstructured":"Wolter, F., Zakharyaschev, M.: Reasoning about distances. In: Gottlob, G., Walsh, T. (eds.) IJCAI 2003, Acapulco, Mexico, 9\u201315 August 2003. Proceedings, pp. 1275\u20131282. Morgan Kaufmann (2003)","key":"11_CR33"},{"doi-asserted-by":"crossref","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. 33\u201342. IEEE Computer Society (2016)","key":"11_CR34","DOI":"10.1109\/ICECCS.2016.014"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15008-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:09:49Z","timestamp":1662332989000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15008-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031150074","9783031150081"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15008-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"5 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Warsaw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmics2022.fsa.win.tue.nl\/","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":"22","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":"13","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":"0","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":"59% - 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","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":"2.5","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)"}}]}}