{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T14:32:35Z","timestamp":1763389955835,"version":"3.45.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2026,1,31]]},"abstract":"<jats:p>\n                    This article focuses on the runtime verification of hyperproperties expressed in Hyper-\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{rec}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    HML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathsf{rec}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    HML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralized monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.\n                  <\/jats:p>","DOI":"10.1145\/3767738","type":"journal-article","created":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T13:30:44Z","timestamp":1758029444000},"page":"1-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Centralized vs. Decentralized Monitors for Hyperproperties"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2197-3018","authenticated-orcid":false,"given":"Luca","family":"Aceto","sequence":"first","affiliation":[{"name":"Department of Computer Science, Reykjavik University, Reykjavik, Iceland and Gran Sasso Science Institute, L\u2019Aquila, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1314-333X","authenticated-orcid":false,"given":"Antonis","family":"Achilleos","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Reykjavik University, Reykjavik, Iceland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7526-9256","authenticated-orcid":false,"given":"Elli","family":"Anastasiadi","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University, Aalborg, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3829-7391","authenticated-orcid":false,"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[{"name":"University of Malta, Msida, Malta"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8859-9844","authenticated-orcid":false,"given":"Daniele","family":"Gorla","sequence":"additional","affiliation":[{"name":"Department of Computer Science, \u201cSapienza\u201d University of Rome, Rome, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8616-3905","authenticated-orcid":false,"given":"Jana","family":"Wagemaker","sequence":"additional","affiliation":[{"name":"iCIS, Radboud University, Nijmegen, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2025,11,17]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08679-3_1"},{"key":"e_1_3_2_3_1","first-page":"1","volume-title":"35th International Conference on Concurrency Theory (CONCUR)","volume":"311","author":"Aceto Luca","year":"2024","unstructured":"Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, and Jana Wagemaker. 2024a. Centralized vs decentralized monitors for hyperproperties. In 35th International Conference on Concurrency Theory (CONCUR). LIPiCS, Vol. 311, Article 34, 1\u201319."},{"key":"e_1_3_2_4_1","doi-asserted-by":"crossref","unstructured":"Luca Aceto Antonis Achilleos Elli Anastasiadi Adrian Francalanza Daniele Gorla and Jana Wagemaker. 2025. Centralized vs decentralized monitors for hyperproperties. arXiv:2405.12882. Retrieved from https:\/\/arxiv.org\/abs\/2405.12882","DOI":"10.1145\/3767738"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08143-9_12"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2023.103031"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290365"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31514-6_15"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-21485-2_4"},{"key":"e_1_3_2_10_1","doi-asserted-by":"crossref","unstructured":"Luca Aceto Antonis Achilleos Adrian Francalanza Anna Ing\u00f3lfsd\u00f3ttir and Karoliina Lehtinen. 2021. An operational guide to monitorability with applications to regular properties. Software and Systems Modeling 20 2 (2021) 335\u2013361.","DOI":"10.1007\/s10270-020-00860-z"},{"key":"e_1_3_2_11_1","first-page":"1","volume-title":"38th European Conference on Object-Oriented Programming (ECOOP)","author":"Aceto Luca","year":"2024","unstructured":"Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ing\u00f3lfsd\u00f3ttir. 2024c. Runtime instrumentation for reactive components. In 38th European Conference on Object-Oriented Programming (ECOOP). LIPIcs, Vol. 313, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 16, 1\u201333."},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-023-00441-9"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.24"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78089-0_14"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/3635637.3662865"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.02.009"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46982-9_4"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00019"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3550483"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47169-3_27"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_2"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_5"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.254.6"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44267-4_9"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_3_2_34_1","first-page":"194","volume-title":"24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201918)","author":"Finkbeiner Bernd","year":"2018","unstructured":"Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. 2018. RVHyper: A runtime verification tool for temporal hyperproperties. In 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201918). LNCS, Vol. 10806, Springer, 194\u2013200."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-019-00334-z"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2017.30"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","unstructured":"Pierre Fraigniaud Sergio Rajsbaum and Corentin Travers. 2020. A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring. Journal of Applied and Computational Topology 4 1 (2020) 141\u2013179. DOI: 10.1007\/s41468-019-00047-6","DOI":"10.1007\/s41468-019-00047-6"},{"key":"e_1_3_2_38_1","first-page":"1","volume-title":"28th International Conference on Concurrency Theory (CONCUR)","author":"Francalanza Adrian","year":"2017","unstructured":"Adrian Francalanza. 2017. Consistently-detecting monitors. In 28th International Conference on Concurrency Theory (CONCUR). LIPIcs, Vol. 85, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 8, 1\u201319."},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2021.104704"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Adrian Francalanza Luca Aceto and Anna Ing\u00f3lfsd\u00f3ttir. 2017. Monitorability for the Hennessy-Milner logic with recursion. Formal Methods in System Design 51 1 (2017) 87\u2013116. DOI: 10.1007\/S10703-017-0273-Z","DOI":"10.1007\/S10703-017-0273-Z"},{"key":"e_1_3_2_41_1","doi-asserted-by":"crossref","unstructured":"Adrian Francalanza Andrew Gauci and Gordon J. Pace. 2013. Distributed system contract monitoring. The Journal of Logic and Algebraic Programming 82 5\u20137 (2013) 186\u2013215.","DOI":"10.1016\/j.jlap.2013.04.001"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","unstructured":"Jens Oliver Gutsfeld Markus M\u00fcller-Olm and Christoph Ohrem. 2021. Automata and fixpoints for asynchronous hyperproperties. Proceedings of the ACM on Programming Languages 5 POPL Article 38 (Jan. 2021) 29 pages. DOI: 10.1145\/3434319","DOI":"10.1145\/3434319"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_7"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67531-2_26"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837662"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.08.021"},{"key":"e_1_3_2_49_1","doi-asserted-by":"crossref","unstructured":"Ruggero Lanotte Massimo Merro and Andrei Munteanu. 2023. Industrial control systems security via runtime enforcement. ACM Transactions on Privacy and Security 26 1 (2023) 4:1\u20134:41.","DOI":"10.1145\/3546579"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90038-J"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131864"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90117-4"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_38"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00214-X"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/550448"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73582"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3767738","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T12:59:52Z","timestamp":1763384392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3767738"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,17]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1,31]]}},"alternative-id":["10.1145\/3767738"],"URL":"https:\/\/doi.org\/10.1145\/3767738","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2025,11,17]]},"assertion":[{"value":"2024-10-22","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-31","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}