{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:36:29Z","timestamp":1770896189163,"version":"3.50.1"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2022,10,27]],"date-time":"2022-10-27T00:00:00Z","timestamp":1666828800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF","award":["FMitF Award 1917979 and SaTC Award 1813388"],"award-info":[{"award-number":["FMitF Award 1917979 and SaTC Award 1813388"]}]},{"name":"ANR"},{"name":"UNAM-PAPIIT","award":["IN106520"],"award-info":[{"award-number":["IN106520"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            <jats:italic>Runtime verification<\/jats:italic>\n            is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous\n            <jats:italic>distributed<\/jats:italic>\n            monitors observing the system, only if each monitor can emit verdicts taken from a\n            <jats:italic>large enough<\/jats:italic>\n            finite set. We revisit this impossibility result in the concrete context of linear-time logic (\n            <jats:sc>ltl<\/jats:sc>\n            ) semantics for runtime verification, that is, when the correctness of the system is specified by an\n            <jats:sc>ltl<\/jats:sc>\n            formula on its execution traces. First, we show that monitors synthesized based on the 4-valued semantics of\n            <jats:sc>ltl<\/jats:sc>\n            (\n            <jats:sc>rv-ltl<\/jats:sc>\n            ) may result in inconsistent distributed monitoring, even for some simple\n            <jats:sc>ltl<\/jats:sc>\n            formulas. More generally, given any\n            <jats:sc>ltl<\/jats:sc>\n            formula\u00a0\u03c6, we relate the number of different verdicts required by the monitors for consistently monitoring\u00a0\u03c6, with a specific structural characteristic of\u00a0\u03c6 called its\n            <jats:italic>alternation number<\/jats:italic>\n            . Specifically, we show that, for every\n            <jats:italic>k \u2265 0<\/jats:italic>\n            , there is an\n            <jats:sc>ltl<\/jats:sc>\n            formula\u00a0\u03c6 with alternation number\u00a0\n            <jats:italic>k<\/jats:italic>\n            that cannot be verified at runtime by distributed monitors emitting verdicts from a set of cardinality smaller than\n            <jats:italic>k<\/jats:italic>\n            + 1. On the positive side, we define a family of logics, called\n            <jats:italic>distributed<\/jats:italic>\n            <jats:sc>ltl<\/jats:sc>\n            (abbreviated as\n            <jats:sc>dltl<\/jats:sc>\n            ), parameterized by\n            <jats:italic>k<\/jats:italic>\n            \u2265 0, which refines\n            <jats:sc>rv-ltl<\/jats:sc>\n            by incorporating\n            <jats:italic>2k<\/jats:italic>\n            + 4 truth values. Our main contribution is to show that, for every\n            <jats:italic>k<\/jats:italic>\n            \u2265 0, every\n            <jats:sc>ltl<\/jats:sc>\n            formula\u00a0\u03c6 with alternation number\u00a0\n            <jats:italic>k<\/jats:italic>\n            can be consistently monitored by distributed monitors, each running an automaton based on a (2 \u2308\n            <jats:italic>k<\/jats:italic>\n            \/2 \u2309 +4)-valued logic taken from the\n            <jats:sc>dltl<\/jats:sc>\n            family.\n          <\/jats:p>","DOI":"10.1145\/3550483","type":"journal-article","created":{"date-parts":[[2022,8,10]],"date-time":"2022-08-10T12:20:09Z","timestamp":1660134009000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Decentralized Asynchronous Crash-resilient Runtime Verification"],"prefix":"10.1145","volume":"69","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1800-5419","authenticated-orcid":false,"given":"Borzoo","family":"Bonakdarpour","sequence":"first","affiliation":[{"name":"Michigan State University, U.S.A."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4534-4803","authenticated-orcid":false,"given":"Pierre","family":"Fraigniaud","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris and CNRS, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0009-5287","authenticated-orcid":false,"given":"Sergio","family":"Rajsbaum","sequence":"additional","affiliation":[{"name":"Universidad Nacional Aut\u00f3nomade M\u00e9xico, M\u00e9xico"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8933-8267","authenticated-orcid":false,"given":"David","family":"Rosenblueth","sequence":"additional","affiliation":[{"name":"Universidad Nacional Aut\u00f3nomade M\u00e9xico, M\u00e9xico"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6797-4542","authenticated-orcid":false,"given":"Corentin","family":"Travers","sequence":"additional","affiliation":[{"name":"University of Bordeaux and CNRS, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,27]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/153724.153741"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2732263"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200869"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2022.104869"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795279463"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1002\/0471478210"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn075"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_10"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2013.105"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_25"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_14"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS.2013.19"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_12"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2018.2809551"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14472-6_11"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-013-0188-x"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_9"},{"key":"e_1_3_2_22_2","first-page":"20:1\u201320:17","volume-title":"Proceedings of the 24th International Conference on Principles of Distributed Systems (OPODIS)","author":"Ganguly R.","year":"2020","unstructured":"R. Ganguly, A. Momtaz, and B. Bonakdarpour. 2020. Distributed runtime verification under partial asynchrony. In Proceedings of the 24th International Conference on Principles of Distributed Systems (OPODIS). 20:1\u201320:17."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.5555\/2568432"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020429"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-004-0117-0"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2015.95"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75142-7_32"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_38"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27860-3_17"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999446"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3550483","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3550483","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3550483","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:17Z","timestamp":1750182677000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3550483"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,27]]},"references-count":31,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3550483"],"URL":"https:\/\/doi.org\/10.1145\/3550483","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,27]]},"assertion":[{"value":"2020-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-10-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}