arXiv CSopen access

TACO: A Toolsuite for the Verification of Threshold Automata

TACO: A Toolsuite for the Verification of Threshold Automata Paul Eichler1 , Tom Baumeister1 , Mouhammad Sakr2 , Mahboubeh Kalateh Dowlati3 , Marcus Völp3 , and Swen Jacobs1

arXiv:2605.06118v1 [cs.DC] 7 May 2026

1

CISPA Helmholtz Center for Information Security, Germany 2 American University of Beirut, Lebanon 3 SnT, Luxembourg University, Luxembourg

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

1

Introduction

Ensuring the correctness of the algorithms at the heart of modern distributed systems is a challenging but important task. Many different approaches, models, and tools have been developed to tackle this challenge [15, 17, 33, 36, 39, 41, 50]. Real-world systems require their underlying distributed algorithms to be fault-tolerant and to scale to any number of participants. While verifying correctness with a parameterized number of processes is already challenging, faulttolerance additionally requires to reason modulo a resilience condition that bounds the type and number of faults that can be tolerated. Without such a condition, it is impossible for many essential algorithms to achieve their desired properties [35]. In Taco, we have chosen threshold automata (TA) as the underlying system model as it supports a parametric number of processes as well as resillience conditions [24,27,32,33]. This model allows expressing many essential consensus algorithms [8–10, 19, 37], as well as more advanced distributed algorithms, e.g., from modern blockchain applications [11, 24]. Intuitively, a TA models the local state of a participant of a protocol in the automaton locations and the global state by shared integer variables. These variables essentially count how often a given event (e.g., broadcast of a certain message) has happened so far. Thresholds can be assigned as guards to transitions of the TA, such that an action can only be taken after the threshold is crossed. Moreover, different fragments of TA have been shown to support decidable parameterized verification, i.e., their correctness can be decided independent of

2

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

the number of participants [3, 8, 18, 25–30, 33, 46, 47]. As the restrictions of these decidable fragments may be too strict for certain applications, such as roundbased algorithms with resets of shared variables, more generalized verification approaches based on semi-decision procedures have also been considered [6]. While TA can be used to express and verify many interesting distributed algorithms, and the theory of TA is well-documented and steadily growing, the situation is not as satisfactory on the tool side: The only publicly available tool for TA is ByMC [18, 22, 24, 26–30, 32], which is no longer maintained. Implementations of other decision procedures for TA and variants of TA are prototypes not well-suited for use by non-expert users and further development by third parties [2, 3, 6, 45, 47, 48]. The only related tool that is publicly available and currently supported is PyLTA, a model checker for layered threshold automata (LTA) [49]. However, LTA are not a generalization of standard TA, and PyLTA does not support the existing TA benchmark library. Contributions. In this paper, we present Taco4 , a toolsuite for the development and verification of threshold-based distributed algorithms. Taco provides: 1. an efficient implementation of three model checking algorithms that scale to previously unsolved TA and extensions of the standard TA model, and 2. a documented, maintained, and extensible code base, well-suited to serve as the basis of future model checkers and tools for TA, as well as 3. an intuitive user interface that supports users in modeling and debugging distributed algorithms. In this paper, we will give a high-level overview of the three algorithms, describe important features of Taco, and evaluate the performance of the algorithms on different classes of benchmarks, comparing their strengths and weaknesses.

2

System Model and Specifications

We first define the underlying formal model of TA and introduce the specification language, before providing more details on the architecture of Taco. Definition 1 (Threshold Automaton [27, 32]). A threshold automaton (TA) is a tuple A = (L, I, Γ, Π, R, RC) where L is a finite set of locations, I ⊆ L the set of initial locations, Γ is a finite set of shared variables over N0 , Π is a finite set of parameter variables over N0 , RC is the resilience condition, a linear integer arithmetic formula over parameter variables, and R is a set of |Γ | rules. A rule is a tuple r = (from, to, φ, uv) where, from, to ∈ L, uv ∈ N0 the update vector for shared variables and φ is a conjunction of lower guards P|Π| and upper guards. A lower guard is a constraint a0 + i=1 ai ·pi ≤ x, with 4

TACO’s source code is available on GitHub https://github.com/cispa/TACO and the documentation is on the webpage https://taco-mc.dev. A reproduction package containing the source code, benchmark files and documentation at the time of submission is available on Zenodo [12].

TACO: A Toolsuite for the Verification of Threshold Automata

3

x ∈ Γ , a0 , . . . , a|Π| ∈ Q, p1 , . . . , p|Π| ∈ Π. An upper guard is a constraint P|Π| a0 + i=1 ai ·pi > x. The left-hand side of a lower or upper guard is a threshold. |Γ |

Note that the update vector uv is in N0 and consequently shared variables can only increase. In the following, we will also call such an automaton a monotonic threshold automaton (MTA). MTA do not allow variable decrements or resets, which restricts their ability to model algorithms, including round-based distributed algorithms, whose execution relies on resetting or reusing rounds. To address this limitation, Taco |Γ | additionally supports extended threshold automata (ETA) [6], where uv ∈ Z0 , i.e., variables can also be decremented, and a rule contains an additional set τ ⊆ Γ which contains the variables that are reset to 0. To simplify the presentation, where the distinction does not affect our results, we refer to both models simply as threshold automata (TA). Otherwise, we distinguish between ETA and MTA as required. Common parameter variables in TA are Π = {n, t, f }, where n is the number of processes, t is a bound on the number of faulty processes, and f is the actual number of faulty processes. This allows RC to express assumptions about the fraction of faulty processes in the system, e.g., RC = n > 3t ∧ t ≥ f . Algorithm 1 1: int v ← input({0, 1}) 2: broadcast v; 3: R ← receive messages from all; 4: if |{r ∈ R : r = 1}| > n − t 5: decide 1; 6: if |{r ∈ R : r = 0}| > n − t 7: decide 0;

v0

r0 :

x0 +

+

r2 :

x0 ≥

n−

t

d0

t

d1

wait

v1

r1 :

x1 +

+

r3 :

x1 ≥

n−

Figure 2: TA of the algorithm in Fig. 1

Figure 1: A simple voting protocol. Example 1. Fig. 1 shows pseudocode for a naive voting protocol. Figure 2 sketches the corresponding TA (taken from [6]) with I = {v0 , v1 }, L = {v0 , v1 , wait, d0 , d1 }, Γ = {x0 , x1 }, Π = {n, t}. A process in v0 has a vote of 0 and a process in v1 has a vote of 1. If at least n − t processes vote with 0 (respectively, 1), the decision will be 0 (1), modeled by all processes moving to d0 (d1 ). For a more advanced example, including variable resets, see Appendix A. |L|

Configurations. A configuration of a TA is a triple σ = (k, g, p), where k ∈ N0 |Γ | assigns a number of processes to each location, g ∈ N0 is a valuation of the shared variables, and p is a parameter valuation such that p |= RC, i.e., RC holds after substituting each parameter with its value given by p. We say that a configuration is initial if g = 0 and ∀i k[i] > 0 ⇒ li ∈ I. Paths. A rule r = (from, to, φ, uv, τ ) is enabled in a configuration σ = (k, g, p) if k[from] > 0 and (g, p) |= φ, producing σ ′ = r(σ), where r(σ) denotes the

4

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

resulting configuration after some process executes r, updating k and g. A path π is then a sequence of configurations π = σ0 , σ1 , . . . such that for each i there exists an enabled rule ri with σi+1 = ri (σi ). A configuration σr is said to be reachable if there exists a path starting from an initial configuration and ending in σr . We also refer to a path reaching an error configuration as an error path. Specifications. Taco supports safety properties in the temporal logic ELT LF T [30], which can express reachability of configurations where certain locations are empty or non-empty. Note that, in contrast to ByMC [22, 29], Taco currently does not support liveness properties. However, Taco allows lower integer bounds on the number of processes in a location. Formally, the supported specification syntax is defined as follows: ψ ::= pform | □ψ | ψ ∧ ψ pform ::= cform | gform ∨ cform cform ::= σ.k[l] ∗ n | σ.k[l] = 0 | σ.k[l] ̸= 0 | cform ∧ cform | cform ∨ cform gform ::= φ | ¬gform | gform ∧ gform where φ is a rule guard as defined in Definition 1, l ∈ L, n ∈ N, ∗ ∈ {>, ≥}, and □ denotes the temporal operator ’globally’. For the example above, the specification □ (σ.k[d0 ] = 0 ∨ σ.k[d1 ] = 0) states that processes cannot decide on different values. Parameterized Verification. More formally, the problem that Taco aims to solve is checking these specifications against the parameterized system specified by the TA, i.e., the infinite family of concrete transition systems resulting from instantiating parameter variables with valuations that satisfy the resilience condition RC. This problem is known to be decidable for MTA [3, 6, 27] and undecidable for ETA (as a consequence of results in [33]).

3

Architecture and Implementation

A high-level overview of the architecture of Taco is provided in Fig. 3. At the heart of Taco are three different model checking algorithms, based on representations for different flavors of TA, on different abstraction levels. Additionally, it contains a parser for specification files, a preprocessor, unified interfaces to binary decision diagram (BDD) [20] libraries and satisfiability modulo theories (SMT) solvers, as well as utility code (not shown in the figure), e.g., for the command line interface (CLI). All components are designed to be usable individually to enable fast and easy development of, for example, new model checking algorithms, different user interfaces, new specification formats or testing of new backends like a new BDD library. We describe the most interesting components in more detail below. For algorithmic details of the model checking algorithms, we refer the reader to the respective original publications [3, 6].

