Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata

TL;DR

This paper introduces advanced verification techniques for threshold automata, enabling automatic analysis of complex round-based distributed algorithms like consensus protocols, despite increased expressiveness leading to undecidability.

Contribution

It extends threshold automata with variable resets and decrements, broadening the class of verifiable distributed algorithms and providing semi-decision algorithms for their verification.

Findings

Successfully modeled the phase king consensus algorithm

Verified the Red Belly Blockchain protocol automatically

Extended the automata model to include resets and decrements

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.