{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T02:42:50Z","timestamp":1772505770599,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031212215","type":"print"},{"value":"9783031212222","type":"electronic"}],"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"}],"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_11","type":"book-chapter","created":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T09:04:55Z","timestamp":1671095095000},"page":"187-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["MLTL Multi-type (MLTLM): A Logic for\u00a0Reasoning About Signals of\u00a0Different Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3447-2183","authenticated-orcid":false,"given":"Gokul","family":"Hariharan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2239-4218","authenticated-orcid":false,"given":"Brian","family":"Kempa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3977-122X","authenticated-orcid":false,"given":"Tichakorn","family":"Wongpiromsarn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8220-7552","authenticated-orcid":false,"given":"Phillip H.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Y.","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,16]]},"reference":[{"key":"11_CR1","unstructured":"Allen, J.F., Hayes, P.J.: A common-sense theory of time. In: Proceedings of the 9th International Joint Conference on Artificial Intelligence - Volume 1, IJCAI 1985, pp. 528\u2013531. Morgan Kaufmann Publishers Inc., San Francisco (1985)"},{"key":"11_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"11_CR3","unstructured":"Balbiani, P.: Time representation and temporal reasoning from the perspective of non-standard analysis. In: Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning, KR 2008, pp. 695\u2013704. AAAI Press (2008)"},{"issue":"1","key":"11_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1002\/malq.201700036","volume":"66","author":"S Baratella","year":"2020","unstructured":"Baratella, S., Masini, A.: A two-dimensional metric temporal logic. Math. Log. Q. 66(1), 7\u201319 (2020). https:\/\/doi.org\/10.1002\/malq.201700036","journal-title":"Math. Log. Q."},{"issue":"5s","key":"11_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358219","volume":"18","author":"O Bataineh","year":"2019","unstructured":"Bataineh, O., Rosenblum, D.S., Reynolds, M.: Efficient decentralized LTL monitoring framework using tableau technique. ACM Trans. Embed. Comput. Syst. 18(5s), 1\u201321 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-32759-9_10","volume-title":"FM 2012: Formal Methods","author":"A Bauer","year":"2012","unstructured":"Bauer, A., Falcone, Y.: Decentralised LTL monitoring. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 85\u2013100. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_10"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Bottoni, P., Fish, A.: Policy specifications with timed spider diagrams. In: 2011 IEEE Symposium on Visual Languages and Human-Centric Computing (VL\/HCC), pp. 95\u201398 (2011). https:\/\/doi.org\/10.1109\/VLHCC.2011.6070385","DOI":"10.1109\/VLHCC.2011.6070385"},{"issue":"2","key":"11_CR8","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1093\/logcom\/13.2.195","volume":"13","author":"H Bowman","year":"2003","unstructured":"Bowman, H., Thompson, S.: A decision procedure and complete axiomatization of finite interval temporal logic with projection. J. Log. Comput. 13(2), 195\u2013239 (2003). https:\/\/doi.org\/10.1093\/logcom\/13.2.195","journal-title":"J. Log. Comput."},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"11_CR10","unstructured":"Clifford, J., Rao, A.: A simple, general structure for temporal domains (1986)"},{"key":"11_CR11","unstructured":"Cohen-Solal, Q., Bouzid, M., Niveau, A.: An algebra of granular temporal relations for qualitative reasoning. In: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI 2015, pp. 2869\u20132875. AAAI Press (2015)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Dabney, J.B., Badger, J.M., Rajagopal, P.: Adding a verification view for an autonomous real-time system architecture. In: AIAA Scitech 2021 Forum, p. 0566 (2021)","DOI":"10.2514\/6.2021-0566"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249\u2013260. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_23"},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"1473","DOI":"10.1016\/j.procs.2016.05.468","volume":"80","author":"MN Dinh","year":"2016","unstructured":"Dinh, M.N., Abramson, D., Jin, C.: Runtime verification of scientific codes using statistics. Procedia Comput. Sci. 80, 1473\u20131484 (2016). https:\/\/doi.org\/10.1016\/j.procs.2016.05.468. International Conference on Computational Science 2016, ICCS 2016, 6\u20138 June 2016, San Diego, California, USA","journal-title":"Procedia Comput. Sci."},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Dinh, M.N., Trung Vo, C., Abramson, D.: Tracking scientific simulation using online time-series modelling. In: 2020 20th IEEE\/ACM International Symposium on Cluster, Cloud and Internet Computing (CCGRID), pp. 202\u2013211, May 2020. https:\/\/doi.org\/10.1109\/CCGrid49817.2020.00-73","DOI":"10.1109\/CCGrid49817.2020.00-73"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-642-40787-1_27","volume-title":"Runtime Verification","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A.: On signal temporal logic. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 382\u2013383. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_27"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Euzenat, J., Montanari, A.: Time granularity. In: Handbook of Temporal Reasoning in Artificial Intelligence, January 2005","DOI":"10.1016\/S1574-6526(05)80005-7"},{"issue":"2","key":"11_CR18","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1016\/j.jal.2005.06.004","volume":"4","author":"M Franceschet","year":"2006","unstructured":"Franceschet, M., Montanari, A., Peron, A., Sciavicco, G.: Definability and decidability of binary predicates for time granularity. J. Appl. Log. 4(2), 168\u2013191 (2006). https:\/\/doi.org\/10.1016\/j.jal.2005.06.004","journal-title":"J. Appl. Log."},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-11164-3_18","volume-title":"Runtime Verification","author":"J Geist","year":"2014","unstructured":"Geist, J., Rozier, K.Y., Schumann, J.: Runtime observer pairs and bayesian network reasoners on-board fpgas: flight-certifiable system health management for embedded systems. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 215\u2013230. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_18"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-030-57628-8_12","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B Kempa","year":"2020","unstructured":"Kempa, B., Zhang, P., Jones, P.H., Zambreno, J., Rozier, K.Y.: Embedding online runtime verification for fault disambiguation on Robonaut2. In: Bertrand, N., Jansen, N. (eds.) FORMATS 2020. LNCS, vol. 12288, pp. 196\u2013214. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57628-8_12"},{"issue":"1","key":"11_CR21","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.tcs.2006.12.014","volume":"373","author":"UD Lago","year":"2007","unstructured":"Lago, U.D., Montanari, A., Puppis, G.: Compact and tractable automaton-based representations of time granularities. Theor. Comput. Sci. 373(1), 115\u2013141 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.014","journal-title":"Theor. Comput. Sci."},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Lago, U.D., Montanari, A., Puppis, G.: On the equivalence of automaton-based representations of time granularities. In: 14th International Symposium on Temporal Representation and Reasoning (TIME 2007), pp. 82\u201393 (2007). https:\/\/doi.org\/10.1109\/TIME.2007.56","DOI":"10.1109\/TIME.2007.56"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-25543-5_1","volume-title":"Computer Aided Verification","author":"J Li","year":"2019","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 3\u201322. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_1"},{"key":"11_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-031-06773-0_28","volume-title":"NFM 2022","author":"Z Luppen","year":"2022","unstructured":"Luppen, Z., et al.: Elucidation and analysis of specification patterns in aerospace system telemetry. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 527\u2013537. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_28"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Montanari, A., Ratto, E., Corsetti, E., Morzenti, A.: Embedding time granularity in logical specifications of real-time systems. In: Proceedings of EUROMICRO 1991 Workshop on Real-Time Systems, pp. 88\u201397 (1991)","DOI":"10.1109\/EMWRT.1991.144087"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: 2015 IEEE International Parallel and Distributed Processing Symposium, pp. 494\u2013503 (2015)","DOI":"10.1109\/IPDPS.2015.95"},{"key":"11_CR27","unstructured":"Okubo, N.: Using R2U2 in JAXA program. Electronic correspondence, November\u2013December 2020. Series of emails and zoom call from JAXA to PI with technical questions about embedding R2U2 into an autonomous satellite mission with a provable memory bound of 200 KB"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1\u201313. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85778-5_1"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-54862-8_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357\u2013372. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_24"},{"key":"11_CR30","unstructured":"Rozier, K.Y., Schumann, J.: R2U2: tool overview. In: Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES), Seattle, WA, USA, vol. 3, pp. 138\u2013156. Kalpa Publications, September 2017"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-319-46982-9_35","volume-title":"Runtime Verification","author":"J Schumann","year":"2016","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime analysis with R2U2: a tool exhibition report. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 504\u2013509. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_35"},{"issue":"1","key":"11_CR32","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1), 72\u201399 (1983)","journal-title":"Inf. Control"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,10]],"date-time":"2024-10-10T13:11:18Z","timestamp":1728565878000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-21222-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031212215","9783031212222"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-21222-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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":"NSV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Numerical Software Verification","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":"11 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nsv2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nsv22.github.io\/","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":"4","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":"3","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":"75% - 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":"1","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)"}}]}}