TACO: A Toolsuite for the Verification of Threshold Automata

5

Input .ta /.eta /.tla

Preprocessor parse input LIATA

SMT Model Checker

all paths

SMT Solver

BDD

derive input

ZCS Model Checker

error paths

ACSTA

ACS Model Checker

error paths

Threshold Automata Representations

Model Checkers

IntervalTA

SMT Encoder

Result

derive input

Figure 3: Architecture of the TACO toolsuite

Tool-Supported Modelling Languages. Taco supports models in two different languages. The first is an extension of the language introduced by ByMC for modelling threshold automata [22, 23, 29], which are usually denoted by the file ending .ta (.eta for extended threshold automata). The second is a fragment of TLA+ [34], a more well-known language for model checking, which enables expressing the same models in a logic-based framework. The grammars of both languages are available in the tool repository and an informal description of the formats on the tool page. A .ta model corresponding to the threshold automaton depicted in Fig. 2 is provided in Listing 1 and Section B.2 provides the same model written in the TLA+ fragment. ta ALG1 { shared x0, x1; 3 parameters n, t; 4 assumptions (2) { n > 3 * t; } 5 locations (5) { V0: [0]; V1: [1]; D0: [2]; D1: [3]; WAIT: [4]; } 6 inits(4) { WAIT == 0; D0 == 0; D1 == 0; V1 + V0 == n; x0 == 0; x1 == 0; } 7 rules (4) { 8 0: V0 -> WAIT when (true) do { x0’ := x0 + 1; }; 9 1: V1 -> WAIT when (true) do { x1’ := x1 + 1; }; 10 2: WAIT -> D0 when (x0 >= n - t) do {}; 11 3: WAIT -> D1 when (x1 >= n - t) do {}; 12 } 13 specifications (1) { 14 cor: [](!(D0 > 0 && D1 > 0)) 15 } 16 } 1 2

Listing 1: TA of Fig. 2 encoded as a .ta file

6

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

Preprocessor. The Taco preprocessor parses the TA and performs a sanity check on the input, followed by a static analysis of the TA and the specification in order to simplify the problem. This includes removing self-loops without effect on the variables and transition guards that are always satisfied under the given resilience condition of the TA. Optionally, the preprocessor can also remove transitions with guards that will never be satisfied in the given TA. Moreover, if Taco can statically determine that, under the assumptions on initial states given in the specification, some locations are never reachable, then these locations are completely removed before checking the property. SMT Model Checking Algorithm. Balasubramanian et al. [3] showed that the reachability problem for MTA can be reduced to deciding the satisfiability of an SMT formula. More precisely, they construct an existential Presburger arithmetic formula ϕREACH (σ, σ ′ ) such that an assignment for σ, σ ′ satisfies ϕREACH (σ, σ ′ ) if and only if σ ′ is reachable from σ for the given MTA. This algorithm directly uses a basic TA representation shown as LIATA in Fig. 3, corresponding closely to the definition of ETA. In contrast to the original implementation described in [3] and published later at [2], we do not use non-deterministic guessing to keep SMT queries small. Instead, we encode all steady paths and leave it to the SMT solver to resolve the non-determinism. Note that this algorithm can only verify correctness of MTA since it relies on the monotonicity of guards, which requires that whenever a lower (upper) guard is disabled (enabled), it stays disabled (enabled) forever. ZCS Model Checking Algorithm. This algorithm, originally described in [6], is based on an abstraction of the parameterized system semantics to a set of 01counter systems (ZCS) [13, 18, 40]. It uses the IntervalTA representation, which is derived from LIATA, where the main difference is that shared variables are mapped to a finite domain through parametric interval abstraction [18,21]. This interval abstraction depends on a total ordering between thresholds. As this may depend on parameter valuations, Taco uses the SMT solver to compute all possible orders under the resilience condition, and then constructs the corresponding IntervalTA and the ZCS representing its abstract semantics for each of them.The finite state space of each ZCS is represented and manipulated using BDDs. Based on a set of ZCS error configurations, derived from the specification, the ZCS Model Checker performs a BDD-based backward exploration from the error configurations until reaching a fixed point. Finally, it checks breadthfirst if the resulting error graph contains a non-spurious path, i.e., a path of the ZCS that can be instantiated to a concrete error path. Note that for ETA, the procedure is only a semi-decision procedure. ACS Model Checking Algorithm. The ACS Model Checker follows a similar workflow as the ZCS Model Checker, but operates on an abstract counter system (ACS) that keeps track of the concrete number of processes in each location. It was shown in [6] that an ACS forms a WSTS, which enables parameterized safety verification by a fixed point computation using finite representations of infinite sets of configurations [1, 14].

TACO: A Toolsuite for the Verification of Threshold Automata

7

The ACS Model Checker operates on the ACSTA representation, which is derived from the IntervalTA by amending it with a representation of configurations that enables efficient implementation of the WSTS-based fixed point computation. Based on this representation, the algorithm maintains a representation of all visited configurations in a tree data structure, facilitating fast lookups of comparable configurations (with respect to the well-quasi order (wqo)). As a heuristic that has proven useful, the SMT checks for spuriosity of abstract error paths are done incrementally over the length of the path. This allows us to exclude whole sets of abstract paths with relatively simple SMT queries, and the SMT solver can re-use information from the shorter paths when checking their extensions. However, the performance of this heuristic depends on how efficiently the SMT solver supports incremental queries. Note that for ETA, the procedure is only a semi-decision procedure and does not support specifications that require target locations to be empty, for more details refer to [6].

4

Tool Features

Basic User Experience. Taco supports the fully automatic verification of threshold automata: Supply it with a TA and a specification, and it will automatically choose a model checking algorithm5 and answer whether the specification is satisfied. This allows users who are not experts to use the tool, as long as they can produce inputs in one of the supported formats. The basic input format for TA is adopted from ByMC [22, 29], enabling intuitive modeling and re-use of the existing benchmark library. In addition, Taco supports a fragment of TLA+ , which is more welcoming for users familiar with TLA+ and also allows checking fixed-size instances of the protocol. Both formats allow the inclusion of specifications in ELT LF T (described in Section 2). Taco has been developed with user experience in mind. In case of user errors such as faulty inputs, it provides easy-to-read and extensively documented API and CLI interfaces. Advanced Features. Although Taco can be used as a push-button tool, it offers lots of additional features for advanced users. Besides a simple yes/no answer on whether the current protocol satisfies the specification, Taco also provides algorithm designers with richer, informative outputs. This includes the visualization of TA for more intuitive modeling and verification, concrete error traces if an error is found during verification, or intermediate results such as abstract error paths. These outputs can help the designer to identify unintended behavior of the protocol and amend it accordingly. Additionally Taco exposes a wealth of configuration parameters for experts. The user can, for example, choose which of the three model checking algorithms 5

The default model checker for standard TA is the SMT model checker, and for ETA the ZCS model checker.

8

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

to use or configure the backend components. This includes configuring SMT solver tactics or setting the reordering method of the BDD managers. Extensions of the System Model. In contrast to previous tools for the verification of threshold automata, Taco goes beyond the decidable fragment. It is the first tool to support ETA. While Taco is not guaranteed to terminate for such inputs, our experiments (in Section 5) show that it can solve a number of benchmarks from this class. Code Quality and Modularity.The goal of a model checker is to verify the correctness. However, to meaningfully increase the confidence in a protocol, the verifier must be trustworthy itself. Therefore, we use extensive testing, achieving ∼ 97% line coverage at the time of writing, and software engineering best practices such as code reviews and linting to maintain a high-quality code base. Additionally, Taco is written entirely in the safe fragment of Rust, guaranteeing memory and type safety while not adding major overhead and allowing for low-level optimizations. Moreover, to enable others to write tools for TA based on Taco, we designed it in a highly modular and reusable fashion. Most major components (e.g., parser, preprocessor, TA representations, and model checking algorithms) are separated into individual, publicly available Rust crates. This should allow others to easily re-use them and, for example, add other model checking algorithms. The same modular approach has been taken for backend components such as SMT solvers or BDD libraries. Taco supports any SMT solver that uses the SMTLIB2 standard [5] and has an interactive mode. For BDD libraries we implemented a general high-level interface, which requires minimal code to add a new library, and we currently support CUDD [42, 43] and OxiDD [16].

5

Experimental Evaluation

We evaluate all three of our model checking algorithms and compare them against the only available existing tool for verification of TA, ByMC [22, 29]. Other implementations of approaches from the literature, such as Balasubramanian et al. [2, 3] or Baumeister et al. [6], are research prototypes that do not support our benchmark suite without additional manual effort, for example manual input for the parametric interval abstraction [6] or encoding of benchmarks by hand into internal data structures [2,3]. Additionally, comparing Taco to the execution times reported in [6], Taco significantly outperforms the implementation in [6], especially on the larger ETA benchmarks. Setup. All model checkers were run in their default settings6 and set to terminate upon detecting a violated property. By default, Taco uses Z3 [38] as SMT solver, and the ZCS model checker uses CUDD [42, 43] as the BDD library. 6

We also attempted to run an additional mode of ByMC but it reported invalid counterexamples, for more details, see Section C.2.

