{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:50Z","timestamp":1780994570074,"version":"3.54.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T00:00:00Z","timestamp":1674000000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Austrian Science Fund","award":["W 1255"],"award-info":[{"award-number":["W 1255"]}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["787367"],"award-info":[{"award-number":["787367"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Threshold guards are a basic primitive of many fault-tolerant algorithms that\nsolve classical problems in distributed computing, such as reliable broadcast,\ntwo-phase commit, and consensus. Moreover, threshold guards can be found in\nrecent blockchain algorithms such as, e.g., Tendermint consensus. In this\narticle, we give an overview of techniques for automated verification of\nthreshold-guarded fault-tolerant distributed algorithms, implemented in the\nByzantine Model Checker (ByMC). These threshold-guarded algorithms have the\nfollowing features: (1) up to $t$ of processes may crash or behave Byzantine;\n(2) the correct processes count messages and make progress when they receive\nsufficiently many messages, e.g., at least $t+1$; (3) the number $n$ of\nprocesses in the system is a parameter, as well as the number $t$ of faults;\nand (4) the parameters are restricted by a resilience condition, e.g., $n &gt;\n3t$. Traditionally, these algorithms were implemented in distributed systems\nwith up to ten participating processes. Nowadays, they are implemented in\ndistributed systems that involve hundreds or thousands of processes. To make\nsure that these algorithms are still correct for that scale, it is imperative\nto verify them for all possible values of the parameters.<\/jats:p>","DOI":"10.46298\/lmcs-19(1:5)2023","type":"journal-article","created":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T08:55:13Z","timestamp":1674032113000},"source":"Crossref","is-referenced-by-count":4,"title":["Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker"],"prefix":"10.46298","volume":"Volume 19, Issue 1","author":[{"given":"Igor","family":"Konnov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijana","family":"Lazi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilina","family":"Stoilkovska","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2023,1,18]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/10824\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/10824\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:18:51Z","timestamp":1687292331000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/6947"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,18]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-19(1:5)2023","relation":{"has-preprint":[{"id-type":"arxiv","id":"2011.14789v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2011.14789v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2011.14789","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2011.14789","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,18]]},"article-number":"6947"}}