### Abstract

Original language | Undefined |
---|---|

Title of host publication | Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014) |

Editors | Dragan Bošnački, Stefan Edelkamp, Alberto Lluch Lafuente, Anton Wijs |

Publisher | EPTCS |

Pages | 44-57 |

Number of pages | 14 |

DOIs | |

State | Published - Apr 2014 |

### Publication series

Name | Electronic Proceedings in Theoretical Computer Science |
---|---|

Publisher | EPTCS |

Volume | 159 |

ISSN (Print) | 2075-2180 |

ISSN (Electronic) | 2075-2180 |

### Fingerprint

### Keywords

- EWI-24980
- GROOVE
- Graph Transformation
- IR-91953
- Consensus Protocols
- Model Checking
- METIS-305983
- SPIN

### Cite this

*Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)*(pp. 44-57). (Electronic Proceedings in Theoretical Computer Science; Vol. 159). EPTCS. DOI: 10.4204/EPTCS.159.5

}

*Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014).*Electronic Proceedings in Theoretical Computer Science, vol. 159, EPTCS, pp. 44-57. DOI: 10.4204/EPTCS.159.5

**Graph- versus Vector-Based Analysis of a Consensus Protocol.** / Delzanno, Giorgio; Rensink, Arend; Traverso, Riccardo.

Research output: Scientific - peer-review › Conference contribution

TY - CHAP

T1 - Graph- versus Vector-Based Analysis of a Consensus Protocol

AU - Delzanno,Giorgio

AU - Rensink,Arend

AU - Traverso,Riccardo

N1 - 10.4204/EPTCS.159.5

PY - 2014/4

Y1 - 2014/4

N2 - 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.

AB - 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.

KW - EWI-24980

KW - GROOVE

KW - Graph Transformation

KW - IR-91953

KW - Consensus Protocols

KW - Model Checking

KW - METIS-305983

KW - SPIN

U2 - 10.4204/EPTCS.159.5

DO - 10.4204/EPTCS.159.5

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 44

EP - 57

BT - Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)

PB - EPTCS

ER -