TACO: A Toolsuite for the Verification of Threshold Automata

9

The experiments were conducted on machines with two AMD EPYC 7773x processors, with 64 cores each and 2TB RAM. Time and memory consumption was monitored with the time command and we report the elapsed wall-clock time. A more detailed description of the setup can be found in Section C.1. Benchmark Sets. Overall, we used five sets of benchmarks for our evaluation. For MTA (supported by all model checkers), we used 1. ByMC Handcoded ISOLA18, a set of handcrafted TA that appeared in [29], 2. ByMC ISOLA18 Promela, a set of benchmarks that was obtained by executing the Promela translation of ByMC and also from [29], and 3. RedBelly small, containing Red Belly blockchain components [11] modeled as TA [6, 7]. 7 As mentioned in Section 2, Taco only supports the safety fragment of ELT LF T . Therefore, the comparisons were performed on properties within that fragment. Additionally, we compared the model checkers that support ETA (our ZCS and ACS model checkers) on two variants of a multi-phase King Consensus protocol and a set of multi-phase RedBelly benchmarks taken from [6]. The execution times and memory consumption for all model checkers are given in Table 1. 8 Analysis: MTA Benchmarks. On all benchmarks, except “nbacg” and “nbacr” from the Promela set, at least one model checker of Taco outperformed ByMC. On the majority of the safe benchmarks (15 out of 19), one or both of the ZCS and ACS model checkers were among the fastest. This is mostly because for these TA the abstract error graphs constructed in those model checkers contained few paths that needed to be checked using the SMT solver or were even empty. Notably, for the hand-coded “cc” benchmark, both the ACS and ZCS model checkers timed out. For this benchmark, both error graphs contain many abstract error paths that have to be checked for spuriousness by ACS and ZCS. Out of the nine unsafe benchmarks, four were solved fastest by the SMT model checker, two by ByMC, and two by the ZCS approach. In most of these cases, the ACS- and ZCS-based approaches timed out, since the error graph contains many abstract error paths and takes a lot of time to check them. The two benchmarks that were solved fastest by ByMC were not solved within the timeout by the SMT-based approach, but they were solved in less than a minute by the ZCS-based approach. Here, the formula ϕREACH is very big, whereas the error graph and the number of abstract error paths in the ZCS approach remain feasible. Surprisingly, ByMC reported unsupported syntax for the “cc_case*” benchmarks from Promela. The cause was unclear, since the files were generated using ByMC, appear valid, and were accepted by Taco. In summary, these results show that on unsafe benchmarks, the SMT-based approach outperforms most model checkers, with some exceptions where the ZCS approach is faster. On safe benchmarks, the ACS and ZCS approaches 7 8

For more details on the origin and selection of benchmarks, refer to Section C.3. Extended benchmark results ,e.g., Taco with CVC5, can be found in Section C.4.

10

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

Table 1: Benchmark results for Taco and ByMC. Columns |L| and |R| give the number of locations and rules of the TA, respectively. In column “safe?” ✓ denotes that all checked properties hold, ✗ denotes a violated property was found, and ? that the result is unknown. Execution time (here wall clock time) is given in seconds, TO denotes a timeout after 20min. The fastest execution time per benchmark is highlighted in bold font. RSS columns give the maximal resident set size in GB. “Err” denotes that an error was returned. TA

ByMC

|L| |R| safe?

time RSS

Benchmark

MTA Benchmarks ByMC Handcoded ISOLA18 [29] aba 5 10 bcrb 5 13 bosco 8 20 c1cs 9 30 cc 7 14 cf1s 9 26 nbacg 8 16 nbacr 7 16 strb 4 8 RedBelly small [6] rb-bc 10 19 rb-simple 19 33 rb 26 41 ByMC ISOLA18 Promela [29] aba_case1 37 202 aba_case2 61 425 bosco_case1 28 152 bosco_case2 40 242 bosco_case3 32 188 c1cs_case1 101 1285 c1cs_case2 70 650 c1cs_case3 101 1333 cc_case1 164 2064 cc_case2 73 470 cc_case3 304 6928 cc_case4 161 2105 cf1s_case1 41 280 cf1s_case2 41 280 cf1s_case3 68 696 frb 7 14 nbacg 24 64 nbacr 77 1031 strb 7 21 ETA Benchmarks King Consensus [6] phase-king-buggy phase-king RedBelly with resets [6] rb-2x_reset rb-floodMin_V0 rb-floodMin_V1 rb-RelBrd_V1 rb-reset_V0 rb-reset_V1 rb-simple-2x_reset_V0 rb-simple-2x_reset_V1 rb-simple-reset_V0 rb-simple-reset_V1

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

0.69 0.04 0.42 0.04 139.33 0.07 TO 0.40 0.04 397.75 0.10 0.36 0.04 0.31 0.04 0.26 0.04

✓ ✓ ✓

0.96 0.04 TO TO -

SMT time RSS

TACO ACS time RSS

ZCS time RSS

0.07 0.03 0.06 0.03 0.07 0.03 0.08 0.03 0.07 0.03 0.07 0.03 1.03 0.04 117.29 0.04 160.34 0.05 0.72 0.05 1.68 0.03 29.25 0.05 0.26 0.04 TO TO 0.22 0.04 0.17 0.03 0.28 0.05 0.24 0.05 0.24 0.05 0.41 0.05 0.08 0.05 0.08 0.05 0.11 0.05 0.06 0.03 0.06 0.03 0.04 0.03 0.14 0.03 1.24 0.07 10.04 0.49

0.09 0.03 7.18 0.82 58.47 3.44

0.11 0.03 0.81 0.03 0.85 0.03

✓ ✓ ✗ ✗ ✗ ✗ ✗ ✗ ? ✗ ? ? ✓ ✓ ✓ ✓ ✗ ✗ ✓

15.19 0.06 2.08 0.17 1.19 0.03 1.43 0.04 290.42 0.11 19.49 0.74 17.79 0.09 15.12 0.15 45.16 0.06 7.61 0.09 332.93 0.06 104.76 0.19 752.65 0.08 38.47 0.21 TO TO 52.14 0.06 13.30 0.12 982.39 0.10 117.45 0.17 Err TO TO 83.00 0.22 TO 1164.87 14.06 102.70 0.41 26.23 0.15 TO TO TO TO Err TO TO TO Err - 1178.05 8.82 TO TO Err TO TO TO Err TO TO TO 18.31 0.07 8.22 0.90 0.43 0.03 0.59 0.03 102.08 0.10 7.25 0.90 0.54 0.03 0.90 0.03 TO 41.35 1.17 7.99 0.28 8.53 0.09 0.36 0.03 0.06 0.03 0.06 0.03 0.06 0.03 0.30 0.04 0.40 0.06 0.41 0.05 0.41 0.05 1.69 0.17 TO TO 8.65 0.22 0.34 0.04 0.07 0.03 0.07 0.03 0.07 0.03

27 27

10 10

✗ ✗

48.84 3.23 TO 64.21 3.73 410.01 0.38

49 10 10 7 47 47 43 43 39 39

28 7 7 4 26 26 21 21 19 19

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

TO 37.25 0.15 0.08 0.03 0.08 0.03 0.08 0.03 0.08 0.03 0.07 0.03 0.07 0.03 TO 80.60 0.19 TO - 236.44 0.22 11.52 0.32 1.28 0.04 1138.11 31.25 5.47 0.07 334.97 13.89 2.27 0.04 239.67 13.16 3.66 0.04

TACO: A Toolsuite for the Verification of Threshold Automata

11

outperform SMT and ByMC, with ACS generally being more efficient on small benchmarks and ZCS better on larger ones. Analysis: ETA Benchmarks. The ETA benchmarks are only evaluated on the ZCS and ACS model checkers, as the other approaches do not support extended threshold automata. The ZCS approach outperforms the ACS model checker on all safe ETA benchmarks except for the three smallest benchmarks, where both tie. Closer analysis indicates that the ACS approach takes significantly longer to construct the error graph on larger examples, suggesting that 01-abstraction paired with the efficient representation as BDDs is more efficient than the WSTS approach for large benchmarks. On unsafe benchmarks with limited error graph size, the ACS approach finds counterexamples faster. This is most likely because the error graph exploration of the ACS model checker uses depth-first instead of breadth-first search, finding a concrete counterexample much quicker. In summary, for larger examples, the ZCS model checker outperforms the ACS model checker, whereas on small unsafe ones, the ACS model checker can be significantly faster.

6

Conclusion

We introduced Taco, a modular, openly available, well-documented toolsuite for the verification of threshold-based distributed algorithms. Our implementation includes multiple model checkers for decidable fragments, as well as semi-decision procedures that extend beyond these fragments. In our experimental evaluation, Taco significantly outperformed the only other existing but no longer maintained tool, ByMC. As future work, we plan to add support for liveness verification, including the development of novel algorithms that reduce the proof burden on protocol designers compared to the existing approaches. On the user experience side, we are working on an automatic translation from pseudocode or domain-specific languages to threshold automata, as well as a graphical user interface. These new interfaces should help to make Taco more accessible for non-expert users. Acknowledgments. T. Baumeister and P. Eichler carried out this work as members of the Saarbrücken Graduate School of Computer Science. This research was funded in whole or in part by the German Research Foundation (DFG) grant 513487900, by the German Research Foundation (DFG) grant 497132954 and the Luxembourg National Research Fund (FNR) grant C22/IS/17432184. For the purpose of open access, and in fulfilment of the obligations arising from the grant agreement, the author has applied a Creative Commons Attribution 4.0 International (CC BY 4.0) license to any Author Accepted Manuscript version arising from this submission. Disclosure of Interests. The authors have no competing interests to declare that are relevant to the content of this article.

