## Igor Konnov ; Marijana Lazić ; Ilina Stoilkovska ; Josef Widder - Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker

lmcs:6947 - Logical Methods in Computer Science, January 18, 2023, Volume 19, Issue 1 - https://doi.org/10.46298/lmcs-19(1:5)2023
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker

Authors: Igor Konnov ; Marijana Lazić ; Ilina Stoilkovska ; Josef Widder

Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems in distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain algorithms such as, e.g., Tendermint consensus. In this article, we give an overview of techniques for automated verification of threshold-guarded fault-tolerant distributed algorithms, implemented in the Byzantine Model Checker (ByMC). These threshold-guarded algorithms have the following features: (1) up to $t$ of processes may crash or behave Byzantine; (2) the correct processes count messages and make progress when they receive sufficiently many messages, e.g., at least $t+1$; (3) the number $n$ of processes in the system is a parameter, as well as the number $t$ of faults; and (4) the parameters are restricted by a resilience condition, e.g., $n > 3t$. Traditionally, these algorithms were implemented in distributed systems with up to ten participating processes. Nowadays, they are implemented in distributed systems that involve hundreds or thousands of processes. To make sure that these algorithms are still correct for that scale, it is imperative to verify them for all possible values of the parameters.

Volume: Volume 19, Issue 1
Published on: January 18, 2023
Accepted on: November 17, 2022
Submitted on: December 1, 2020
Keywords: Computer Science - Distributed, Parallel, and Cluster Computing,Computer Science - Logic in Computer Science
Fundings :
Source : OpenAIRE Graph
• Parametrized Verification and Synthesis; Funder: European Commission; Code: 787367
• Vollantrag zu Logical Methods in Computer Science; Funder: Austrian Science Fund (FWF); Code: W 1255