{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T00:44:49Z","timestamp":1780620289978,"version":"3.54.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","funder":[{"name":"National Science Foundation","award":["CAREER award (SHF-2048094), CNS-1932620, CNS-2039087, FMitF-1837131, CCF-SHF-1932620, IIS-SLES-2417075"],"award-info":[{"award-number":["CAREER award (SHF-2048094), CNS-1932620, CNS-2039087, FMitF-1837131, CCF-SHF-1932620, IIS-SLES-2417075"]}]},{"name":"Toyota R&D and Siemens Corporate Research through the USC Center for Autonomy and AI, an Amazon Faculty Research Award"},{"name":"Airbus Institute for Engineering Research"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,11,30]]},"abstract":"<jats:p>\n            Multi-agent systems (MASs) consisting of a number of autonomous agents that communicate, coordinate, and jointly sense the environment to achieve complex missions can be found in a variety of applications such as robotics, smart cities, and internet-of-things applications. Modeling and monitoring MAS requirements to guarantee overall mission objectives, safety, and reliability is an important problem. Such requirements implicitly require reasoning about diverse sensing and communication modalities between agents, analysis of the dependencies between agent tasks, and the spatial or virtual distance between agents. To capture such rich MAS requirements, we model agent interactions via multiple directed graphs, and introduce a new logic \u2013\n            <jats:italic toggle=\"yes\">Spatio-Temporal Logic with Graph Operators<\/jats:italic>\n            (STL-GO). The key innovation in STL-GO are graph operators that enable us to reason about the number of agents along either the incoming or outgoing edges of the underlying interaction graph that satisfy a given property of interest; for example, the requirement that an agent should sense at least two neighboring agents whose task graphs indicate the ability to collaborate. We then propose novel distributed monitoring conditions for individual agents that use only local information to determine whether or not an STL-GO specification is satisfied. We compare the expressivity of STL-GO against existing spatio-temporal logic formalisms, and demonstrate the utility of STL-GO and our distributed monitors in a bike-sharing and a multi-drone case study.\n          <\/jats:p>","DOI":"10.1145\/3760258","type":"journal-article","created":{"date-parts":[[2025,8,11]],"date-time":"2025-08-11T11:26:22Z","timestamp":1754911582000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["STL-GO: Spatio-Temporal Logic with Graph Operators for Distributed Systems with Multiple Network Topologies"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-4283-6358","authenticated-orcid":false,"given":"Yiqi","family":"Zhao","sequence":"first","affiliation":[{"name":"Computer Science, University of Southern California","place":["Los Angeles, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3161-7043","authenticated-orcid":false,"given":"Xinyi","family":"Yu","sequence":"additional","affiliation":[{"name":"Computer Science, University of Southern California","place":["Los Angeles, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6255-7566","authenticated-orcid":false,"given":"Bardh","family":"Hoxha","sequence":"additional","affiliation":[{"name":"Toyota Research Institute North America","place":["Ann Arbor, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0456-2129","authenticated-orcid":false,"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[{"name":"Toyota Research Institute North America","place":["Ann Arbor, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4683-5540","authenticated-orcid":false,"given":"Jyotirmoy","family":"Deshmukh","sequence":"additional","affiliation":[{"name":"Computer Science, University of Southern California","place":["Los Angeles, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3430-6625","authenticated-orcid":false,"given":"Lars","family":"Lindemann","sequence":"additional","affiliation":[{"name":"Computer Science, University of Southern California","place":["Los Angeles, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,9,26]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"2024. Retrieved November 14th 2024 from https:\/\/citibikenyc.com\/system-data. (2024)."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TRA.2002.806024"},{"key":"e_1_3_3_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_3_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3127050"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50763-7"},{"key":"e_1_3_3_8_2","unstructured":"Raven Beutner and Bernd Finkbeiner. 2021. A temporal logic for strategic hyperproperties. 32nd International Conference on Concurrency Theory (CONCUR 2021)."},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1515\/9781400831470"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1049\/ip-sen:19971023"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0286-7"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2174666"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2656045.2656054"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_19"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_3"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.3390\/a15040126"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2013.02.003"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:SYNT.0000024915.66183.d1"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2016.7487733"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728633"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2024.3410150"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9413-9"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2022.3143304"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/15136.001.0001"},{"key":"e_1_3_3_27_2","first-page":"142","volume-title":"Proceedings of the ACM\/IEEE 14th International Conference on Cyber-Physical Systems","author":"Lindemann Lars","year":"2023","unstructured":"Lars Lindemann, Xin Qin, Jyotirmoy V. Deshmukh, and George J. Pappas. 2023. Conformal prediction for stl runtime verification. In Proceedings of the ACM\/IEEE 14th International Conference on Cyber-Physical Systems. 142\u2013153."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS48487.2020.00013"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477032"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2020.109469"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198537878.001.0001"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71493-4_33"},{"key":"e_1_3_3_34_2","doi-asserted-by":"crossref","unstructured":"Mehran Mesbahi and Magnus Egerstedt. 2010. Graph theoretic methods in multiagent networks. Princeton University Press.","DOI":"10.1515\/9781400835355"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3576841.3585937"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-023-00718-x"},{"key":"e_1_3_3_37_2","article-title":"A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems","volume":"18","author":"Nenzi Laura","year":"2022","unstructured":"Laura Nenzi, Ezio Bartocci, Luca Bortolussi, and Michele Loreti. 2022. A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems. Logical Methods in Computer Science 18, 1 (2022), 1\u20134.","journal-title":"Logical Methods in Computer Science"},{"issue":"4","key":"e_1_3_3_38_2","article-title":"Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic","volume":"1","author":"Nenzi Laura","year":"2015","unstructured":"Laura Nenzi and Luca Bortolussi. 2015. Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. EAI Endorsed Transactions on Cloud Systems 1, 4 (2015), 66\u201373.","journal-title":"EAI Endorsed Transactions on Cloud Systems"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23820-3_2"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883831"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3313353"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRERA.2013.6749783"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.017"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10514-008-9107-6"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65633-0_15"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2016.2611536"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC40024.2019.9029181"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.5772\/57313"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_4"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2022.3197693"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS61052.2024.00022"},{"key":"e_1_3_3_52_2","doi-asserted-by":"crossref","unstructured":"Yiqi Zhao Emily Zhu Bardh Hoxha Georgios Fainekos Jyotirmoy V. Deshmukh and Lars Lindemann. 2025. Distributionally robust predictive runtime verification under spatio-temporal logic specifications. ACM Transactions on Cyber-Physical Systems.","DOI":"10.1145\/3748818"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3760258","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T17:12:48Z","timestamp":1759338768000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3760258"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,26]]},"references-count":51,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2025,11,30]]}},"alternative-id":["10.1145\/3760258"],"URL":"https:\/\/doi.org\/10.1145\/3760258","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,26]]},"assertion":[{"value":"2025-07-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}