12

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

Data Availability The benchmarks, evaluation scripts, source code of Taco and container images used to obtain the results presented in Section 5 and Section C are available on Zenodo under Apache 2.0 license at https://doi.org/10.5281/zenodo. 19659446. Additionally, the source code and documentation of Taco is publicly available on GitHub at https://github.com/cispa/TACO and the documentation is also hosted on the tool website https://taco-mc.dev.

References 1. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. pp. 313–321. IEEE Computer Society (1996). https://doi.org/10.1109/LICS.1996. 561359 2. Balasubramanian, A.R.: Source Code: Complexity of Verification and Synthesis of Threshold Automata, A. R. Balasubramanian, J. Esparza, M. Lazic; ATVA20. https://github.com/arbalan96/thr_aut_SMT (2025), [Online (GitHub); accessed 22-April-2026] 3. Balasubramanian, A.R., Esparza, J., Lazic, M.: Complexity of verification and synthesis of threshold automata. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12302, pp. 144–160. Springer (2020). https://doi.org/10. 1007/978-3-030-59152-6_8 4. Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrialstrength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 415–442. Springer (2022). https://doi.org/10.1007/978-3-030-99524-9_24 5. Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK). vol. 13, p. 14 (2010), https://smt-lib.org/papers/ smt-lib-reference-v2.0-r10.12.21.pdf 6. Baumeister, T., Eichler, P., Jacobs, S., Sakr, M., Völp, M.: Parameterized verification of round-based distributed algorithms via extended threshold automata. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14933, pp. 638–657. Springer (2024). https://doi.org/10.1007/978-3-031-71162-6_33 7. Bertrand, N., Gramoli, V., Konnov, I., Lazic, M., Tholoniat, P., Widder, J.: Brief announcement: Holistic verification of blockchain consensus pp. 424–426 (2022). https://doi.org/10.1145/3519270.3538468 8. Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: Fokkink, W.J., van Glabbeek, R.

TACO: A Toolsuite for the Verification of Threshold Automata

13

(eds.) 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, The Netherlands, August 27-30, 2019. LIPIcs, vol. 140, pp. 33:1–33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://doi.org/10. 4230/LIPICS.CONCUR.2019.33 9. Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824–840 (1985). https://doi.org/10.1145/4221.214134 10. Brasileiro, F.V., Greve, F., Mostéfaoui, A., Raynal, M.: Consensus in one communication step. In: Malyshkin, V.E. (ed.) Parallel Computing Technologies, 6th International Conference, PaCT 2001, Novosibirsk, Russia, September 3-7, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2127, pp. 42–50. Springer (2001). https://doi.org/10.1007/3-540-44743-1_4 11. Crain, T., Natoli, C., Gramoli, V.: Red belly: A secure, fair and scalable open blockchain. In: 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021. pp. 466–483. IEEE (2021). https://doi. org/10.1109/SP40001.2021.00087 12. Eichler, P., Baumeister, T., Sakr, M., Dowlati, M.K., Völp, M., Jacobs, S.: TACO - Artifact Package. https://doi.org/10.5281/zenodo.19659446 (2026), [Online (Zenodo); accessed 22-April-2026] 13. Eichler, P., Jacobs, S., Weil-Kennedy, C.: Parameterized verification of systems with precise (0,1)-counter abstraction. In: Krishna, S., Sankaranarayanan, S., Trivedi, A. (eds.) Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Denver, CO, USA, January 20-21, 2025, Proceedings, Part I. Lecture Notes in Computer Science, vol. 15529, pp. 101–124. Springer (2025). https://doi.org/10.1007/978-3-031-82700-6_5 14. Finkel, A.: A generalization of the procedure of karp and miller to well structured transition systems. In: Ottmann, T. (ed.) Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings. Lecture Notes in Computer Science, vol. 267, pp. 499–508. Springer (1987). https://doi.org/10.1007/3-540-18088-5_43 15. Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83–92 (2017). https://doi.org/10.1145/3068608 16. Husung, N., Dubslaff, C., Hermanns, H., Köhl, M.A.: OxiDD: A safe, concurrent, modular, and performant decision diagram framework in Rust. In: Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’24) (2024). https://doi.org/10.1007/ 978-3-031-57256-2_13 17. Jaber, N., Wagner, C., Jacobs, S., Kulkarni, M., Samanta, R.: Quicksilver: modeling and parameterized verification for distributed agreement-based systems. Proc. ACM Program. Lang. 5(OOPSLA), 1–31 (2021). https://doi.org/10. 1145/3485534 18. John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp. 201–209. IEEE (2013). https://doi.org/10.1109/FMCAD.2013.6679411 19. John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Bartocci, E., Ramakrishnan, C.R. (eds.) Model Checking Software - 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7976, pp. 209–226. Springer (2013). https://doi.org/10.1007/ 978-3-642-39176-7_14

14

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

20. Jr., S.B.A.: Binary decision diagrams. IEEE Trans. Computers 27(6), 509–516 (1978). https://doi.org/10.1109/TC.1978.1675141 21. Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. Int. J. Softw. Tools Technol. Transf. 2(4), 328–342 (2000). https://doi.org/10.1007/S100090050040 22. Konnov, I.: ByMC - GitHub repository. https://github.com/konnov/bymc/tree/ 266366f738bce9dbd5d04336fd9123d85ae2bca1 (2012-2023), [Online (GitHub); accessed 7-January-2026] 23. Konnov, I.: fault-tolerant-benchmarks GitHub repository. https://github.com/konnov/fault-tolerant-benchmarks/tree/ c9e8de463e0a6bc378d8f05270ffc7db043e79e6 (2014-2020), [Online (GitHub); accessed 7-January-2026] 24. Konnov, I., Lazic, M., Stoilkovska, I., Widder, J.: Survey on parameterized verification with threshold automata and the byzantine model checker. Log. Methods Comput. Sci. 19(1) (2023). https://doi.org/10.46298/LMCS-19(1:5)2023 25. Konnov, I., Lazic, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. CoRR abs/1608.05327 (2016). https://doi.org/10.1145/3009837.3009860 26. Konnov, I., Lazic, M., Veith, H., Widder, J.: Para2 : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods Syst. Des. 51(2), 270–307 (2017). https://doi.org/10. 1007/S10703-017-0297-4 27. Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8704, pp. 125–140. Springer (2014). https://doi.org/10. 1007/978-3-662-44584-6_10 28. Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9206, pp. 85–102. Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_6 29. Konnov, I., Widder, J.: Bymc: Byzantine model checker. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III. Lecture Notes in Computer Science, vol. 11246, pp. 327–342. Springer (2018). https://doi.org/10.1007/ 978-3-030-03424-5_22 30. Konnov, I.V., Lazic, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 719–734. ACM (2017). https://doi.org/10.1145/3009837. 3009860 31. Konnov, I.V., Veith, H., Widder, J.: What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: Mazzara, M., Voronkov, A. (eds.) Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopo-

TACO: A Toolsuite for the Verification of Threshold Automata

15

lis, Russia, August 24-27, 2015, Revised Selected Papers. Lecture Notes in Computer Science, vol. 9609, pp. 6–21. Springer (2015). https://doi.org/10.1007/ 978-3-319-41579-6_2 32. Konnov, I.V., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Inf. Comput. 252, 95–109 (2017). https://doi.org/10.1016/J.IC.2016.03.006 33. Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: All flavors of threshold automata. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. LIPIcs, vol. 118, pp. 19:1–19:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018). https://doi.org/10.4230/LIPICS.CONCUR.2018.19 34. Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002), http://research.microsoft. com/users/lamport/tla/book.html 35. Lamport, L., Shostak, R.E., Pease, M.C.: The byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382–401 (1982). https://doi.org/10.1145/ 357172.357176 36. McMillan, K.L., Padon, O.: Ivy: A multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 190–202. Springer (2020). https://doi.org/10.1007/978-3-030-53291-8_12 37. Mostéfaoui, A., Mourgaya, E., Parvédy, P.R., Raynal, M.: Evaluating the conditionbased approach to solve consensus. In: 2003 International Conference on Dependable Systems and Networks (DSN 2003), 22-25 June 2003, San Francisco, CA, USA, Proceedings. pp. 541–550. IEEE Computer Society (2003). https: //doi.org/10.1109/DSN.2003.1209964 38. de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008). https://doi.org/10.1007/ 978-3-540-78800-3_24 39. Pîrlea, G., Gladshtein, V., Kinsbruner, E., Zhao, Q., Sergey, I.: Veil: A framework for automated and interactive verification of transition systems. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III. Lecture Notes in Computer Science, vol. 15933, pp. 26–41. Springer (2025). https://doi.org/ 10.1007/978-3-031-98682-6_2 40. Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2404, pp. 107–122. Springer (2002). https://doi.org/10.1007/3-540-45657-0_9 41. Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal specification, verification, and implementation of fault-tolerant systems using eventml. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015). https://doi.org/10.14279/ TUJ.ECEASST.72.1013

16

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

