Graph- versus Vector-Based Analysis of a Consensus Protocol

TL;DR

This paper compares graph transformation and vector-based model checking techniques for analyzing the Paxos consensus protocol, highlighting the efficiency of graph-based methods in managing large state spaces.

Contribution

It introduces a graph transformation modeling approach for Paxos and demonstrates its advantages over traditional vector-based methods using the GROOVE model checker.

Findings

Graph transformation modeling reduces state space size.

GROOVE effectively exploits symmetry for state space reduction.

Compared to Spin, graph-based analysis handles larger models more efficiently.

Abstract

The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.