{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T09:37:11Z","timestamp":1766050631418,"version":"build-2065373602"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T00:00:00Z","timestamp":1718323200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T00:00:00Z","timestamp":1718323200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["2102106"],"award-info":[{"award-number":["2102106"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1007\/s10703-024-00450-5","type":"journal-article","created":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T08:02:12Z","timestamp":1718352132000},"page":"146-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Runtime verification of partially-synchronous distributed system"],"prefix":"10.1007","volume":"64","author":[{"given":"Ritam","family":"Ganguly","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anik","family":"Momtaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1800-5419","authenticated-orcid":false,"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,14]]},"reference":[{"issue":"3","key":"450_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2491245","volume":"31","author":"JC Corbett","year":"2013","unstructured":"Corbett JC, Dean J, Epstein M, Fikes A, Frost C, Furman JJ, Ghemawat S, Gubarev A, Heiser C, Hochschild P, Hsieh W, Kanthak S, Kogan E, Li H, Lloyd A, Melnik S, Mwaura D, Nagle D, Quinlan S, Rao R, Rolig L, Saito Y, Szymaniak M, Taylor C, Wang R, Woodford D (2013) Spanner: Google\u2019s globally distributed database. ACM Trans. Comput. Syst. 31(3):1\u201322. https:\/\/doi.org\/10.1145\/2491245","journal-title":"ACM Trans. Comput. Syst."},{"issue":"1\u20132","key":"450_CR2","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/s10703-016-0253-8","volume":"48","author":"A Bauer","year":"2016","unstructured":"Bauer A, Falcone Y (2016) Decentralised LTL monitoring. Form Methods Syst Design 48(1\u20132):46\u201393","journal-title":"Form Methods Syst Design"},{"key":"450_CR3","doi-asserted-by":"crossref","unstructured":"Ogale VA, Garg VK (2007) Detecting temporal logic predicates on distributed computations. In: Proceedings of the 21st international symposium on distributed computing (DISC), pp 420\u2013434","DOI":"10.1007\/978-3-540-75142-7_32"},{"key":"450_CR4","doi-asserted-by":"crossref","unstructured":"Mostafa M, Bonakdarpour B (2015) Decentralized runtime verification of LTL specifications in distributed systems. In: Proceedings of the 29th IEEE international parallel and distributed processing symposium (IPDPS), pp 494\u2013503","DOI":"10.1109\/IPDPS.2015.95"},{"key":"450_CR5","doi-asserted-by":"crossref","unstructured":"Mills D (2010) Network time protocol version 4: protocol and algorithms specification. RFC 5905, RFC Editor","DOI":"10.17487\/rfc5905"},{"issue":"4","key":"450_CR6","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol (TOSEM) 20(4):14\u201311464","journal-title":"ACM Trans Softw Eng Methodol (TOSEM)"},{"key":"450_CR7","doi-asserted-by":"crossref","unstructured":"Havelund K, Rosu G (2001) Monitoring programs using rewriting. In: Automated software engineering (ASE), pp 135\u2013143","DOI":"10.1109\/ASE.2001.989799"},{"key":"450_CR8","unstructured":"Ganguly R, Momtaz A, Bonakdarpour B (2020) Distributed runtime verification under partial asynchrony. In: Proceedings of the 24nd international conference on principles of distributed systems (OPODIS), pp 20\u201312017"},{"key":"450_CR9","doi-asserted-by":"publisher","unstructured":"Mehlitz P, Giannakopoulou D, Shafiei N (2019) Analyzing airspace data with race. In: 2019 IEEE\/AIAA 38th digital avionics systems conference (DASC), pp 1\u201310. https:\/\/doi.org\/10.1109\/DASC43569.2019.9081664","DOI":"10.1109\/DASC43569.2019.9081664"},{"key":"450_CR10","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Symposium on foundations of computer science (FOCS), pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"450_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin"},{"issue":"7","key":"450_CR12","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport L (1978) Time, clocks, and the ordering of events in a distributed system. Commun ACM 21(7):558\u2013565","journal-title":"Commun ACM"},{"key":"450_CR13","doi-asserted-by":"crossref","unstructured":"Kulkarni SS, Demirbas M, Madappa D, Avva B, Leone M (2014) Logical physical clocks. In: Proceedings of the 18th international conference on principles of distributed systems, pp 17\u201332","DOI":"10.1007\/978-3-319-14472-6_2"},{"issue":"3","key":"450_CR14","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer A, Leucker M, Schallhart C (2010) Comparing LTL semantics for runtime verification. J Log Comput 20(3):651\u2013674. https:\/\/doi.org\/10.1093\/logcom\/exn075","journal-title":"J Log Comput"},{"key":"450_CR15","volume-title":"Elements of distributed computing","author":"VK Garg","year":"2002","unstructured":"Garg VK (2002) Elements of distributed computing. Wiley, USA"},{"key":"450_CR16","doi-asserted-by":"crossref","unstructured":"de Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems (TACAS), pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"450_CR17","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1145\/1773912.1773922","volume":"44","author":"A Lakshman","year":"2010","unstructured":"Lakshman A, Malik P (2010) Cassandra: a decentralized structured storage system. SIGOPS Oper Syst Rev 44(2):35\u201340. https:\/\/doi.org\/10.1145\/1773912.1773922","journal-title":"SIGOPS Oper Syst Rev"},{"issue":"1","key":"450_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3355181","volume":"29","author":"A El-Hokayem","year":"2020","unstructured":"El-Hokayem A, Falcone Y (2020) On the monitoring of decentralized specifications: semantics, properties, analysis, and simulation. ACM Trans Softw Eng Methodol 29(1):1\u20131157","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"1\u20132","key":"450_CR19","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10703-016-0251-x","volume":"49","author":"C Colombo","year":"2016","unstructured":"Colombo C, Falcone Y (2016) Organising LTL monitors over distributed systems with a global clock. Form Methods Syst Design 49(1\u20132):109\u2013158","journal-title":"Form Methods Syst Design"},{"key":"450_CR20","doi-asserted-by":"crossref","unstructured":"Danielsson LM, S\u00e1nchez C (2019) Decentralized stream runtime verification. In: Proceedings of the 19th international conference on runtime verification (RV), pp 185\u2013201","DOI":"10.1007\/978-3-030-32079-9_11"},{"key":"450_CR21","doi-asserted-by":"crossref","unstructured":"Kazemloo S, Bonakdarpour B (2018) Crash-resilient decentralized synchronous runtime verification. In: Proceedings of the 37th symposium on reliable distributed systems (SRDS), pp 207\u2013212","DOI":"10.1109\/SRDS.2018.00032"},{"key":"450_CR22","doi-asserted-by":"publisher","unstructured":"D\u2019Angelo B, Sankaranarayanan S, Sanchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) Lola: runtime monitoring of synchronous systems. In: 12th international symposium on temporal representation and reasoning (TIME\u201905), pp 166\u2013174. https:\/\/doi.org\/10.1109\/TIME.2005.26","DOI":"10.1109\/TIME.2005.26"},{"key":"450_CR23","doi-asserted-by":"crossref","unstructured":"Chauhan H, Garg VK, Natarajan A, Mittal N (2013) A distributed abstraction algorithm for online predicate detection. In: Proceedings of the 32nd IEEE symposium on reliable distributed systems (SRDS), pp 101\u2013110","DOI":"10.1109\/SRDS.2013.19"},{"issue":"3","key":"450_CR24","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s00446-004-0117-0","volume":"17","author":"N Mittal","year":"2005","unstructured":"Mittal N, Garg VK (2005) Techniques and applications of computation slicing. Distrib Comput 17(3):251\u2013277","journal-title":"Distrib Comput"},{"key":"450_CR25","doi-asserted-by":"crossref","unstructured":"Garg VK (2020) Predicate detection to solve combinatorial optimization problems. In: Proceedings of the 32nd ACM symposium on parallelism in algorithms and architectures, pp 235\u2013245","DOI":"10.1145\/3350755.3400235"},{"key":"450_CR26","doi-asserted-by":"crossref","unstructured":"Valapil VT, Yingchareonthawornchai S, Kulkarni SS, Torng E, Demirbas M (2017) Monitoring partially synchronous distributed systems using SMT solvers. In: Proceedings of the 17th international conference on runtime verification (RV), pp 277\u2013293","DOI":"10.1007\/978-3-319-67531-2_17"},{"key":"450_CR27","doi-asserted-by":"crossref","unstructured":"Momtaz A, Basnet N, Abbas H, Bonakdarpour B (2021) Predicate monitoring in distributed cyber-physical systems. In: International conference on runtime verification, pp 3\u201322. Springer","DOI":"10.1007\/978-3-030-88494-9_1"},{"key":"450_CR28","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/BFb0030684","volume-title":"Distributed algorithms","author":"SD Stoller","year":"1997","unstructured":"Stoller SD (1997) Detecting global predicates in distributed systems with clocks. In: Mavronicolas M, Tsigas P (eds) Distributed algorithms. Springer, Berlin, pp 185\u2013199"},{"key":"450_CR29","doi-asserted-by":"crossref","unstructured":"Sen K, Vardhan A, Agha G, Rosu G (2004) Efficient decentralized monitoring of safety in distributed systems. In: Proceedings of the 26th international conference on software engineering (ICSE), pp 418\u2013427","DOI":"10.1109\/ICSE.2004.1317464"},{"key":"450_CR30","unstructured":"Bonakdarpour B, Fraigniaud P, Rajsbaum S, Rosenblueth DA, Travers C (2016) Decentralized asynchronous crash-resilient runtime verification. In: Proceedings of the 27th international conference on concurrency theory (CONCUR), pp 16\u201311615"},{"key":"450_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-71500-7_1","volume-title":"Fundamental approaches to software engineering","author":"L Aceto","year":"2021","unstructured":"Aceto L, Attard DP, Francalanza A, Ing\u00f3lfsd\u00f3ttir A (2021) On benchmarking for concurrent runtime verification. In: Guerra E, Stoelinga M (eds) Fundamental approaches to software engineering. Springer, Cham, pp 3\u201323"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00450-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00450-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00450-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T18:03:15Z","timestamp":1735408995000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00450-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,14]]},"references-count":31,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["450"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00450-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2024,6,14]]},"assertion":[{"value":"15 December 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 March 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}