42. Somenzi, F.: Cudd: Cu decision diagram package. Public Software, University of Colorado (1997), online (GitHub Mirror); accessed 16-January-2026; https:// github.com/cuddorg/cudd/tree/f54f533303640afd5dbe47a05ebeabb3066f2a25 43. Somenzi, F.: Efficient manipulation of decision diagrams. Int. J. Softw. Tools Technol. Transf. 3(2), 171–181 (2001). https://doi.org/10.1007/S100090100042 44. Srikanth, T.K., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Comput. 2(2), 80–94 (1987). https://doi. org/10.1007/BF01667080 45. Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II. Lecture Notes in Computer Science, vol. 11428, pp. 357–374. Springer (2019). https://doi.org/10. 1007/978-3-030-17465-1_20 46. Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Eliminating message counters in threshold automata. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12302, pp. 196–212. Springer (2020). https://doi.org/10.1007/ 978-3-030-59152-6_11 47. Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Eliminating message counters in synchronous threshold automata. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12597, pp. 196–218. Springer (2021). https://doi.org/10.1007/978-3-030-67067-2_10 48. Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. Int. J. Softw. Tools Technol. Transf. 24(1), 33–48 (2022). https://doi.org/10.1007/S10009-021-00637-9 49. Thomas, B., Sankur, O.: Pylta: A verification tool for parameterized distributed algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13994, pp. 28–35. Springer (2023). https://doi.org/10.1007/978-3-031-30820-8_4 50. Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. pp. 357–368. ACM (2015). https://doi.org/10.1145/2737924.2737958

TACO: A Toolsuite for the Verification of Threshold Automata

A

17

Modeling Example: Reliable Broadcast Protocol

Algorithm 2 1: int v = input({0, 1}) 2: bool accept = false; 3: while (!accept) do 4: if (v == 1) 5: broadcast ⟨ECHO⟩; 6: receive messages from all; 7: if received ⟨ECHO⟩ ≥ t + 1 8: v = 1; 9: if received ⟨ECHO⟩ ≥ n − t 10: accept = true;

rec++ V0

RV0 rec = 0 rec ≥ φ3 ∧ nsnt < φ1 nsnt := 0; rec := 0

nsnt ≥ φ1

nsnt ≥ φ2 SE

φ2 < nt 0 s = n ∧ ec : φ3 ; r ≥ =0 c : 0 re nt c= ns re

V1 n ns

t

; ++

AC

+ c+

re

φ1 = t − f + 1 φ2 = n − t − f φ3 = n − f

Figure 4: Pseudocode of a reliable Figure 5: TA of the algorithm in Fig. 1. broadcast protocol.

Example 2. Fig. 4 shows the pseudocode of a reliable broadcast, inspired by [44]. In every round, processes with input v = 1 will broadcast a message, then processes with v = 0 will set v = 1 if they received at least t + 1 messages, and finally processes set accept = true if at least n − t messages have been received. If accept is false at the end of the round, a new round starts. Fig. 5 depicts a TA for this algorithm, with L = {V0 , V1 , RV0 , SE, AC}, I = {V0 , V1 }, Γ = {nsnt, rec}, Π = {n, t, f }, and RC = n > 3t ∧ t ≥ f ≥ 0. A process in V1 has input 1 and can move freely (there is no guard) to SE, incrementing both variables nsnt and rec to simulate lines 4–6 of the algorithm. A process in location V0 has input 0 and can move to RV0 , incrementing rec to simulate line 6 (but not line 5, since the condition in line 4 evaluates to false). From RV0 , a process can move to SE if nsnt ≥ φ1 , simulating lines 7-8. Processes that started with v = 1 already are in SE, corresponding to the fact that v = 1 is not changed in line 8. Note that instead of being t + 1, φ1 is chosen as t + 1 − f . This prevents processes from making a transition based on messages from faulty processes, hence the TA represents the behavior of correct processes and f the effect of faulty processes on correct ones. For more details on the role of f , see [46]. Processes in SE can move to AC if nsnt ≥ φ2 , simulating lines 9-10. If nsnt < φ2 and rec ≥ φ3 (this constraint corresponds to waiting long enough for all non-faulty processes to receive all messages), the condition in line 9 was not satisfied and a new iteration of the while-loop is started by moving back from SE to V1 . The first process taking this transition will reset nsnt and rec, the others

18

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

take the transition that does not change any variables. Similarly, processes in RV0 will move to V0 to start the new round. The RC condition is critical here to ensure fault-tolerance: if f > t, then AC will be reachable even if all processes start in V0 , violating the validity property.

B

Input Formats

This section presents the threshold automaton from Fig. 2 and Fig. 5 into the two input formats supported by Taco. B.1

.ta Input

ta SRB { shared nsnt, rec; 3 parameters n, t, f; 4 assumptions (3) { n > 3 * t; t >= f; f >= 0; } 5 locations (5) { V0: [0]; V1: [1]; RV0: [2]; SE: [3]; AC: [4]; } 6 inits(6) { nsnt == 0; rec == 0; RV0 == 0; SE == 0; AC == 0; 7 V1 + V0 == n - f; /* n-f correct processes in initial states */ } 8 rules (8) { 9 0: V0 -> RV0 when (true) do { rec’ := rec + 1; }; 10 1: V1 -> SE when (true) 11 do { nsnt’ := nsnt + 1; rec’ := rec + 1; }; 12 2: RV0 -> SE when (nsnt >= t + 1 - f) do {}; 13 3: SE -> AC when (nsnt >= n - t - f) do {}; 14 4: RV0 -> V0 when ((rec >= n - f) && (nsnt > t + 1 - f)) do {}; 15 5: RV0 -> V0 when (rec == 0) do {}; 16 6: SE -> V1 when ((rec >= n - f) && (nsnt > t + 1 - f)) 17 do { rec’ := 0; nsnt’ := 0; }; 18 7: SE -> V1 when (rec == 0) do {}; 19 } 20 specifications (1) { validity: V1 == 0 -> [](AC == 0); } 21 } 1 2

Listing 2: TA of Fig. 5 encoded as a .ta file

B.2

TLA+ Input

---------------------------- MODULE ALG1--------------------------EXTENDS Integers, FiniteSets 3 CONSTANT Processes, NbOfCorrProc, n, t 1 2

4 5 6

ASSUME NbOfCorrProc = n /\ n > 3 * t

7 8

VARIABLES ProcessesLocations, x0, x1

9 10 11

TypeOk == x0 \in Nat /\ x1 \in Nat /\ ProcessesLocations \in [Processes -> {"V0", "V1", "D0", "D1", "WAIT"}]

12

Init == ProcessesLocations \in [Processes -> {"V0", "V1"}] /\ x0 = 0 /\ x1 = 0 15 -----------------------------------------------------------------13 14

TACO: A Toolsuite for the Verification of Threshold Automata Rule0(p) == ProcessesLocations[p] = "V0" /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "WAIT"] 18 /\ x0’ = x0 + 1 19 /\ UNCHANGED <<x1>> 20 -----------------------------------------------------------------21 Rule1(p) == ProcessesLocations[p] = "V1" 22 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "WAIT"] 23 /\ x1’ = x1 + 1 24 /\ UNCHANGED <<x0>> 25 -----------------------------------------------------------------26 Rule2(p) == ProcessesLocations[p] = "WAIT" 27 /\ x0 >= n - t 28 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "D0"] 29 /\ UNCHANGED <<x0,x1>> 30 -----------------------------------------------------------------31 Rule3(p) == ProcessesLocations[p] = "WAIT" 32 /\ x1 >= n - t 33 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "D1"] 34 /\ UNCHANGED <<x0,x1>> 35 -----------------------------------------------------------------36 Next == \E p \in Processes: Rule0(p) \/ Rule1(p) \/ Rule2(p) \/ Rule3(p) 16 17

37

Spec == Init /\ [][Next]_<< ProcessesLocations,x0,x1 >> -----------------------------------------------------------------40 NumInD0 == Cardinality({p \in Processes : ProcessesLocations[p] = "D0"}) 41 NumInD1 == Cardinality({p \in Processes : ProcessesLocations[p] = "D1"}) 38 39

42 43

cor == []( ( NumInD0 > 0 / NumInD1 > 0))

Listing 3: TLA+ specification of Fig. 2 ---------------------------- MODULE SRB --------------------------EXTENDS Integers, FiniteSets 3 CONSTANT Processes, NbOfCorrProc, N, T, F 1 2

4

ASSUME NbOfCorrProc = N - F /\ N > 3 * T 7 /\ T >= F 8 /\ F >= 0 5 6

9 10

VARIABLES ProcessesLocations, nsnt, rDone

11 12 13

TypeOk == rDone \in Nat /\ nsnt \in Nat /\ ProcessesLocations \in [Processes -> {"V0", "V1", "SE", "AC", "fRound"}]

14

Init == ProcessesLocations \in [Processes -> {"V0"}] /\ nsnt = 0 /\ rDone = 0 17 -----------------------------------------------------------------18 Rule0(p) == ProcessesLocations[p] = "V0" 19 /\ nsnt >= T - F + 1 20 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "SE"] 21 /\ nsnt’ = nsnt + 1 22 /\ UNCHANGED <<rDone>> 23 -----------------------------------------------------------------24 Rule1(p) == ProcessesLocations[p] = "V0" 25 /\ nsnt >= N - T - F 26 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "AC"] 27 /\ UNCHANGED <<nsnt, rDone>> 28 -----------------------------------------------------------------15 16

