{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:22:38Z","timestamp":1779074558738,"version":"3.51.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031742330","type":"print"},{"value":"9783031742347","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T00:00:00Z","timestamp":1728691200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T00:00:00Z","timestamp":1728691200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In distributed systems with processes that do not share a global clock, <jats:italic>partial synchrony<\/jats:italic> is achieved by clock synchronization that guarantees bounded clock skew among all applications. Existing solutions for distributed runtime verification under partial synchrony against temporal logic specifications are exact but suffer from significant computational overhead. In this paper, we propose an <jats:italic>approximate<\/jats:italic> distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates this issue by abstracting away potential interleaving behaviors. This conservative abstraction enables a significant speedup of the distributed monitors, albeit with a tradeoff in accuracy. We address this tradeoff with a methodology that combines our approximate monitor with its exact counterpart, resulting in enhanced efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its efficacy in both real-world applications and synthetic examples.<\/jats:p>","DOI":"10.1007\/978-3-031-74234-7_18","type":"book-chapter","created":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T10:01:58Z","timestamp":1728640918000},"page":"282-301","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Approximate Distributed Monitoring Under Partial Synchrony: Balancing Speed &amp; Accuracy"],"prefix":"10.1007","author":[{"given":"Borzoo","family":"Bonakdarpour","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anik","family":"Momtaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dejan","family":"Ni\u010dkovi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N. Ege","family":"Sara\u00e7","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,12]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: The best a monitor can do. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, 25\u201328 January 2021, Ljubljana, Slovenia (Virtual Conference). LIPIcs, vol.\u00a0183, pp. 7:1\u20137:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2021.7","DOI":"10.4230\/LIPICS.CSL.2021.7"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","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, D.P., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On benchmarking for concurrent runtime verification. In: FASE 2021. LNCS, vol. 12649, pp. 3\u201323. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_1"},{"key":"18_CR3","unstructured":"Alechina, N., Dastani, M., Logan, B.: Norm approximation for imperfect monitors. In: Bazzan, A.L.C., Huhns, M.N., Lomuscio, A., Scerri, P. (eds.) International conference on Autonomous Agents and Multi-Agent Systems, AAMAS 2014, Paris, France, 5\u20139 May 2014, pp. 117\u2013124. IFAAMAS\/ACM (2014). http:\/\/dl.acm.org\/citation.cfm?id=2615753"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Grosu, R.: Monitoring with uncertainty. In: Bortolussi, L., Bujorianu, M., Pola, G. (eds.) Proceedings Third International Workshop on Hybrid Autonomous Systems, HAS 2013, Rome, Italy, 17th March 2013. EPTCS, vol.\u00a0124, pp.\u00a01\u20134 (2013). https:\/\/doi.org\/10.4204\/EPTCS.124.1","DOI":"10.4204\/EPTCS.124.1"},{"issue":"1\u20132","key":"18_CR5","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.: Decentralised LTL monitoring. Formal Methods Syst. Design 48(1\u20132), 46\u201393 (2016)","journal-title":"Formal Methods Syst. Design"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., Fraigniaud, P., Rajsbaum, S., Rosenblueth, D.A., Travers, C.: Decentralized asynchronous crash-resilient runtime verification. J. ACM 69(5), 34:1\u201334:31 (2022)","DOI":"10.1145\/3550483"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Chauhan, H., Garg, V.K., Natarajan, A., Mittal, N.: A distributed abstraction algorithm for online predicate detection. In: Proceedings of the 32nd IEEE Symposium on Reliable Distributed Systems (SRDS), pp. 101\u2013110 (2013)","DOI":"10.1109\/SRDS.2013.19"},{"issue":"1\u20132","key":"18_CR8","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.: Organising LTL monitors over distributed systems with a global clock. Formal Methods Syst. Design 49(1\u20132), 109\u2013158 (2016)","journal-title":"Formal Methods Syst. Design"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"El-Hokayem, A., Falcone, Y.: On the monitoring of decentralized specifications: semantics, properties, analysis, and simulation. ACM Trans. Softw. Eng. Methodol. 29(1), 1:1\u20131:57 (2020)","DOI":"10.1145\/3355181"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Ganguly, R., Momtaz, A., Bonakdarpour, B.: Runtime verification of partially-synchronous distributed system. Formal Methods Syst. Design (FMSD) (2024, to appear)","DOI":"10.1007\/s10703-024-00450-5"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Ganguly, R., Momtaz, A., Bonakdarpour, B.: Distributed runtime verification under partial synchrony. In: Bramas, Q., Oshman, R., Romano, P. (eds.) 24th International Conference on Principles of Distributed Systems, OPODIS 2020, 14\u201316 December 2020, Strasbourg, France (Virtual Conference). LIPIcs, vol.\u00a0184, pp. 20:1\u201320:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2020.20","DOI":"10.4230\/LIPIcs.OPODIS.2020.20"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Garg, V.K.: Predicate detection to solve combinatorial optimization problems. In: Proceedings of the 32nd ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pp. 235\u2013245. ACM (2020)","DOI":"10.1145\/3350755.3400235"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-031-17196-3_11","volume-title":"Runtime Verification - RV 2022","author":"TA Henzinger","year":"2022","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Abstract monitors for quantitative specifications. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 200\u2013220. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_11"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-031-30829-1_17","volume-title":"Foundations of Software Science and Computation Structures - FoSSaCS 2023","author":"TA Henzinger","year":"2023","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Quantitative safety and liveness. In: Kupferman, O., Sobocinski, P. (eds.) FoSSaCS 2023. LNCS, vol. 13992, pp. 349\u2013370. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30829-1_17"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Quantitative and approximate monitoring. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, 29 June\u20132 July 2021, pp. 1\u201314. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470547","DOI":"10.1109\/LICS52264.2021.9470547"},{"issue":"3","key":"18_CR16","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Transf. 15(3), 247\u2013268 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0247-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"18_CR17","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, V.K.: Techniques and applications of computation slicing. Distrib. Comput. 17(3), 251\u2013277 (2005)","journal-title":"Distrib. Comput."},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Momtaz, A., Abbas, H., Bonakdarpour, B.: Monitoring signal temporal logic in distributed cyber-physical systems. In: Mitra, S., Venkatasubramanian, N., Dubey, A., Feng, L., Ghasemi, M., Sprinkle, J. (eds.) Proceedings of the ACM\/IEEE 14th International Conference on Cyber-Physical Systems, ICCPS 2023, (with CPS-IoT Week 2023), San Antonio, TX, USA, 9\u201312 May 2023, pp. 154\u2013165. ACM (2023). https:\/\/doi.org\/10.1145\/3576841.3585937","DOI":"10.1145\/3576841.3585937"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Mostafa, M., Bonakdarpour, B.: 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 (2015)","DOI":"10.1109\/IPDPS.2015.95"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-75142-7_32","volume-title":"Distributed Computing","author":"VA Ogale","year":"2007","unstructured":"Ogale, V.A., Garg, V.K.: Detecting temporal logic predicates on distributed computations. In: Pelc, A. (ed.) DISC 2007. LNCS, vol. 4731, pp. 420\u2013434. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75142-7_32"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Pant, Y.V., Abbas, H., Mangharam, R.: Smooth operator: control using the smooth robustness of temporal logic. In: 2017 IEEE Conference on Control Technology and Applications (CCTA), pp. 1235\u20131240. IEEE (2017)","DOI":"10.1109\/CCTA.2017.8062628"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-29860-8_15","volume-title":"Runtime Verification","author":"SD Stoller","year":"2012","unstructured":"Stoller, S.D., et al.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193\u2013207. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_15"},{"key":"18_CR24","unstructured":"USNRC: Pressurized water reactor systems (2021). https:\/\/www.nrc.gov\/reading-rm\/basic-ref\/students\/for-educators\/04.pdf"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-74234-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T10:04:12Z","timestamp":1728641052000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-74234-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,12]]},"ISBN":["9783031742330","9783031742347"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-74234-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,12]]},"assertion":[{"value":"12 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Instanbul","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"T\u00fcrkiye","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/yeni.cmpe.bogazici.edu.tr\/rv24\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}