{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:48:21Z","timestamp":1776509301585,"version":"3.51.2"},"publisher-location":"Cham","reference-count":73,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_21","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:42:26Z","timestamp":1759844546000},"page":"371-391","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing MLTL Formula Progression in Isabelle\/HOL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9336-6006","authenticated-orcid":false,"given":"Katherine","family":"Kosaian","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6180","authenticated-orcid":false,"given":"Zili","family":"Wang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0496-9241","authenticated-orcid":false,"given":"Elizabeth","family":"Sloan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"2018 Runtime Verification Benchmark Competition. https:\/\/www.rv-competition.org\/2018-2\/"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. In: LICS. pp. 390\u2013401. IEEE (1990)","DOI":"10.1109\/LICS.1990.113764"},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. In: Logrippo, L. (ed.) PODC. pp. 139\u2013152. ACM (1991). https:\/\/doi.org\/10.1145\/112600.112613, https:\/\/doi.org\/10.1145\/112600.112613","DOI":"10.1145\/112600.112613"},{"key":"21_CR4","unstructured":"Amjad, R., van Glabbeek, R., O\u2019Connor, L.: Definitive set semantics for LTL3. Archive of Formal Proofs (August 2024), https:\/\/isa-afp.org\/entries\/LTL3_Semantics.html, Formal proof development"},{"key":"21_CR5","unstructured":"Anastasia Mavridou: Capturing and analyzing requirements with FRET. Presentation, NFM, https:\/\/github.com\/NASA-SW-VnV\/fret, NASA, Pasadena, California, USA (May 2022)"},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Aurandt, A., Jones, P., Rozier, K.Y.: Runtime verification triggers real-time, autonomous fault recovery on the CySat-I. In: NFM. LNCS, vol. 13260. Springer, Cham, Caltech, California, USA (May 2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_45","DOI":"10.1007\/978-3-031-06773-0_45"},{"key":"21_CR7","unstructured":"Bacchus, F., Kabanza, F.: Planning for temporally extended goals. In: Clancey, W.J., Weld, D.S. (eds.) AAAI. pp. 1215\u20131222. AAAI Press \/ The MIT Press (1996), http:\/\/www.aaai.org\/Library\/AAAI\/1996\/aaai96-180.php"},{"key":"21_CR8","doi-asserted-by":"publisher","unstructured":"Basin, D.A., Dardinier, T., Hauser, N., Heimes, L., y\u00a0Munive, J.J.H., Kaletsch, N., Krstic, S., Marsicano, E., Raszyk, M., Schneider, J., Tirore, D.L., Traytel, D., Zingg, S.: VeriMon: A formally verified monitoring tool. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) ICTAC. LNCS, vol. 13572, pp.\u00a01\u20136. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_1, https:\/\/doi.org\/10.1007\/978-3-031-17715-6_1","DOI":"10.1007\/978-3-031-17715-6_1"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Cauwels, M., Hammer, A., Hertz, B., Jones, P., Rozier, K.Y.: Integrating runtime verification into an automated UAS traffic management system. In: Proceedings of DETECT: international workshop on moDeling, vErification and Testing of dEpendable CriTical systems. CCIS, Springer, L\u2019Aquila, Italy (September 2020). https:\/\/doi.org\/10.1007\/978-3-030-59155-7_26","DOI":"10.1007\/978-3-030-59155-7_26"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Chattopadhyay, A., Mamouras, K.: A verified online monitor for metric temporal logic with quantitative semantics. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV. pp. 383\u2013403. Springer International Publishing, Cham (2020)","DOI":"10.1007\/978-3-030-60508-7_21"},{"key":"21_CR11","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. pp. 68\u201381. ACM (2022). https:\/\/doi.org\/10.1145\/3497775.3503685, https:\/\/doi.org\/10.1145\/3497775.3503685","DOI":"10.1145\/3497775.3503685"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Coupet-Grimal, S.: An axiomatization of linear temporal logic in the calculus of inductive constructions. J. Log. Comput. 13(6), 801\u2013813 (2003). https:\/\/doi.org\/10.1093\/LOGCOM\/13.6.801, https:\/\/doi.org\/10.1093\/logcom\/13.6.801","DOI":"10.1093\/LOGCOM\/13.6.801"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Dabney, J.B., Badger, J.M., Rajagopal, P.: Adding a verification view for an autonomous real-time system architecture. In: Proceedings of SciTech Forum. p. Online. 2021-0566, AIAA (January 2021). https:\/\/doi.org\/10.2514\/6.2021-0566","DOI":"10.2514\/6.2021-0566"},{"key":"21_CR14","unstructured":"Dabney, J.B.: Using assume-guarantee contracts in autonomous spacecraft. Flight Software Workshop (FSW) Online: https:\/\/www.youtube.com\/watch?v=zrtyiyNf674 (February 2021)"},{"key":"21_CR15","unstructured":"Dabney, J.B., Rajagopal, P., Badger, J.M.: Using assume-guarantee contracts for developmental verification of autonomous spacecraft. Flight Software Workshop (FSW) Online: https:\/\/www.youtube.com\/watch?v=HFnn6TzblPg (February 2022)"},{"key":"21_CR16","doi-asserted-by":"publisher","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.) iFM. LNCS, vol. 14300, pp. 279\u2013301. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_15, https:\/\/doi.org\/10.1007\/978-3-031-47705-8_15","DOI":"10.1007\/978-3-031-47705-8_15"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A fully verified executable LTL model checker. Archive of Formal Proofs (May 2014), https:\/\/isa-afp.org\/entries\/CAVA_LTL_Modelchecker.html, Formal proof development","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"21_CR18","doi-asserted-by":"crossref","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: RV. vol.\u00a08734, pp. 215\u2013230. Springer-Verlag (September 2014)","DOI":"10.1007\/978-3-319-11164-3_18"},{"key":"21_CR19","unstructured":"Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) IJCAI. pp. 854\u2013860. IJCAI\/AAAI (2013), http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6997"},{"key":"21_CR20","unstructured":"Giannakopoulou, D., Mavridou, A., Rhein, J., Pressburger, T., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020). No. ARC-E-DAA-TN77785 (2020)"},{"key":"21_CR21","unstructured":"Haftmann, F.: Code generation from Isabelle\/HOL theories. https:\/\/isabelle.in.tum.de\/doc\/codegen.pdf (2024), tutorial, with contributions from Lukas Bulwahn and Tobias Nipkow"},{"key":"21_CR22","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 (2023). https:\/\/doi.org\/10.1007\/978-3-031-42626-1_6, https:\/\/doi.org\/10.1007\/978-3-031-42626-1_6","DOI":"10.1007\/978-3-031-42626-1_6"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Hertz, B., Luppen, Z., Rozier, K.Y.: Integrating runtime verification into a sounding rocket control system. In: NFM (May 2021), available online at http:\/\/temporallogic.org\/research\/NFM21\/","DOI":"10.1007\/978-3-030-76384-8_10"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Johannsen, C., Jones, P., Kempa, B., Rozier, K.Y., Zhang, P.: R2U2 version 3.0: Re-imagining a toolchain for specification, resource estimation, and optimized observer generation for runtime verification in hardware and software. In: Enea, C., Lal, A. (eds.) CAV. pp. 483\u2013497. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-37709-9_23"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Johannsen, C., Anderson, M., Burken, W., Diersen, E., Edgren, J., Glick, C., Jou, S., Kumar, A., Levandowski, J., Moyer, E., Roquet, T., VandeLoo, A., Rozier, K.Y.: OpenUAS Version 1.0. IEEE, Athens, Greece (Virtual) (June 2021)","DOI":"10.1109\/ICUAS51884.2021.9476814"},{"key":"21_CR26","doi-asserted-by":"publisher","unstructured":"Kamide, N.: Bounded linear-time temporal logic: A proof-theoretic investigation. Ann. Pure Appl. Log. 163(4), 439\u2013466 (2012). https:\/\/doi.org\/10.1016\/J.APAL.2011.12.002, https:\/\/doi.org\/10.1016\/j.apal.2011.12.002","DOI":"10.1016\/J.APAL.2011.12.002"},{"key":"21_CR27","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. pp. 196\u2013214. LNCS, Springer, Vienna, Austria (September 2020), http:\/\/research.temporallogic.org\/papers\/KZJZR20.pdf","DOI":"10.1007\/978-3-030-57628-8_12"},{"key":"21_CR28","unstructured":"Kessler, F.B.: nuXmv 1.1.0 (2016-05-10) Release Notes. https:\/\/es-static.fbk.eu\/tools\/nuxmv\/downloads\/NEWS.txt (2016)"},{"key":"21_CR29","unstructured":"Kosaian, K., Wang, Z., Sloan, E.: Mission-time Linear Temporal Logic. Archive of Formal Proofs (January 2025), https:\/\/isa-afp.org\/entries\/Mission_Time_LTL.html, Formal proof development"},{"key":"21_CR30","unstructured":"Kosaian, K., Wang, Z., Sloan, E.: Mission-time Linear Temporal Logic formula progression. Archive of Formal Proofs (July 2025), https:\/\/isa-afp.org\/entries\/Mission_Time_LTL_Formula_Progression.html, Formal proof development"},{"key":"21_CR31","doi-asserted-by":"publisher","unstructured":"de\u00a0Leng, D., Heintz, F.: Approximate stream reasoning with metric temporal logic under uncertainty. In: AAAI. pp. 2760\u20132767. AAAI Press (2019). https:\/\/doi.org\/10.1609\/AAAI.V33I01.33012760, https:\/\/doi.org\/10.1609\/aaai.v33i01.33012760","DOI":"10.1609\/AAAI.V33I01.33012760"},{"key":"21_CR32","doi-asserted-by":"publisher","unstructured":"Li, J., Rozier, K.Y.: MLTL benchmark generation via formula progression. In: Colombo, C., Leucker, M. (eds.) RV. LNCS, vol. 11237, pp. 426\u2013433. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_25, https:\/\/doi.org\/10.1007\/978-3-030-03769-7_25","DOI":"10.1007\/978-3-030-03769-7_25"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for Mission-time LTL. In: CAV. LNCS, Springer, New York, NY, USA (July 2019)","DOI":"10.1007\/978-3-030-25543-5_1"},{"key":"21_CR34","unstructured":"Lowry, M., Bajwa, A.: Autonomy Operating System (AOS) for UAVs. Proposal Presentation, NASA Ames Research Center, Moffett Field, California (June 2015)"},{"key":"21_CR35","unstructured":"Lowry, M., Bajwa, A., Quach, P., Karsai, G., Rozier, K.Y., Rayadurgam, S.: Autonomy Operating System for UAVs. Online: https:\/\/nari.arc.nasa.gov\/sites\/default\/files\/attachments\/15%29%20Mike%20Lowry%20SAEApril19-2017.Final_.pdf (April 2017)"},{"key":"21_CR36","doi-asserted-by":"publisher","unstructured":"Luppen, Z., Jacks, M., Baughman, N., Hertz, B., Cutler, J., Lee, D.Y., Rozier, K.Y.: Elucidation and analysis of specification patterns in aerospace system telemetry. In: NFM. LNCS, vol. 13260. Springer, Cham, Caltech, California, USA (May 2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_28","DOI":"10.1007\/978-3-031-06773-0_28"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"Luppen, Z.A., Lee, D.Y., Rozier, K.Y.: A case study in formal specification and runtime verification of a CubeSat communications system. In: SciTech. AIAA, Nashville, TN, USA (January 2021)","DOI":"10.2514\/6.2021-0997"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pp. 152\u2013166. Springer (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"21_CR39","unstructured":"NASA: PVS library: LTL module. https:\/\/github.com\/nasa\/pvslib\/tree\/master\/LTL (nd)"},{"key":"21_CR40","unstructured":"NASA Technology Transfer Program: FRET : Formal Requirements Elicitation Tool (ARC-18066-1). Online: https:\/\/software.nasa.gov\/software\/ARC-18066-1 (2024)"},{"key":"21_CR41","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, LNCS, vol.\u00a02283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"21_CR42","doi-asserted-by":"publisher","unstructured":"Niu, T., Xu, Y., Xiao, S., Xiao, L., Huang, Y., Li, J.: $$\\text{LTL}_f$$ satisfiability checking via formula progression. In: Chang, S. (ed.) SEKE. pp. 357\u2013362. KSI Research Inc. (2023). https:\/\/doi.org\/10.18293\/SEKE2023-143, https:\/\/doi.org\/10.18293\/SEKE2023-143","DOI":"10.18293\/SEKE2023-143"},{"key":"21_CR43","unstructured":"Okubo, N.: Using R2U2 in JAXA program. Electronic correspondence (November\u2013December 2020), correspondance"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) Formal Modeling and Analysis of Timed Systems. pp. 1\u201313. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-85778-5_1"},{"key":"21_CR45","doi-asserted-by":"publisher","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363\u2013397 (1989). https:\/\/doi.org\/10.1007\/BF00248324","DOI":"10.1007\/BF00248324"},{"key":"21_CR46","doi-asserted-by":"publisher","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL. EPiC Series in Computing, vol.\u00a02, pp. 1\u201311. EasyChair (2010). https:\/\/doi.org\/10.29007\/36DT","DOI":"10.29007\/36DT"},{"key":"21_CR47","unstructured":"Perez, I.: Runtime verification with Ogma. In: Invited Talk to University of California (2023)"},{"key":"21_CR48","unstructured":"Perez, I., Goodloe, A.: Ogma. https:\/\/github.com\/nasa\/ogma (2021)"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"Perez, I., Mavridou, A., Pressburger, T., Goodloe, A., Giannakopoulou, D.: Automated translation of natural language requirements to runtime monitors. In: Fisman, D., Rosu, G. (eds.) TACAS. pp. 387\u2013395. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-99524-9_21"},{"key":"21_CR50","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, Proc. 18th IEEE Symp. pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"21_CR51","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Arons, T.: TLPVS: A PVS-based LTL verification system. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. LNCS, vol.\u00a02772, pp. 598\u2013625. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-39910-0_26, https:\/\/doi.org\/10.1007\/978-3-540-39910-0_26","DOI":"10.1007\/978-3-540-39910-0_26"},{"key":"21_CR52","doi-asserted-by":"publisher","unstructured":"Raszyk, M., Basin, D.A., Traytel, D.: Multi-head monitoring of metric dynamic logic. In: Hung, D.V., Sokolsky, O. (eds.) ATVA. LNCS, vol. 12302, pp. 233\u2013250. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_13, https:\/\/doi.org\/10.1007\/978-3-030-59152-6_13","DOI":"10.1007\/978-3-030-59152-6_13"},{"key":"21_CR53","doi-asserted-by":"crossref","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: TACAS. LNCS, vol.\u00a08413, pp. 357\u2013372. Springer-Verlag (April 2014)","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"21_CR54","doi-asserted-by":"publisher","unstructured":"Roohi, N., Viswanathan, M.: Revisiting MITL to fix decision procedures. In: Dillig, I., Palsberg, J. (eds.) VMCAI. LNCS, vol. 10747, pp. 474\u2013494. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_22, https:\/\/doi.org\/10.1007\/978-3-319-73721-8_22","DOI":"10.1007\/978-3-319-73721-8_22"},{"key":"21_CR55","unstructured":"Rosentrater, A., Rozier, K.Y.: FPROGG: A formula progression-based MLTL benchmark generator. To appear (2025)"},{"key":"21_CR56","doi-asserted-by":"publisher","unstructured":"Rosentrater, A., Wang, Z., Kosaian, K., Rozier, K.Y.: Language partitioning for Mission-Time Linear Temporal Logic. In: Dutle, A., Humphrey, L.R., Titolo, L. (eds.) NFM. LNCS, vol. 15682, pp. 313\u2013332. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-93706-4_18, https:\/\/doi.org\/10.1007\/978-3-031-93706-4_18","DOI":"10.1007\/978-3-031-93706-4_18"},{"key":"21_CR57","unstructured":"Rozier, K.Y.: R2U2 in space: System and software health management for small satellites. In: Spacecraft Flight Software Workshop (FSW) (December 2016), https:\/\/www.youtube.com\/watch?v=OAgQFuEGSi8, https:\/\/www.youtube.com\/watch?v=OAgQFuEGSi8"},{"key":"21_CR58","unstructured":"Rozier, K.Y., Schumann, J., Ippolito, C.: Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS. Technical Memorandum NASA\/TM-2015-218817, NASA, NASA Ames Research Center, Moffett Field, CA 94035, USA (May 2015)"},{"key":"21_CR59","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y.: Linear temporal logic Symbolic Model Checking. Computer Science Review Journal 5(2), 163\u2013203 (May 2011). https:\/\/doi.org\/10.1016\/j.cosrev.2010.06.002, http:\/\/dx.doi.org\/10.1016\/j.cosrev.2010.06.002","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"21_CR60","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y.: On the evaluation and comparison of runtime verification tools for hardware and cyber-physical systems. In: RV-CUBES. vol.\u00a03, pp. 123\u2013137. Kalpa Publications, Seattle, WA, USA (September 2017). https:\/\/doi.org\/10.29007\/pld3, https:\/\/easychair.org\/publications\/paper\/877G","DOI":"10.29007\/pld3"},{"key":"21_CR61","unstructured":"Rozier, K.Y., Schumann, J.: R2U2: Tool Overview. In: RV-CUBES. vol.\u00a03, pp. 138\u2013156. Kalpa Publications, Seattle, WA, USA (September 2017), https:\/\/easychair.org\/publications\/paper\/Vncw"},{"key":"21_CR62","unstructured":"Schimpf, A., Lammich, P.: Converting linear-time temporal logic to generalized B\u00fcchi automata. Archive of Formal Proofs (May 2014), https:\/\/isa-afp.org\/entries\/LTL_to_GBA.html, Formal proof development"},{"key":"21_CR63","doi-asserted-by":"crossref","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime analysis with R2U2: A tool exhibition report. In: RV. Springer-Verlag, Madrid, Spain (September 2016)","DOI":"10.1007\/978-3-319-46982-9_35"},{"key":"21_CR64","doi-asserted-by":"crossref","unstructured":"Schumann, J., Rozier, K.Y., Reinbacher, T., Mengshoel, O.J., Mbaya, T., Ippolito, C.: Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. IJPHM 6(1), 1\u201327 (June 2015)","DOI":"10.36001\/ijphm.2015.v6i1.2243"},{"key":"21_CR65","unstructured":"Seidl, B., Sickert, S.: A compositional and unified translation of LTL into $$\\omega $$-automata. Archive of Formal Proofs (April 2019), https:\/\/isa-afp.org\/entries\/LTL_Master_Theorem.html, Formal proof development"},{"key":"21_CR66","unstructured":"Sickert, S.: Converting linear temporal logic to deterministic (generalized) Rabin automata. Archive of Formal Proofs (September 2015), https:\/\/isa-afp.org\/entries\/LTL_to_DRA.html, Formal proof development"},{"key":"21_CR67","unstructured":"Sickert, S.: Linear temporal logic. Archive of Formal Proofs (March 2016), https:\/\/isa-afp.org\/entries\/LTL.html, Formal proof development"},{"key":"21_CR68","doi-asserted-by":"crossref","unstructured":"Sickert, S.: An efficient normalisation procedure for linear temporal logic: Isabelle\/HOL formalisation. Archive of Formal Proofs (May 2020), https:\/\/isa-afp.org\/entries\/LTL_Normal_Form.html, Formal proof development","DOI":"10.1145\/3373718.3394743"},{"key":"21_CR69","unstructured":"Titolo, L., Conrad, E., Giannakopoulou, D., Pressburger, T., Dutle, A.: FRET Proof Framework. https:\/\/lauratitolo.github.io\/project\/fret-proof-framework\/ (2022)"},{"key":"21_CR70","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: From Church and Prior to PSL. In: 25 Years of Model Checking: History, Achievements, Perspectives, pp. 150\u2013171. Springer (2008)","DOI":"10.1007\/978-3-540-69850-0_10"},{"key":"21_CR71","unstructured":"Wang, Z., Gamboa-Guzman, L.P., Rozier, K.Y.: WEST: Interactive validation of Mission-time Linear Temporal Logic (MLTL) (2024), https:\/\/temporallogic.org\/research\/WEST\/"},{"key":"21_CR72","doi-asserted-by":"crossref","unstructured":"Wang, Z., Kosaian, K., Rozier, K.: Formally verifying a transformation from MLTL formulas to regular expressions, accepted to TACAS 2025, preprint available at: https:\/\/arxiv.org\/abs\/2501.17444","DOI":"10.1007\/978-3-031-90643-5_13"},{"key":"21_CR73","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.) FORMATS. LNCS, vol. 14138, pp. 158\u2013180. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-42626-1_10, https:\/\/doi.org\/10.1007\/978-3-031-42626-1_10","DOI":"10.1007\/978-3-031-42626-1_10"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07021-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:21:56Z","timestamp":1776507716000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032070203","9783032070210"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","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":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}