TACO: A Toolsuite for the Verification of Threshold Automata

TL;DR

TACO is a comprehensive toolsuite designed for developing and automatically verifying fault-tolerant distributed algorithms modeled as threshold automata, supporting multiple verification approaches.

Contribution

It introduces a modular, extensible framework implementing various model checking algorithms for threshold automata, including both decidable and semi-decision procedures.

Findings

Implemented three model checking approaches for threshold automata.

Evaluated performance of algorithms experimentally.

Supports development of fault-tolerant distributed algorithms.

Abstract

We present TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments. Moreover, TACO is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. We present important features, give an overview of the implemented algorithms, and evaluate their performance experimentally.