{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T23:07:44Z","timestamp":1726182464506},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031212215"},{"type":"electronic","value":"9783031212222"}],"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.springernature.com\/gp\/researchers\/text-and-data-mining"},{"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.springernature.com\/gp\/researchers\/text-and-data-mining"},{"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.springernature.com\/gp\/researchers\/text-and-data-mining"},{"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.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-21222-2_8","type":"book-chapter","created":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T09:04:55Z","timestamp":1671095095000},"page":"131-143","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal Specification for\u00a0Learning-Enabled Autonomous Systems"],"prefix":"10.1007","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[]},{"given":"Chih-Hong","family":"Cheng","sequence":"additional","affiliation":[]},{"given":"Xiaowei","family":"Huang","sequence":"additional","affiliation":[]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[]},{"given":"Adam","family":"Molin","sequence":"additional","affiliation":[]},{"given":"Dejan","family":"Nickovic","sequence":"additional","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,16]]},"reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: AAAI 2018, pp. 2669\u20132678 (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"issue":"6","key":"8_CR3","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Balakrishnan, A., et al.: Specifying and evaluating quality metrics for vision-based perception systems. In: DATE, pp. 1433\u20131438 (2019)","DOI":"10.23919\/DATE.2019.8715114"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bloem, R., Maderbacher, B., Manjunath, N., Nickovic, D.: Adaptive testing for CPS with specification coverage. In: ADHS 2021 (2021)","DOI":"10.1016\/j.ifacol.2021.08.503"},{"key":"8_CR6","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"},{"issue":"2","key":"8_CR7","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 45 (2015)","journal-title":"J. ACM"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"Runtime Verification","author":"A Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126\u2013138. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77395-5_11"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2010","unstructured":"Bloem, R., et al.: RATSY \u2013 a new requirements analysis tool with synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 425\u2013429. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_37"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cordts, M., et al.: The cityscapes dataset for semantic urban scene understanding. CoRR, abs\/1604.01685 (2016)","DOI":"10.1109\/CVPR.2016.350"},{"key":"8_CR12","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":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/11940197_12","volume-title":"Formal Approaches to Software Testing and Runtime Verification","author":"GE Fainekos","year":"2006","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications. In: Havelund, K., N\u00fa\u00f1ez, M., Ro\u015fu, G., Wolff, B. (eds.) FATES\/RV 2006. LNCS, vol. 4262, pp. 178\u2013192. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11940197_12"},{"issue":"3","key":"8_CR14","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10703-011-0114-4","volume":"38","author":"Y Falcone","year":"2011","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223\u2013262 (2011)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Ferr\u00e8re, T., Nickovic, D., Donz\u00e9, A., Ito, H., Kapinski, J.: Interface-aware signal temporal logic. In: HSCC 2019, pp. 57\u201366 (2019)","DOI":"10.1145\/3302504.3311800"},{"volume-title":"A Brief Guide to the Standard Object Modeling Language","year":"2004","author":"M Fowler","key":"8_CR16","unstructured":"Fowler, M., Distilled, U.M.L.: A Brief Guide to the Standard Object Modeling Language. Addison-Wesley, Boston (2004)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D., Ulus, D.: First order temporal logic monitoring with BDDs. In: FMCAD 2017, pp. 116\u2013123 (2017)","DOI":"10.23919\/FMCAD.2017.8102249"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-46002-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"HS Hong","year":"2002","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 327\u2013341. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_23"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83, 91\u2013130 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G., Ivancic, F., Gupta, A., Pappas, G.: Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: HSCC 2010, pp. 211\u2013220 (2010)","DOI":"10.1145\/1755952.1755983"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Prabhakar, P., Lal, R., Kapinski, J.: Automatic trace generation for signal temporal logic. In: RTSS 2018, pp. 208\u2013217 (2018)","DOI":"10.1109\/RTSS.2018.00038"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Redmon, J., Divvala, S., Girshick, R., Farhadi, A.: You only look once: unified, real-time object detection. In: CVPR 2016, pp. 779\u2013788 (2016)","DOI":"10.1109\/CVPR.2016.91"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-319-63387-9_11","volume-title":"Computer Aided Verification","author":"H Roehm","year":"2017","unstructured":"Roehm, H., Heinz, T., Mayer, E.C.: STLInspector: STL validation with guarantees. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017, Part I. LNCS, vol. 10426, pp. 225\u2013232. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_11"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69061-0","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69061-0"},{"key":"8_CR26","series-title":"Ergebnisse der Mathematik und ihrer Grenzgebiete. 2. Folge","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"RR Smullyan","year":"2012","unstructured":"Smullyan, R.R.: First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete. 2. Folge, Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-86718-7"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-030-88494-9_18","volume-title":"Runtime Verification","author":"A Balakrishnan","year":"2021","unstructured":"Balakrishnan, A., Deshmukh, J., Hoxha, B., Yamaguchi, T., Fainekos, G.: PerceMon: online monitoring for\u00a0perception systems. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 297\u2013308. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_18"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Dutle, A., et al: From requirements to autonomous flight: an overview of the monitoring ICAROUS project. In: Proceedings of 2nd Workshop on Formal Methods for Autonomous Systems (FMAS). EPTCS, vol. 329, pp. 23\u201330 (2020)","DOI":"10.4204\/EPTCS.329.3"},{"issue":"4","key":"8_CR29","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)","journal-title":"Real-Time Syst.."}],"container-title":["Lecture Notes in Computer Science","Software Verification and Formal Methods for ML-Enabled Autonomous Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-21222-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T20:08:58Z","timestamp":1671134938000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-21222-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031212215","9783031212222"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-21222-2_8","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":"16 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoMLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Workshop on Formal Methods for ML-Enabled Autonomous Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","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":"31 July 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fomlas2022","order":10,"name":"conference_id","label":"Conference ID","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":"8","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":"8","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":"100% - 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":"2","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}