Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems
For designers of distributed algorithms, this work offers a practical verification method for infinite-state processes in asynchronous rounds, though the undecidability result limits generality.
The paper shows that parameterized verification of asynchronous round-based distributed algorithms is undecidable, but provides a sound and complete reduction to LTL model checking over finite-counter systems, enabling verification of safety and liveness properties for consensus and leader-election algorithms using nuXmv.
Traditional model-checking techniques typically verify distributed algorithms only for a fixed number of finite-state processes. Parameterized model checking generalizes this to any number of processes, while still typically assuming that each process is finite-state. In this work, we consider asynchronous round-based distributed algorithms in which each process is infinite-state since it can execute for an infinite number of rounds. We show that the parameterized verification problem for asynchronous round-based distributed algorithms is undecidable, already for simple specifications. Nevertheless, as our main contribution, we provide a reduction to LTL model checking over finite-counter systems and prove that it is sound and complete. This enables the use of off-the-shelf, mature symbolic model checkers for finite-counter systems. We demonstrate the practical applicability of this reduction by verifying safety and liveness properties of several asynchronous round-based consensus and leader-election algorithms using the nuXmv model checker.