19

20

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

Rule2(p) == ProcessesLocations[p] = "V1" /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "SE"] 31 /\ nsnt’ = nsnt + 1 32 /\ UNCHANGED <<rDone>> 33 -----------------------------------------------------------------34 Rule3(p) == ProcessesLocations[p] = "V1" 35 /\ nsnt >= N - T - F 36 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "AC"] 37 /\ UNCHANGED <<nsnt, rDone>> 38 -----------------------------------------------------------------39 Rule4(p) == ProcessesLocations[p] = "SE" 40 /\ nsnt >= N - T - F 41 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "AC"] 42 /\ UNCHANGED <<nsnt, rDone>> 43 -----------------------------------------------------------------44 Rule5(p) == ProcessesLocations[p] = "AC" 45 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "fRound"] 46 /\ rDone’ = rDone + 1 47 /\ UNCHANGED <<nsnt>> 48 -----------------------------------------------------------------49 Rule6(p) == ProcessesLocations[p] = "fRound" 50 /\ rDone >= N - F 51 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "V1"] 52 /\ nsnt’ = 0 53 /\ rDone’ = 0 54 -----------------------------------------------------------------55 Rule7(p) == ProcessesLocations[p] = "fRound" 56 /\ rDone > 1 57 /\ ProcessesLocations’ = [ProcessesLocations EXCEPT ![p] = "V1"] 58 /\ UNCHANGED <<nsnt, rDone>> 59 -----------------------------------------------------------------60 Next == \E p \in Processes: Rule0(p) \/ Rule1(p) \/ Rule2(p) \/ Rule3(p) 61 \/ Rule4(p) \/ Rule5(p) \/ Rule6(p) \/ Rule7(p) 29 30

62 63 64

Spec == Init /\ [][Next]_<< ProcessesLocations,nsnt,rDone >> ------------------------------------------------------------------

65 66 67

NumInV1 == Cardinality({p \in Processes : ProcessesLocations[p] = "V1"}) NumInAC == Cardinality({p \in Processes : ProcessesLocations[p] = "AC"})

68 69 70

validity1 == NumInV1 = 0 => [](NumInAC = 0)

Listing 4: TLA+ specification of Fig. 5

TACO: A Toolsuite for the Verification of Threshold Automata

C

21

Extended Evaluation

This section extends the evaluation in Section 5. We provide more details on the setup, present additional results on an extended benchmark set and evaluate additional modes of Taco and ByMC. C.1

Evaluation Environment

The evaluation was conducted on Dell R6525 nodes equipped with 2x AMD Epyc 7773x with 128 physical cores + 128 Simultaneous Multithreading and 2TB of RAM. The benchmarking scripts always report the elapsed real-time and maximal resident set size as reported by the GNU time command. All model checkers were set to run in their sequential modes. Additionally, we used the timeout command to stop benchmark runs that exceed the maximal runtime. During the evaluation, the timeout was set to 20min, and a memory limit (on the virtual memory consumption) of 2071552MB was set using ulimit -SHv. ByMC Container. For benchmarking ByMC, we created a container image of the tool from a custom Dockerfile9 . Alternatively, a link to a virtual machine (VM) is provided in the ByMC repository10 . We chose to create our own Dockerfile for two main reasons: – Newer dependencies. To reduce the impact of optimizations to external components (like SMT solvers), we included the most recent version for which the build of ByMC would succeed without modification to the source code. The VM comes, for example, with Z3 [38] 4.4.1 (released Oct 5th 2015 on Github11 ) installed, which is three years older than the version included in the container image, which is 4.7.1 (released May 23rd 2018 on GitHub12 ). Note that the Z3 version in the VM is surprising since the ByMC tool paper [29] explicitly reports that the benchmark results were obtained with Z3 version 4.6.0. Still, ByMC has not been maintained for years, and many dependencies cannot be easily upgraded to up-to-date versions. – Cumbersome benchmark process. The ByMC VM is based on Debian 9 and in our testing, the guest additions did not work properly. This made automation of the rather large set of benchmarks difficult. Any errors encountered during evaluation, like, for example, the syntax errors reported in Section 5 and the errors described in the next section, were reproducible in the VM. 9

Available in the reproduction package [12] or on GitHub https://github. com/pleich/bymc/blob/0bca349cc7d3e8511f649726be4ce990f458c00a/bymc/ Dockerfile (accessed 16-01-2026) 10 Link available in top level README section “Installation” in the ByMC GitHub repository [22] 11 https://github.com/Z3Prover/z3/releases/tag/z3-4.4.1, accessed 16-01-2026 12 https://github.com/Z3Prover/z3/releases/tag/z3-4.7.1, accessed 16-01-2026

22

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

C.2

ByMC Additional Modes

ByMC, as provided in the VM and in the Dockerfile, has support for multiple modes. The default one is ltl (implementing the methods described in [25, 30]), which we used for the evaluation in Section 5. Besides the ltl mode, ByMC implements a mode ltl-mpi (corresponding to [29]) and a mode cav15 (corresponding to [26, 28]). The cav15 mode is intended for verification of safety properties (specifically reachability as defined in [28]) and should be compatible with our set of benchmarks. However, as mentioned in Section 5, the latter mode was excluded from the evaluation as it reports (invalid) counterexamples to safe benchmarks (which are also reported as safe by the ltl mode and Taco). Specifically, this mode reports counterexamples for three hand-coded benchmarks: bosco.ta, c1cs.ta and cf1s.ta (from the fault-tolerant-benchmarks repository in folder isola18/ta [23]). For example, for the bosco.ta ByMC reports the counterexample depicted in Fig. 6. This counterexample does not correspond to a valid run in the threshold automaton.

Figure 6: Screenshot of the counterexample reported ByMC in the cav15 mode on isola18/bosco.ta (running in the VM provided by the ByMC authors [22])

Because of these correctness issues, we did not include this mode in the evaluation in Section 5. However, we still include performance result in Table 2. Older ByMC Modes. In addition to the modes mentioned above, at some point ByMC supported additional (older) decision procedures described in [18, 24, 26–28, 31, 32] that used a refinement loop and counter abstraction combined with different model checkers. However, as mentioned in [26, 28], these older methods did not scale to larger examples. Additionally, they are no longer executable inside the ByMC VM and we did not manage to compile the required dependencies of these modules (which are also marked as legacy in the ByMC repository [22]). Therefore, we do not report performance results for these modes.

TACO: A Toolsuite for the Verification of Threshold Automata

C.3

23

Origin of the Benchmarks

All “ByMC” benchmarks appearing in Table 2 were directly taken or generated from the fault-tolerant-benchmarks GitHub repository [23]. These benchmarks originally appeared in [8, 18, 25–30, 32]. For benchmarks in the Promela format, ByMC was used to first create the threshold automata in the .ta format (via data abstraction [18, 26–28, 32]). The benchmarking was then conducted directly on the .ta files. When benchmarking ByMC, all liveness properties were removed from the files. The .ta files used during the evaluation are included in the reproduction package [12] (and in the TACO GitHub repository 13 ). The “RedBelly” and “King Consensus” benchmarks first appeared in [6] and are also available in the TACO GitHub repository and in the reproduction package [12]. Selection of Benchmarks in Section 5. Note that many benchmarks in this full set of benchmarks are quite similar. For example, the README for the benchmarks ByMC POPL17 Promela states that they are an extension of the benchmark set ByMC CAV15 Promela with some corrections to correct for liveness properties. This made it difficult to select a representative set. Threfore, for the ByMC benchmarks in Section 5, we chose to use the same benchmark set as in [29] and [3]. We believe that the files named “cc” correspond to the benchmarks called “cbc” in [29], and we could not obtain the two additional “bosco” cases mentioned there. Note that they are also missing from [3]. C.4

Extended Evaluation Results

The execution times and memory consumption of ByMC in the default (ltl) and in the cav15 mode, as well as the execution times for all of Taco’s model checkers with Z3 [38] and with CVC5 [4] as SMT solver are provided in Table 2. Analysis of MTA Benchmarks Table 2. Out of the 86 benchmarks, one of Taco’s model checkers outperformed ByMC (in either mode) in 59 cases, 64 if we exclude the cav15 mode. Moreover, there is no benchmark that can be solved by ByMC but is not solved by any model checker of Taco within the 20min timeout. In contrast, there are eight benchmarks (not counting the cases where ByMC returned errors), which none of the modes of ByMC solved within the time limit. Otherwise, the extended evaluation confirms the observations in Section 5. For unsafe benchmarks, usually the SMT model checker performs best, with some exceptions where the ZCS model checker is faster. On safe benchmarks, ACS and ZCS are often faster than the SMT model checker. Random19 Benchmarks. Note that most of the benchmarks where ByMC outperforms Taco stem from the ByMC Random19 [8] set of benchmarks. These 13

https://github.com/cispa/TACO

24

P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

