{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T02:33:56Z","timestamp":1773369236618,"version":"3.50.1"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>Modern cyber-physical systems-of-systems (CPSoS) operate in complex systems-of-systems that must seamlessly work together to control safety- or mission-critical functions. Linear Temporal Logic (LTL) and Mission-time Linear Temporal logic (MLTL) intuitively express CPSoS requirements for automated system verification and validation. However, both LTL and MLTL presume that all signals populating the variables in a formula are sampled over the same rate and type (e.g., time or distance), and agree on a standard \u201ctime\u201d step. Formal verification of CPSoS needs validate-able requirements expressed over (sub-)system signals of different types, such as signals sampled at different timescales, distances, or levels of abstraction, expressed in the same formula. Previous works developed more expressive logics to account for types (e.g., timescales) by sacrificing the intuitive simplicity of LTL. However, a legible direct one-to-one correspondence between a verbal and formal specification will ease validation, reduce bugs, increase productivity, and linearize the workflow from a project\u2019s conception to actualization. Validation includes both transparency for human interpretation, and tractability for automated reasoning, as CPSoS often run on resource-limited embedded systems. To address these challenges, we introduced Mission-time Linear Temporal Logic Multi-type (Hariharan et\u00a0al., Numerical Software Verification Workshop, 2022), a logic building on MLTL. MLTLM enables writing formal requirements over finite input signals (e.g., sensor signals and local computations) of different types, while maintaining the same simplicity as LTL and MLTL. Furthermore, MLTLM maintains a direct correspondence between a verbal requirement and its corresponding formal specification. Additionally, reasoning a formal specification in the intended type (e.g., hourly for an hourly rate, and per second for a seconds rate) will use significantly less memory in resource-constrained hardware. This article extends the previous work with (1) many illustrated examples on types (e.g., time and space) expressed in the same specification, (2) proofs omitted for space in the workshop version, (3) proofs of succinctness of MLTLM compared to MLTL, and (4) a minimal translation to MLTL of optimal length.<\/jats:p>","DOI":"10.1145\/3704809","type":"journal-article","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T05:53:27Z","timestamp":1732514007000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["MLTL Multi-type: A Typed Logic for Cyber-Physical Systems"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3447-2183","authenticated-orcid":false,"given":"Gokul","family":"Hariharan","sequence":"first","affiliation":[{"name":"Iowa State University","place":["Ames, United States"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2239-4218","authenticated-orcid":false,"given":"Brian","family":"Kempa","sequence":"additional","affiliation":[{"name":"Iowa State University","place":["Ames, United States"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3977-122X","authenticated-orcid":false,"given":"Tichakorn","family":"Wongpiromsarn","sequence":"additional","affiliation":[{"name":"Iowa State University","place":["Ames, United States"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8220-7552","authenticated-orcid":false,"given":"Phillip","family":"Jones","sequence":"additional","affiliation":[{"name":"Electrical and Computer Engineering, Iowa State University","place":["Ames, United States"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin","family":"Rozier","sequence":"additional","affiliation":[{"name":"Iowa State University","place":["Ames, United States"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,3,2]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/772062.772064"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/1625135.1625236"},{"key":"e_1_3_2_4_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_2_5_2","first-page":"695","volume-title":"Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908)","author":"Balbiani Philippe","year":"2008","unstructured":"Philippe Balbiani. 2008. Time representation and temporal reasoning from the perspective of non-standard analysis. In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908). AAAI Press, 695\u2013704."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.201700036"},{"key":"e_1_3_2_7_2","doi-asserted-by":"crossref","unstructured":"Omar Bataineh David S. Rosenblum and Mark Reynolds. 2019. Efficient decentralized LTL monitoring framework using tableau technique. ACM Transactions on Embedded Computing Systems (TECS) 18 5s Article 87 (2019) 21 pages.","DOI":"10.1145\/3358219"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_10"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44798-9_10"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/VLHCC.2011.6070385"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.2.195"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_2_14_2","unstructured":"James Clifford and Ahobala Rao. 1986. A simple general structure for temporal domains. NYU: IOMS: Information Systems Working Papers (Topic) (1986). https:\/\/api.semanticscholar.org\/CorpusID:7012945"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/2832581.2832650"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/FDL.2018.8524052"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.2514\/6.2021-0566"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/SCC57168.2023.00018"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_23"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40787-1_27"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"J\u00e9r\u00f4me Euzenat and Angelo Montanari. 2005. Chapter 3 - time granularity. In Foundations of Artificial Intelligence M. Fisher D. Gabbay and L. Vila (Eds.). Vol. 1. Elsevier 59\u2013118. 10.1016\/S1574-6526(05)80005-7","DOI":"10.1016\/S1574-6526(05)80005-7"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.06.004"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_18"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21222-2_11"},{"key":"e_1_3_2_26_2","volume-title":"Descriptive Complexity","author":"Immerman Neil","year":"2012","unstructured":"Neil Immerman. 2012. Descriptive Complexity. Springer Science & Business Media."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_23"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-57628-8_12"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.014"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2007.56"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_1"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_28"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2015.95"},{"key":"e_1_3_2_34_2","unstructured":"Naoko Okubo. 2020. Using R2U2 in JAXA program. Electronic correspondence. 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 200KB."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_1"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0140-3"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"e_1_3_2_39_2","first-page":"138","volume-title":"Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES)","volume":"3","author":"Rozier Kristin Yvonne","year":"2017","unstructured":"Kristin Yvonne Rozier and Johann Schumann. 2017. R2U2: Tool overview. In Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES). Vol. 3, Kalpa Publications, Seattle, WA, USA, 138\u2013156."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46982-9_35"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_1"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704809","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T15:04:00Z","timestamp":1773327840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,2]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3704809"],"URL":"https:\/\/doi.org\/10.1145\/3704809","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,2]]},"assertion":[{"value":"2023-12-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-02","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}