{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:56:08Z","timestamp":1776552968455,"version":"3.51.2"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031937057","type":"print"},{"value":"9783031937064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-93706-4_18","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:23:02Z","timestamp":1749316982000},"page":"313-332","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Language Partitioning for\u00a0Mission-Time Linear Temporal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-8186-3631","authenticated-orcid":false,"given":"A. E.","family":"Rosentrater","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6180","authenticated-orcid":false,"given":"Z.","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9336-6006","authenticated-orcid":false,"given":"Katherine","family":"Kosaian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"issue":"4","key":"18_CR1","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1002\/spe.2321","volume":"46","author":"G Cabodi","year":"2016","unstructured":"Cabodi, G., Camurati, P., Quer, S.: A graph-labeling approach for efficient cone-of-influence computation in model-checking problems with multiple properties. Softw. Pract. Exp. 46(4), 493\u2013511 (2016)","journal-title":"Softw. Pract. Exp."},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods Syst. Des. 10, 47\u201371 (1994). https:\/\/doi.org\/10.1023\/A:1008615614281","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Conrad, E., Titolo, L., Giannakopoulou, D., Pressburger, T., Dutle, A.: A compositional proof framework for FRETish requirements. In: Popescu, A., Zdancewic, S. (eds.) CPP 2022: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, 17\u201318 January 2022, pp. 68\u201381. ACM (2022). https:\/\/doi.org\/10.1145\/3497775.3503685","DOI":"10.1145\/3497775.3503685"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Dureja, R., Baumgartner, J., Ivrii, A., Kanzelman, R., Rozier, K.Y.: Boosting verification scalability via structural grouping and semantic partitioning of properties. In: 2019 Formal Methods in Computer Aided Design (FMCAD), pp.\u00a01\u20139. IEEE (2019)","DOI":"10.23919\/FMCAD.2019.8894265"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Dureja, R., Baumgartner, J., Kanzelman, R., Williams, M., Rozier, K.Y.: Accelerating parallel verification via complementary property partitioning and strategy exploration. In: # PLACEHOLDER_PARENT_METADATA_VALUE#, vol.\u00a01, pp. 16\u201325. TU Wien Academic Press (2020)","DOI":"10.23919\/FMCAD.2019.8894265"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-89960-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Dureja","year":"2018","unstructured":"Dureja, R., Rozier, K.Y.: More scalable LTL model checking via discovering design-space dependencies ($$D^{3}$$). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 309\u2013327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_17"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Elwing, J., Gamboa-Guzman, L., Sorkin, J., Travesset, C., Wang, Z., Rozier, K.Y.: Mission-time LTL (MLTL) formula validation via regular expressions. In: Herber, P., Wijs, A. (eds.) Proceedings of the 18th International Conference on integrated Formal Methods (iFM). LNCS, Formal Methods Subline, vol. 14300. Springer, Leiden (2023)","DOI":"10.1007\/978-3-031-47705-8_15"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Falco, G., Gilpin, L.H.: A stress testing framework for autonomous system verification and validation (v &v). In: 2021 IEEE International Conference on Autonomous Systems (ICAS), pp.\u00a01\u20135 (2021). https:\/\/doi.org\/10.1109\/ICAS49788.2021.9551154","DOI":"10.1109\/ICAS49788.2021.9551154"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Ghassabani, E., Gacek, A., Whalen, M.W., Heimdahl, M.P.E., Wagner, L.: Proof-based coverage metrics for formal verification. In: 2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 194\u2013199 (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115632","DOI":"10.1109\/ASE.2017.8115632"},{"key":"18_CR10","unstructured":"Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technical University Munich (2009). http:\/\/mediatum2.ub.tum.de\/node?id=886023"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Hagemeier, C., De\u00a0Giacomo, G., Vardi, M.Y.: LTLF synthesis under unreliable input. arXiv preprint arXiv:2412.14728 (2024)","DOI":"10.1609\/aaai.v39i14.33640"},{"issue":"2","key":"18_CR12","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1002\/j.1538-7305.1950.tb00463.x","volume":"29","author":"RW Hamming","year":"1950","unstructured":"Hamming, R.W.: Error detecting and error correcting codes. Bell Syst. Tech. J. 29(2), 147\u2013160 (1950). https:\/\/doi.org\/10.1002\/j.1538-7305.1950.tb00463.x","journal-title":"Bell Syst. Tech. J."},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Hariharan, G., Jones, P.H., Rozier, K.Y., Wongpiromsarn, T.: Maximum satisfiability of mission-time linear temporal logic. In: Petrucci, L., Sproston, J. (eds.) FORMATS. LNCS, vol. 14138, pp. 86\u2013104. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-42626-1_6","DOI":"10.1007\/978-3-031-42626-1_6"},{"key":"18_CR14","unstructured":"Hofmeier, P., Karayel, E.: Combinatorial enumeration algorithms. Archive of Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/Combinatorial_Enumeration_Algorithms.html, Formal proof development"},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-46982-9_13","volume-title":"Runtime Verification","author":"S Jak\u0161i\u0107","year":"2016","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Ni\u010dkovi\u0107, D.: Quantitative monitoring of STL with edit distance. In: Falcone, Y., S\u00e1nchez, C. (eds.) Runtime Verification, pp. 201\u2013218. Springer, Cham (2016)"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"John, A.K., Shah, S., Chakraborty, S., Trivedi, A., Akshay, S.: Skolem functions for factored formulas. In: 2015 Formal Methods in Computer-Aided Design (FMCAD), pp. 73\u201380. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542255"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Kempa, B., Zhang, P., Jones, P.H., Zambreno, J., Rozier, K.Y.: Embedding online runtime verification for fault disambiguation on robonaut2. In: FORMATS. LNCS, pp. 196\u2013214. Springer, Vienna (2020). http:\/\/research.temporallogic.org\/papers\/KZJZR20.pdf","DOI":"10.1007\/978-3-030-57628-8_12"},{"issue":"4","key":"18_CR18","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1109\/MSP.2017.2695801","volume":"34","author":"S Kolouri","year":"2017","unstructured":"Kolouri, S., Park, S.R., Thorpe, M., Slepcev, D., Rohde, G.K.: Optimal mass transport: signal processing and machine-learning applications. IEEE Signal Process. Mag. 34(4), 43\u201359 (2017). https:\/\/doi.org\/10.1109\/MSP.2017.2695801","journal-title":"IEEE Signal Process. Mag."},{"key":"18_CR19","unstructured":"Kosaian, K., Wang, Z., Sloan, E., Rozier, K.: Formalizing MLTL formula progression in Isabelle\/HOL (2024). https:\/\/arxiv.org\/abs\/2410.03465"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Li, J., Rozier, K.Y.: MLTL benchmark generation via formula progression. In: Runtime Verification, pp. 426\u2013433. Springer, Cham (2018)","DOI":"10.1007\/978-3-030-03769-7_25"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. Inf. Comput. 104923 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104923. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540122000761","DOI":"10.1016\/j.ic.2022.104923"},{"key":"18_CR22","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pp. 152\u2013166. Springer, Heidelberg (2004)"},{"issue":"1","key":"18_CR23","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/s10817-009-9127-8","volume":"43","author":"F Maric","year":"2009","unstructured":"Maric, F.: Formalization and implementation of modern SAT solvers. J. Autom. Reason. 43(1), 81\u2013119 (2009)","journal-title":"J. Autom. Reason."},{"key":"18_CR24","unstructured":"NASA Technology Transfer Program: FRET: Formal Requirements Elicitation Tool (ARC-18066-1) (2024). https:\/\/software.nasa.gov\/software\/ARC-18066-1"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Pan, G., Vardi, M.Y.: Symbolic techniques in satisfiability solving. In: SAT 2005: Satisfiability Research in the Year 2005, pp. 25\u201350. Springer, Cham (2006)","DOI":"10.1007\/978-1-4020-5571-3_3"},{"key":"18_CR26","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":"18_CR27","unstructured":"Rosentrater, A., Rozier, K.Y.: FPROGG: a formula progression-based MLTL benchmark generator. To appear; emailed to authors (2025)"},{"key":"18_CR28","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-031-60698-4_15","volume-title":"NASA Formal Methods","author":"T Schallau","year":"2024","unstructured":"Schallau, T., Naujokat, S., Kullmann, F., Howar, F.: Tree-based scenario classification. In: Benz, N., Gopinath, D., Shi, N. (eds.) NASA Formal Methods, pp. 259\u2013278. Springer, Cham (2024)"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Tabajara, L.M., Vardi, M.Y.: Factored Boolean functional synthesis. In: 2017 Formal Methods in Computer Aided Design (FMCAD), pp. 124\u2013131. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102250"},{"key":"18_CR30","unstructured":"Tabajara, L.M., Vardi, M.Y.: Partitioning techniques in LTLF synthesis. In: 2019 International Joint Conference on Artificial Intelligence (2019)"},{"key":"18_CR31","unstructured":"Wang, Z., Kosaian, K., Rosentrater, A.: Language partitioning for mission-time linear temporal logic. Archive of Formal Proofs (2025). https:\/\/isa-afp.org\/entries\/Mission_Time_LTL_Language_Partition.html, Formal proof development"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Wang, Z., Kosaian, K., Rozier, K.: Formally verifying a transformation from MLTL formulas to regular expressions (2024), accepted to TACAS 2025 (preprint forthcoming)","DOI":"10.1007\/978-3-031-90643-5_13"},{"key":"18_CR33","doi-asserted-by":"publisher","unstructured":"Zhang, P., Aurandt, A.A., Dureja, R., Jones, P.H., Rozier, K.Y.: Model predictive runtime verification for cyber-physical systems with real-time deadlines. In: Petrucci, L., Sproston, J. (eds.) Formal Modeling and Analysis of Timed Systems - 21st International Conference, FORMATS 2023, Antwerp, Belgium, 19\u201321 September 2023, Proceedings. Lecture Notes in Computer Science, vol. 14138, pp. 158\u2013180. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-42626-1_10","DOI":"10.1007\/978-3-031-42626-1_10"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Wang, Z., Kosaian, K., Rozier, K.Y.: Formally verifying a transformation from MLTL formulas to regular expressions. In: Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS. Springer, Cham (2025)","DOI":"10.1007\/978-3-031-90643-5_13"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-93706-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:23:07Z","timestamp":1749316987000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hampton Roads, VA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}