benchmarks have two properties that make them particularly challenging for our model checkers. On the one hand, the SMT model checker does not perform well because these benchmarks have a high number of potential context switches that could occur on an error path (denoted as the number k in [3]). Every additional context switch adds variables to the SMT query and increases its length. On the other hand, these examples also have many potential abstract interval orderings. As the ZCS and ACS model checker have to check reachability in every interval order, resulting in many individual model checker runs (for more details, refer to [6]). Most likely the performance for these benchmarks could be further improved by developing a preprocessor tailored towards these examples. CVC5 vs. Z3. When comparing the performance of the SMT model checker when paired with CVC5 [4] and Z3 [38], we observe that on larger examples, like ByMC CAV15 Promela or ByMC ISOLA18 Promela, the model checker paired with CVC5 mostly outperforms Z3 while usually consuming less memory. CVC5 seems to scale better to the large SMT queries generated by the SMT model checker for these examples. Consequently, our experiments suggest that the SMT model checker should be paired with CVC5 when verifying large TA. On smaller benchmarks, like the benchmarks in the ByMC Handcoded ISOLA18 set, Z3 is in most cases faster than CVC5. For the “bosco” case in particular, the SMT model checker paired with Z3 is around four times faster. Next, we compare the runtime of the ACS and ZCS model checker when paired with different SMT solvers. It is important to note that the SMT queries can significantly differ from the queries of the SMT model checker. Generally, there will be more queries but with significantly fewer variables and clauses. This is becuase the abstract error graphs already provide information on which rules can be applied when checking for spurious counterexamples. However, there might be many paths that need to be checked. Additionally, both ACS and ZCS rely on constructing all potential orders between abstract interval borders. This step additionally requires many small SMT queries. Here, Z3 almost always outperforms the same model checker when paired with CVC5. Most likely because it is optimized to solve small queries fast. Therefore, it is generally advisable to select Z3 for these model checkers. Examples not Supported by ACS. Table 2 contains two examples, “toy” and “nbacg-asyn-guer01-nbac”, which are not supported by the ACS model checker. These examples fullfill the conditions mentioned in Section 3, i.e., they contain properties that require some locations in a target configuration to be empty. However, the wqo used in the ACS model checker is not precise for locations for these cases [6]. This could potentially be addressed in the future by utilizing a different wqo, but would require additional theory. Note that such a wqo will also result in larger error graphs. As properties containing such constraints rarely occur, the ACS model checker has been implemented with the wqo from [6]. The analysis of the benchmark results for the ETA benchmarks can be found in Section 5 as the complete list of ETA benchmarks has already been included in Table 1.

✓ ✗ ✗ ✗ ✓ ✗ ✗ ? ✓

✓ ✓ ✗ ✗ ✗ ✗ ✗ ✗ ? ✗ ? ? ✓ ✓ ✓ ✓ ✗ ✗ ✗ ✓

✓ ✗ ✗ ✓ ✓ ? ✓

|L| |R| safe?

TA

MTA Benchmarks ByMC CONCUR14 Promela [27, 32] asyn-byzagreement0 37 202 asyn-ray97-nbac-clean 109 1831 asyn-ray97-nbac 77 1431 bcast-byz 7 21 bcast-folklore-crash 6 15 cond-consensus2 115 991 toy 5 8 ByMC CAV15 Promela [26, 28] aba-asyn-byzagreement0_case1 37 202 aba-asyn-byzagreement0_case2 61 425 bosco_case1 58 394 bosco_case2 88 752 bosco_case3 62 442 c1cs_case1 125 2050 c1cs_case2 84 964 c1cs_case3 129 2194 cbc-cond-consensus2_case1 74 425 cbc-cond-consensus2_case2 40 169 cbc-cond-consensus2_case3 115 991 cbc-cond-consensus2_case4 71 466 cf1s-consensus-folklore-onestep_case1 57 438 cf1s-consensus-folklore-onestep_case2 57 438 cf1s-consensus-folklore-onestep_case3 98 1194 frb-bcast-folklore-crash 6 13 nbac-asyn-ray97-nbac 77 1431 nbacc-asyn-ray97-nbac-clean 109 1831 nbacg-asyn-guer01-nbac 24 64 strb-bcast-byz 7 21 ByMC POPL17 Promela [25, 30] asyn-byzagreement0 37 202 asyn-guer01-nbac 24 64 asyn-ray97-nbac-clean 78 1431 asyn-ray97-nbac 77 1031 bcast-byz 7 21 bosco 28 152 c1cs 101 1285 cond-consensus2 164 2064 consensus-folklore-onestep 41 280

Benchmark

Err 6.75 0.42 4.11 0.25 0.31 0.03 0.29 0.03 Err 0.29 0.03

cav15 time RSS

00.77 0.10 TO TO 0.13 0.05 0.10 0.05 TO 0.12 0.05

TACO ACS CVC5 Z3 time RSS time RSS

1.40 0.04 21.25 0.30 15.70 0.27 0.07 0.03 0.06 0.03 TO 0.22 0.05

ZCS CVC5 Z3 time RSS time RSS

2.27 0.27 1.84 0.05 1.68 0.03 1.67 0.05 TO TO TO 30.55 0.25 TO TO TO 20.36 0.27 0.08 0.03 0.11 0.05 0.06 0.03 0.12 0.05 0.07 0.03 0.10 0.05 0.05 0.03 0.10 0.05 TO TO TO TO 0.07 0.03 Unsup. - Unsup. 0.36 0.05

SMT CVC5 Z3 time RSS time RSS

15.21 0.06 3.75 0.06 0.33 0.04 0.33 0.03 191.96 3.51 3.82 0.36 1.71 0.17 2.23 0.16 0.33 0.04 0.30 0.03 44.94 0.06 7.73 0.05 TO 503.44 0.47 Err Err 18.26 0.07 1.68 0.06

0.76 0.10 0.55 0.06 TO TO 0.13 0.05 5.58 0.11 82.32 2.02 TO 2.34 0.12

2.15 0.18 0.36 0.06 TO TO 0.07 0.03 7.85 0.09 TO TO 8.00 0.90

1.60 0.05 1.07 0.03 1.56 0.05 1.48 0.04 0.78 0.06 0.40 0.05 0.81 0.05 0.42 0.05 TO TO 18.15 0.18 22.53 0.22 TO TO 12.00 0.18 8.12 0.22 0.12 0.05 0.07 0.03 0.11 0.05 0.07 0.03 TO - 495.32 0.07 125.78 0.19 104.55 0.17 TO TO - 78.34 0.22 103.71 0.22 TO TO TO TO 0.54 0.05 0.46 0.03 0.61 0.05 0.70 0.03

15.23 0.06 3.77 0.07 0.73 0.10 4.65 0.47 1.78 0.05 2.12 0.03 1.34 0.05 1.53 0.04 289.05 0.11 61.89 0.14 3.51 0.29 29.26 1.84 21.37 0.08 21.40 0.09 17.29 0.14 17.49 0.15 228.10 0.10 25.92 0.15 75.17 0.22 69.57 0.91 TO TO TO TO TO - 488.24 0.50 988.40 0.82 TO TO TO TO TO 155.05 0.11 36.17 0.15 181.53 0.31 61.92 0.46 TO TO TO TO TO 991.92 0.87 428.99 8.42 TO TO TO - 945.44 0.33 820.44 0.30 TO 180.06 0.40 57.75 1.44 TO 111.97 0.86 261.23 0.72 75.75 0.19 71.97 0.21 TO TO 1006.74 19.72 TO TO TO TO TO Err Err TO TO TO TO TO TO Err Err 64.73 0.58 25.61 0.38 TO TO TO TO Err Err TO TO TO TO TO TO Err Err TO TO TO TO TO TO 29.64 0.09 2.73 0.08 5.04 0.19 14.37 0.93 0.98 0.05 0.89 0.03 1.19 0.05 1.14 0.04 172.04 0.14 7.43 0.11 5.33 0.23 13.38 0.50 1.26 0.05 1.21 0.05 4.02 0.05 3.65 0.04 TO 246.43 0.48 81.50 2.18 TO 33.33 0.59 29.36 0.59 26.23 0.15 47.45 0.20 0.36 0.04 0.29 0.03 0.11 0.05 0.07 0.03 0.11 0.05 0.06 0.03 0.11 0.05 0.06 0.03 3.10 0.25 4.08 0.26 TO TO TO TO 21.26 0.27 19.16 0.27 5.15 0.43 6.77 0.42 TO TO TO TO 65.94 0.30 32.41 0.30 0.31 0.04 0.32 0.03 0.57 0.06 0.43 0.06 Unsup. - Unsup. 0.76 0.05 0.56 0.05 0.35 0.04 0.31 0.03 0.12 0.05 0.05 0.03 0.12 0.05 0.06 0.03 0.12 0.05 0.07 0.03

Err 5.23 0.43 3.09 0.25 0.34 0.04 0.31 0.04 Err 0.28 0.04

ltl time RSS

ByMC

Table 2: Extended benchmark results for Taco and ByMC. Columns |L| and |R| give the number of locations and rules of the given TA. In column “safe?”, ✓ denotes that all checked properties hold, ✗ denotes that some property was violated, and ? that the result is unknown. Execution time (here elapsed wall clock time) is given in s, TO denotes a timeout after 20min. The fastest execution time per benchmark is highlighted in bold font. RSS columns give the maximal resident set size in GB. “Err” denotes that an error occurred, and “Unsup.” that the benchmark is not supported. Entries in red are benchmarks of ByMC in cav15 mode which reported invalid counterexamples (see Section C.2).

TACO: A Toolsuite for the Verification of Threshold Automata 25

TA ltl time RSS

cav15 time RSS

CVC5 time RSS

SMT

TACO ACS Z3 CVC5 Z3 time RSS time RSS time RSS

ZCS CVC5 Z3 time RSS time RSS

