Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Tom Baumeister, Paul Eichler, Swen Jacobs, Mouhammad Sakr, Marcus Völp
TL;DR
This paper addresses parameterized verification of round-based distributed algorithms by extending threshold automata to support decrements and resets of shared variables and to verify general coverability properties under a resilience condition $RC = n > 3t \land t \ge f$. The approach combines threshold automata with well-structured transition systems and introduces a parametric interval abstraction and a $(0,1)$-abstraction to enable both general and reachability-based specifications. Key contributions include a semi-decision procedure for general coverability, a precision connection between the abstract counter system and the concrete TA, an implementation that models phase king and Red Belly Blockchain, and a performance comparison against the ByMC TA model checker on decidable benchmarks. The results demonstrate automatic verification of protocols that were previously not modelable in canonical TA, and provide practical insights into verifying fault-tolerant distributed systems.
Abstract
Threshold automata are a computational model that has proven to be versatile in modeling threshold-based distributed algorithms and enabling their completely automatic parameterized verification. We present novel techniques for the verification of threshold automata, based on well-structured transition systems, that allow us to extend the expressiveness of both the computational model and the specifications that can be verified. In particular, we extend the model to allow decrements and resets of shared variables, possibly on cycles, and the specifications to general coverability. While these extensions of the model in general lead to undecidability, our algorithms provide a semi-decision procedure. We demonstrate the benefit of our extensions by showing that we can model complex round-based algorithms such as the phase king consensus algorithm and the Red Belly Blockchain protocol (published in 2019), and verify them fully automatically for the first time.