Verification of threshold-based distributed algorithms by decomposition to decidable logics

DOI10.1007/978-3-030-25543-5_15arXiv1905.07805MaRDI QIDQ6154883FDOQ6154883

Authors: Idan Berkovits, Marijana Lazić, Giuliano Losa, Oded Padon, Sharon Shoham 

Publication date: 16 February 2024

Published in: Computer Aided Verification (Search for Journal in Brave)

Abstract: Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only if it has received an acknowledgment from at least half of its peers. Verification of threshold-based protocols is extremely challenging as it involves two kinds of reasoning: first-order reasoning about the unbounded state of the protocol, together with reasoning about sets and cardinalities. In this work, we develop a new methodology for decomposing the verification task of such protocols into two decidable logics: EPR and BAPA. Our key insight is that such protocols use thresholds in a restricted way as a means to obtain certain properties of "intersection" between sets. We define a language for expressing such properties, and present two translations: to EPR and BAPA. The EPR translation allows verifying the protocol while assuming these properties, and the BAPA translation allows verifying the correctness of the properties. We further develop an algorithm for automatically generating the properties needed for verifying a given protocol, facilitating fully automated deductive verification. Using this technique we have verified several challenging protocols, including Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos.

Full work available at URL: https://arxiv.org/abs/1905.07805

Recommendations

• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• A logic-based framework for verifying consensus algorithms
• Complexity of Verification and Synthesis of Threshold Automata
• Eliminating message counters in synchronous threshold automata
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15) Logic in computer science (03B70) Distributed systems (68M14)

Cited In (4)

• Efficient automated reasoning about sets and multisets with cardinality constraints
• Stratified guarded first-order transition systems
• Inferring invariants with quantifier alternations: taming the search space explosion
• Symbolic model checking for TLA+ made faster

This page was built for publication: Verification of threshold-based distributed algorithms by decomposition to decidable logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154883)