|L| |R| safe? ByMC Handcoded ISOLA18 [29] aba 5 10 ✓ 0.69 0.04 0.33 0.03 0.13 0.05 0.07 0.03 0.12 0.05 0.06 0.03 0.12 0.05 0.07 0.03 bcrb 5 13 ✓ 0.42 0.04 0.29 0.03 0.12 0.05 0.08 0.03 0.11 0.05 0.07 0.03 0.12 0.05 0.07 0.03 bosco 8 20 ✓ 139.33 0.07 18.22 0.04 4.39 0.06 1.03 0.04 TO - 117.29 0.04 TO - 160.34 0.05 c1cs 9 30 ✓ TO 44.72 0.23 1.72 0.07 0.72 0.05 6.15 0.11 1.68 0.03 53.62 0.05 29.25 0.05 cc 7 14 ✓ 0.40 0.04 0.30 0.03 0.54 0.06 0.26 0.04 TO TO TO TO cf1s 9 26 ✓ 397.75 0.10 0.44 0.04 0.33 0.06 0.22 0.04 0.32 0.05 0.17 0.03 0.51 0.05 0.28 0.05 nbacg 8 16 ✓ 0.36 0.04 0.29 0.03 0.41 0.05 0.24 0.05 0.51 0.05 0.24 0.05 0.70 0.05 0.41 0.05 nbacr 7 16 ✓ 0.31 0.04 0.27 0.03 0.11 0.05 0.08 0.05 0.13 0.05 0.08 0.05 0.16 0.05 0.11 0.05 strb 4 8 ✓ 0.26 0.04 0.29 0.03 0.10 0.05 0.06 0.03 0.10 0.05 0.06 0.03 0.10 0.05 0.04 0.03 ByMC ISOLA18 Promela [29] aba_case1 37 202 ✓ 15.19 0.06 3.75 0.07 0.94 0.11 2.08 0.17 1.72 0.05 1.19 0.03 1.47 0.05 1.43 0.04 aba_case2 61 425 ✓ 290.42 0.11 63.37 0.14 3.65 0.29 19.49 0.74 14.95 0.08 17.79 0.09 15.30 0.15 15.12 0.15 bosco_case1 28 152 ✗ 45.16 0.06 7.87 0.05 5.74 0.10 7.61 0.09 TO - 332.93 0.06 124.56 0.15 104.76 0.19 bosco_case2 40 242 ✗ 752.65 0.08 98.78 0.09 52.86 0.24 38.47 0.21 TO TO - 1178.32 0.30 TO bosco_case3 32 188 ✗ 52.14 0.06 9.98 0.06 7.24 0.11 13.30 0.12 TO - 982.39 0.10 156.98 0.17 117.45 0.17 c1cs_case1 101 1285 ✗ Err Err 85.32 2.02 TO TO TO 79.32 0.21 83.00 0.22 c1cs_case2 70 650 ✗ TO - 100.39 0.23 17.28 0.52 1164.87 14.06 TO - 102.70 0.41 27.09 0.15 26.23 0.15 c1cs_case3 101 1333 ✗ TO TO - 156.59 3.95 TO TO TO TO TO cc_case1 164 2064 ? Err Err TO TO TO TO TO TO cc_case2 73 470 ✗ Err Err TO - 1178.05 8.82 TO TO TO TO cc_case3 304 6928 ? Err Err TO TO TO TO TO TO cc_case4 161 2105 ? Err Err TO TO TO TO TO TO cf1s_case1 41 280 ✓ 18.31 0.07 1.66 0.06 2.42 0.12 8.22 0.90 0.54 0.05 0.43 0.03 0.59 0.05 0.59 0.03 cf1s_case2 41 280 ✓ 102.08 0.10 4.43 0.08 2.44 0.13 7.25 0.90 0.66 0.05 0.54 0.03 1.65 0.05 0.90 0.03 cf1s_case3 68 696 ✓ TO - 108.28 0.20 22.75 0.71 41.35 1.17 7.82 0.28 7.99 0.28 10.79 0.09 8.53 0.09 frb 7 14 ✓ 0.36 0.03 0.32 0.03 0.11 0.05 0.06 0.03 0.11 0.05 0.06 0.03 0.11 0.05 0.06 0.03 nbacg 24 64 ✗ 0.30 0.04 0.29 0.03 0.55 0.06 0.40 0.06 0.78 0.06 0.41 0.05 0.91 0.05 0.41 0.05 nbacr 77 1031 ✗ 1.69 0.17 2.19 0.16 TO TO TO TO 11.24 0.18 8.65 0.22 strb 7 21 ✓ 0.34 0.04 0.31 0.03 0.13 0.05 0.07 0.03 0.12 0.05 0.07 0.03 0.11 0.05 0.07 0.03

Benchmark

ByMC

26 P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

ByMC

0.96 0.04 TO TO TO TO TO

✓ ✓ ✓

-

-

-

-

TO TO 45.52 0.17 37.25 0.15 0.13 0.05 0.08 0.03 0.15 0.05 0.08 0.03 0.12 0.05 0.08 0.03 0.15 0.05 0.08 0.03 0.11 0.05 0.07 0.03 0.11 0.05 0.07 0.03 TO TO 43.08 0.17 80.60 0.19 TO TO - 145.23 0.21 236.44 0.22 16.31 0.38 11.52 0.32 1.32 0.05 1.28 0.04 736.52 24.97 1138.11 31.25 3.77 0.08 5.47 0.07 275.26 11.86 334.97 13.89 2.15 0.05 2.27 0.04 574.49 18.94 239.67 13.16 2.12 0.05 3.66 0.04

0.11 0.03 0.81 0.03 0.85 0.03

TO

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

0.19 0.05 0.90 0.05 1.16 0.05

TO

TO TO TO TO TO TO TO TO 14.72 0.12 16.59 0.12 TO TO TO TO TO TO TO TO TO TO TO TO TO TO 12.42 0.12 11.27 0.12 TO TO TO TO TO TO TO TO -

48.84 3.23 TO TO 64.21 3.73 693.24 0.38 410.01 0.38

0.09 0.03 7.18 0.82 58.47 3.44

891.86 0.19

TO TO TO TO TO TO TO TO TO TO TO TO TO TO TO TO TO

ZCS CVC5 Z3 time RSS time RSS

52.19 3.31 TO -

0.22 0.05 0.14 0.03 0.19 0.05 1.38 0.09 1.24 0.07 7.16 0.84 6.29 0.16 10.04 0.49 63.96 3.45

TO

TO TO TO TO TO TO TO TO TO TO TO TO TO TO TO TO TO

TACO ACS CVC5 Z3 time RSS time RSS

✗ ✗

-

0.74 0.05 0.33 0.03

✗ 1.89 0.06 0.75 0.06

0.65 0.04 0.30 0.03 4.56 0.08 1.93 0.07 0.43 0.04 0.33 0.03 5.98 0.08 1.59 0.05 0.93 0.05 0.33 0.04 12.61 0.10 3.60 0.07 0.83 0.05 0.33 0.03 6.31 0.10 3.62 0.10 39.36 0.10 0.84 0.05 68.77 0.26 32.10 0.23 1.01 0.05 0.31 0.03 61.13 0.15 9.65 0.13 0.40 0.04 0.29 0.03 17.79 0.11 2.71 0.07 TO TO - 49.34 0.18 1.18 0.10 TO TO - 39.95 0.11 9.00 0.09 0.40 0.04 0.36 0.03 4.93 0.08 1.31 0.05 0.80 0.05 0.32 0.04 10.58 0.10 3.21 0.07 0.71 0.05 0.31 0.03 4.77 0.08 2.44 0.07 30.60 0.09 0.79 0.05 35.19 0.25 21.48 0.23 0.94 0.05 0.32 0.03 51.76 0.20 5.79 0.10 0.35 0.04 0.31 0.03 14.64 0.11 1.96 0.06 TO TO - 24.62 0.17 1.48 0.10 TO TO - 32.49 0.10 6.31 0.08

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✗ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✗ ✓

SMT ltl cav15 CVC5 Z3 |L| |R| safe? time RSS time RSS time RSS time RSS TA

ByMC Random19 [8] ben-or 10 25 n-ben-or-byz 9 18 n-ben-or-nonclean 10 32 n-ben-or 10 27 n-kset 13 58 n-rabc-cr 11 31 n-rabc-s 10 21 n-rabc 14 28 n-rs-bosco 19 48 p-ben-or-byz 9 16 p-ben-or-nonclean 10 30 p-ben-or 10 25 p-kset 13 52 p-rabc-cr 11 29 p-rabc-s 10 19 p-rabc 14 28 p-rs-bosco 19 42 ByMC LMCS20 [24] tendermint-1round-safe 6 22 RedBelly small [6] rb-bc 10 19 rb-simple 19 33 rb 26 41 ETA Benchmarks King Consensus [6] phase-king-buggy 27 10 phase-king 27 10 RedBelly with resets [6] rb-2x_reset 49 28 rb-floodMin_V0 10 7 rb-floodMin_V1 10 7 rb-RelBrd_V1 7 4 rb-reset_V0 47 26 rb-reset_V1 47 26 rb-simple-2x_reset_V0 43 21 rb-simple-2x_reset_V1 43 21 rb-simple-reset_V0 39 19 rb-simple-reset_V1 39 19

Benchmark

TACO: A Toolsuite for the Verification of Threshold Automata 27