tikzLTS  tikzPath

11institutetext:  CISPA Helmholtz Center for Information Security, Germany
22institutetext: SnT, Luxembourg University

# Parameterized Verification of
Round-based Distributed Algorithms
via Extended Threshold Automata

Tom Baumeister 11 Paul Eichler 11 Swen Jacobs 11 Mouhammad Sakr 22 Marcus Völp
22

###### Abstract

Threshold automata are a computational model that has proven to be versatile
in modeling threshold-based distributed algorithms and enabling their
completely automatic parameterized verification. We present novel techniques
for the verification of threshold automata, based on well-structured
transition systems, that allow us to extend the expressiveness of both the
computational model and the specifications that can be verified. In
particular, we extend the model to allow decrements and resets of shared
variables, possibly on cycles, and the specifications to general coverability.
While these extensions of the model in general lead to undecidability, our
algorithms provide a semi-decision procedure. We demonstrate the benefit of
our extensions by showing that we can model complex round-based algorithms
such as the phase king consensus algorithm and the Red Belly Blockchain
protocol (published in 2019), and verify them fully automatically for the
first time.

##  1 Introduction

Due to the increasing prevalence and importance of distributed systems in our
society, ensuring reliability and correctness of these systems has become
paramount. Computer-aided verification of distributed protocols and algorithms
has been a very active research area in recent years [34, 51, 59, 48, 36]. To
be practical, models of distributed algorithms need to take into account that
communication or processes may be faulty, and correctness guarantees should be
given based on a _resilience condition_ that defines the quantity and quality
of faults (e.g., how many processes may crash or even behave arbitrarily [44,
47, 12]).

Moreover, many distributed systems consist of an arbitrary number of
communicating processes, thus requiring _parameterized verification_
techniques that consider the number of processes as a parameter of the system,
and that can provide correctness guarantees regardless of this parameter.
However, the parameterized verification problem is in general undecidable,
even in restricted settings such as identical and anonymous finite-state
processes that communicate by passing a binary-valued token in a ring [57].

Since undecidability arises so easily in this setting, the research into
automatic parameterized verification can in principle be divided into two
directions: (i) identifying _decidable_ classes of systems and properties [32,
27, 1, 29, 28, 31, 26, 40, 25, 53, 3, 4, 14, 5, 37, 6, 35, 23, 7], which are
often restricted to rather specialized use cases, and (ii) developing _semi-
decision procedures_ [15, 2], which are usually much more versatile but come
without a termination guarantee. In practice however, the line between these
two approaches is not so clear. The line blurs when semi-decision procedures
serve as decision procedures for a certain fragment of their possible inputs,
and on the other hand, many decidable problems in parameterized verification
have a huge complexity [53, 23], and to an engineer it does not make a
difference if the verification algorithm is guaranteed to terminate within a
thousand years, or whether it comes without a termination guarantee.

In this paper, we aim for practical verification techniques that cover a large
class of fault-tolerant distributed algorithms. Our focus is not decidability,
but the development of techniques that can in practice verify a wide range of
distributed algorithms, with full automation. We build on the formal model of
threshold automata (TA) and existing techniques to verify them, which we
combine with insights from the theory of well-structured transition systems
(WSTS) [31] and with abstraction techniques. This combination allows us to
lift some of the restrictions of the existing decidable fragments for TAs, and
to verify distributed algorithms that are not supported by the existing
techniques.

In particular, existing verification techniques for TAs are usually restricted
to reason about shared variables that are monotonically increasing or
decreasing over any run of the automaton. An extension of the model that
allows both increasing and decreasing variables has been considered before
[46], but only to show that the problem becomes undecidable, not to develop a
verification technique for this case. In our setting, we can allow increments,
decrements and resets of shared variables, while still obtaining a semi-
decision procedure, and even a decision procedure in certain cases. In this
paper, we demonstrate how this allows us to reason about round-based
algorithms such as the phase king consensus algorithm [10] and the Red Belly
Blockchain algorithm [22], which both use resets of shared variables at the
beginning of a round, without a fixed bound on the number of rounds to be
executed.

Contributions. In this paper,

  1. 1.

we present an extension of threshold automata that allows increments,
decrements and resets of shared variables (Sect. 2),

  2. 2.

we develop a technique (based on well-structured transition systems) that is a
decision procedure for general coverability properties of canonical threshold
automata [46], and is a semi-decision procedure for our extension (Sect. 3-5),

  3. 3.

we develop an additional abstraction that reduces the search space of this
technique and additionally allows us to check another type of specification,
called reachability properties, on extended threshold automata (Sect. 6),

  4. 4.

we implement our techniques and demonstrate their performance on a number of
examples from the literature, several of which — including the _phase king
consensus_ algorithm and the state-of-the-art Red Belly Blockchain algorithm —
cannot be modeled in canonical threshold automata (Sect. 7).

##  2 System Model

In this section, we build on the existing notion of _threshold automata_ (TAs)
[44] and generalize their notion of shared variables. TAs are a model of
distributed computation that encodes information exchange between processes
into a fixed set of shared variables. Shared variables in TAs are usually
required to be monotonically increasing along an execution to ensure
decidability. We extend the definition such that it permits shared variables
to be decreased or reset, which in general introduces undecidability [46]. We
then define the semantics of an unbounded number of such TAs running in
parallel. In Section 2.1, we introduce the notion of an abstract TA and
provide the semantics for this abstraction.

###### Definition 1

A _threshold automaton_ is a tuple
$A=(L,\mathcal{I},\Gamma,\Pi,\mathcal{R},RC)$ where:

  * •

$L$ is a finite set of _locations_.

  * •

$\mathcal{I}\subseteq L$ is the set of _initial locations_.

  * •

$\Gamma=\\{x_{0},\ldots,x_{m}\\}$ is a finite set of _shared variables_ over
$\mathbb{N}_{0}$.

  * •

$\Pi$ is a finite set of _parameter variables_ over $\mathbb{N}_{0}$. Usually,
$\Pi=\\{n,t,f\\}$, where $n$ is the total number of processes, $t$ is a bound
on the number of tolerated faulty processes , and $f$ is the actual number of
faulty processes.

  * •

$RC$, the _resilience condition_ , is a linear integer arithmetic formula over
parameter variables. E.g.: $RC=n>3t\,\land\,t\geq f$.
For a vector $\mathbf{p}\in\mathbb{N}_{0}^{|\Pi|}$, we write
$\mathbf{p}\models RC$ if $RC$ holds after substituting parameter variables
with values according to $\mathbf{p}$. Then the set of _admissible_ parameters
is $\mathbf{P}_{RC}=\\{\mathbf{p}\in\mathbb{N}_{0}^{|\Pi|}:\mathbf{p}\models
RC\\}$.

  * •

$\mathcal{R}$ is a set of rules where a _rule_ is a tuple
$r=(\textit{from},\textit{to},\varphi,\mathbf{uv},\tau)$ such that:

    * –

$\textit{from},\textit{to}\in L$.

    * –

$\mathbf{uv}\in|\mathbb{Z}|^{|\Gamma|}$ is an _update vector_ for shared
variables.

    * –

$\varphi$ is a conjunction of lower guards and upper guards. A _lower guard_
has the form: $a_{0}+\sum_{i=1}^{|\Pi|}a_{i}\cdot p_{i}\leq x$; An _upper
guard_ has the form: $a_{0}+\sum_{i=1}^{|\Pi|}a_{i}\cdot p_{i}>x$, with
$x\in\Gamma$, $a_{0},\ldots,a_{|\Pi|}\in\mathbb{Q}$,
$p_{1},\ldots,p_{|\Pi|}\in\Pi$.
The left-hand side of a lower or upper guard is called a _threshold_.

    * –

$\tau\subseteq\Gamma$ is the set of shared variables to be reset to 0.

$v_{0}$Wait$v_{1}$$d_{0}$$d_{1}$$r_{0}:x_{0}++$$r_{1}:x_{1}++$$r_{2}:x_{0}\geq
n-t$$r_{3}:x_{1}\geq n-t$

Figure 1: A threshold automaton for simple voting.

###### Example 1

Figure 1 sketches a threshold automaton with $\mathcal{I}=\\{v_{0},v_{1}\\}$,
$L=\\{v_{0},v_{1},Wait,d_{0},d_{1}\\}$, $\Gamma=\\{x_{0},x_{1}\\}$,
$\Pi=\\{n,t,f\\}$. A process in $v_{0}$ has a vote of $0$ and a process in
$v_{1}$ 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 $d_{0}$ ($d_{1}$).

Semantics of TA. Given a TA $A=(L,\mathcal{I},\Gamma,\Pi,\mathcal{R},RC)$, let
the function $N:\>\mathbf{P}_{RC}\rightarrow\mathbb{N}_{0}$ determine the
number of processes to be modelled (usually, $N(n,t,f)=n-f$). Then, the
concrete semantics of a system composed of $N(\mathbf{p})$ threshold automata
running in parallel are defined via a _counter system_.

###### Definition 2

A _counter system_ ($\mathsf{CS}$) of a TA
$A=(L,\mathcal{I},\Gamma,\Pi,\mathcal{R},RC)$ is a transition system
$\mathsf{CS(A)}=(\Sigma,\Sigma_{0},\mathcal{T})$ where

  * •

$\Sigma$ is the set of configurations. A _configuration_ is a tuple
$\sigma=(\mathbf{k},\mathbf{g},\mathbf{p})$ where:

    * –

$\mathbf{k}\in\mathbb{N}_{0}^{|L|}$ is a vector of counter values, where
$\mathbf{k}[i]$ represents the number of processes in location $i$. We refer
to locations by their indices in $L$.

    * –

$\mathbf{g}\in\mathbb{N}_{0}^{|\Gamma|}$ is a vector of shared variables’
values, where $\mathbf{g}[i]$ is the value of variable $x_{i}\in\Gamma$.

    * –

$\mathbf{p}\in\mathbf{P}_{RC}$ is an admissible vector of parameter values.

  * •

The set $\Sigma_{0}$ contains all _initial configurations_ , i.e.,
configurations that satisfy

$\forall x_{i}\in\Gamma:\>\>\sigma.\mathbf{g}[i]=0\text{ and
}\sum_{i\in\mathcal{I}}\sigma.\mathbf{k}[i]=N(\mathbf{p})\text{ and
}\sum_{i\not\in\mathcal{I}}\sigma.\mathbf{k}[i]=0$

  * •

$\mathcal{T}\subseteq\Sigma\times\mathcal{R}\times\Sigma$ is the set of
_transitions_ , where $(\sigma,r,\sigma^{\prime})\in\mathcal{T}$ if and only
if all of the following conditions hold:

    * –

$\sigma^{\prime}.\mathbf{p}=\sigma.\mathbf{p}$ (parameter values never
change).

    * –

$\sigma^{\prime}.\mathbf{k}[r.\textit{to}]=\sigma.\mathbf{k}[r.\textit{to}]+1$
(one process moves to $r.\textit{to}$).

    * –

$\sigma^{\prime}.\mathbf{k}[r.\textit{from}]=\sigma.\mathbf{k}[r.\textit{from}]-1$
(one process moves out of $r.\textit{from}$)

    * –

$\sigma.\mathbf{g}\models r.\varphi$ (i.e., $\varphi$ holds after replacing
shared variables with values $\sigma.\mathbf{g}$)

    * –

$\sigma^{\prime}.\mathbf{g}=\sigma.\mathbf{g}+r.\mathbf{uv}$

    * –

$\forall x_{i}\in\tau$ $\sigma^{\prime}.\mathbf{g}[i]=0$

Instead of $(\sigma,r,\sigma^{\prime})\in\mathcal{T}$ we also write
$\sigma\xrightarrow{r}\sigma^{\prime}$. If
$(\sigma,r,\sigma^{\prime})\in\mathcal{T}$, we say $r$ is _enabled_ in
$\sigma$; otherwise it is _disabled_.

Paths of $\mathsf{CS}$. A sequence
$\sigma_{0},r_{0},\sigma_{1},\ldots,\sigma_{k-1},r_{k-1},\sigma_{k}$ of
alternating configurations and rules is a _path_ of a counter system
$\mathsf{CS(A)}=(\Sigma,\Sigma_{0},\mathcal{T})$ if and only if
$\sigma_{0}\in\Sigma_{0}$ and $(\sigma_{i},r_{i},\sigma_{i+1})\in\mathcal{T}$
for $0\leq i<k$. In this case we also write
$\sigma_{0}\rightarrow^{*}\sigma_{k}$. We denote by $Paths(\mathsf{CS(A)})$
the set of all paths of $\mathsf{CS(A)}$.

###### Example 2

Let $N(n,t,f)=n-f$, $RC=n>3t\land t\geq f$, then the following is a valid path
of the counter system of the TA in Figure 1:
$[(4,0,0,0,0)(0,0)],r_{0},[(3,0,1,0,0)(1,0)],r_{0},[(2,0,2,0,0)(2,0)],r_{0}$,
$[(1,0,3,0,0)(3,0)],r_{0},[(0,0,4,0,0)(4,0)],r_{2},[(0,0,3,1,0)(4,0)]$.

###  2.1 Abstract Threshold Automata

The shared variables and parameters of a TA have infinite domains. To
facilitate the application of parameterized verification techniques for
finite-state processes, we introduce an abstraction of TAs based on parametric
interval abstraction [39].

Abstract Domain. Given a TA $A$, define as
$\mathcal{TH}=\\{d_{0},d_{1},\ldots,d_{k}\\}$ the set of thresholds where
$d_{0}=0,d_{1}=1$ and $\forall i>1$ $d_{i}$ is a threshold in $A$. We assume
that $\forall i,j$ $d_{i}<d_{j}$ if $i<j$. Note that this is always possible
for a fixed $\mathbf{p}\in\mathbf{P}_{RC}$. If different
$\mathbf{p}\in\mathbf{P}_{RC}$ result in different orders of the $d_{i}$, then
we consider each of the finitely many such orders separately. Based on this,
define the finite set of intervals
$\mathcal{D}=\\{I_{0},I_{1},\ldots,I_{k}\\}$ where $I_{i}=[d_{i},d_{i+1}[$ if
$i<k$, and $I_{k}=[d_{k},\infty[$.

###### Definition 3

Abstract Threshold Automata. Given a threshold automaton
$A=(L,\mathcal{I},\Gamma,\Pi,\mathcal{R},RC)$, we define the _abstract
threshold automaton_ (or $\overline{\text{TA}}$)
$\overline{A}=(L,\mathcal{I},\overline{\Gamma},\Pi,\overline{\mathcal{R}})$
where:

  * •

$A$ and $\overline{A}$ share the components $L,\mathcal{I},\Pi$.

  * •

Let $\Gamma=\\{x_{0},\ldots,x_{m}\\}$, then
$\overline{\Gamma}=\\{\overline{x}_{0},\ldots,\overline{x}_{m}\\}$, where each
$\overline{x}_{i}$ is over the domain
$\mathcal{D}=\\{I_{0},I_{1},\ldots,I_{k}\\}$.

  * •

$\overline{\mathcal{R}}$ is the set of abstract rules. An _abstract rule_ is a
tuple
$\overline{r}=(\textit{from},\textit{to},\overline{\varphi},\mathbf{uv},$
$\tau)$ where $\textit{from},\textit{to},\mathbf{uv},\tau$ are as before, and
the _abstract guard_ $\overline{\varphi}$ is a Boolean expression over
equalities between shared variables and abstract values.

Formally, let $\varphi=\varphi_{0}\land\ldots\land\varphi_{k}$, then
$\overline{\varphi}=\overline{\varphi}_{0}\land\ldots\land\overline{\varphi}_{k}$
where for $\varphi_{i}=(d_{j}\leq x)$, we have
$\overline{\varphi}_{i}=\bigvee_{c=j}^{k-1}(\overline{x}=[d_{c},d_{c+1}[)\lor\overline{x}=[d_{k},\infty[$,
and for $\varphi_{i}=(d_{j}>x)$, we have
$\overline{\varphi}_{i}=\bigvee_{c=0}^{j-1}(\overline{x}=[d_{c},d_{c+1}[)$.

###### Example 3

Consider again the TA in Figure 1 with $N(n,t,f)=n-f$, $RC=n>3t\land t\geq
f>1$. We have $\mathcal{TH}=\\{0,1,t,n-t\\}$ and
$\mathcal{D}=\\{[0,1[,[1,t[,[t,n-t[,[n-t,\infty[\\}$ whose order is induced by
$RC$. Moreover, we have $\overline{r}_{0}=r_{0},\overline{r}_{1}=r_{1}$ (due
to the absence of a guard),
$\overline{r}_{2}.\overline{\varphi}=(\overline{x}_{0}=[n-t,\infty[)$,
$\overline{r}_{3}.\overline{\varphi}=(\overline{x}_{1}=[n-t,\infty[)$.

To keep the presentation simple, in our definition all shared variables have
the same abstract domain. The abstraction can be improved by considering
different abstract domains for different variables: for a given shared
variable $x$ we can let $\mathcal{TH}_{x}=\\{d_{0},d_{1},\ldots,d_{l}\\}$
where $d_{0}=0,d_{1}=1$ and $\forall i>1$ there is a guard $d_{i}*x$ with
$*\in\\{\geq,<\\}$, to obtain a corresponding abstract domain
$\mathcal{D}_{x}$ for $x$.

####  2.1.1 Semantics of $\overline{\text{TA}}$.

We first over-approximate the semantics of a system composed of an arbitrary
number of $\overline{\text{TA}}$s by an abstract counter system. We later show
how to detect whether a behavior of the abstract counter system corresponds to
a concrete behavior of a counter system.

###### Definition 4

An _abstract counter system_ ($\mathsf{ACS}$) of
$\overline{A}=(L,\mathcal{I},\overline{\Gamma},\Pi,\overline{\mathcal{R}})$ is
a transition system
$\mathsf{ACS(\overline{A})}=(\overline{\Sigma},\overline{\Sigma}_{0},\overline{\mathcal{T}})$
where:

  * •

$\overline{\Sigma}$ is the set of abstract configurations. A _configuration_
of $\mathsf{ACS(\overline{A})}$ is a tuple
$\overline{\sigma}=(\mathbf{k},\overline{\mathbf{g}})$ where:

    * –

$\mathbf{k}\in\mathbb{N}_{0}^{|L|}$ is a vector of counter values where
$\mathbf{k}[i]$ represents the number of processes in location $i$.

    * –

$\overline{\mathbf{g}}\in\mathcal{D}^{|\overline{\Gamma}|}$ is a vector of
shared variables values, where $\overline{\mathbf{g}}[i]$ is the parametric
interval currently assigned to $\overline{x}_{i}$.

  * •

The set $\overline{\Sigma}_{0}$ contains all _initial abstract configurations_
, i.e., those that satisfy

$\forall\overline{x}_{i}\in\overline{\Gamma}:\>\>\overline{\sigma}.\overline{\mathbf{g}}[i]=I_{0}\text{
and }\sum_{i\in\mathcal{I}}\overline{\sigma}.\mathbf{k}[i]\geq 0\text{ and
}\sum_{i\not\in\mathcal{I}}\overline{\sigma}.\mathbf{k}[i]=0$

  * •

$\overline{\mathcal{T}}\subseteq\overline{\Sigma}\times\overline{\mathcal{R}}\times\overline{\Sigma}$
is the set of transitions. A _transition_ is a tuple
$t=(\overline{\sigma},\overline{r},\overline{\sigma}^{\prime})$ where:

    * –

$\overline{\sigma}^{\prime}.\mathbf{k}[\overline{r}.\textit{to}]=\overline{\sigma}.\mathbf{k}[\overline{r}.\textit{to}]+1$

    * –

$\overline{\sigma}^{\prime}.\mathbf{k}[\overline{r}.\textit{from}]=\overline{\sigma}.\mathbf{k}[\overline{r}.\textit{from}]-1$

    * –

$\overline{\sigma}.\overline{\mathbf{g}}\models\overline{r}.\overline{\varphi}$

    * –

$\overline{\sigma}^{\prime}.\overline{\mathbf{g}}=\overline{\sigma}.\overline{\mathbf{g}}\dot{+}\overline{r}.\mathbf{uv}$,
defined as follows: $\forall i<|\Gamma|$:

      1. 1.

$\overline{\sigma}^{\prime}.\overline{\mathbf{g}}[i]=\overline{\sigma}.\overline{\mathbf{g}}[i]$,
if $\overline{r}.\mathbf{uv}[i]=0$

      2. 2.

$(\overline{\sigma}^{\prime}.\overline{\mathbf{g}}[i]=\overline{\sigma}.\overline{\mathbf{g}}[i])\lor(\overline{\sigma}^{\prime}.\overline{\mathbf{g}}[i]=\overline{\sigma}.\overline{\mathbf{g}}[i].next)$,
if $\overline{r}.\mathbf{uv}[i]=1$

      3. 3.

$(\overline{\sigma}^{\prime}.\overline{\mathbf{g}}[i]=\overline{\sigma}.\overline{\mathbf{g}}[i])\lor(\overline{\sigma}^{\prime}.\overline{\mathbf{g}}[i]=\overline{\sigma}.\overline{\mathbf{g}}[i].previous)$,
if $\overline{r}.\mathbf{uv}[i]=-1$

      4. the first disjunct in 2 and the second in 3 are omitted if $\overline{\sigma}.\overline{\mathbf{g}}[i]=I_{0}$.

      5. 4.

$\forall
x_{i}\in\overline{r}.\tau:\>\>\overline{\sigma}^{\prime}.\overline{\mathbf{g}}[i]=I_{0}$

We also write
$\overline{\sigma}\xrightarrow{\overline{r}}\overline{\sigma}^{\prime}$
instead of
$(\overline{\sigma},\overline{r},\overline{\sigma}^{\prime})\in\overline{\mathcal{T}}$.

In contrast to prior work [39], the domain of counters is not abstracted in
$\mathsf{ACS}$.

Paths of $\mathsf{ACS}$. A sequence
$\overline{\sigma}_{0},\overline{r}_{0},\overline{\sigma}_{1},\ldots,\overline{\sigma}_{k-1},\overline{r}_{k-1},\overline{\sigma}_{k}$
of alternating abstract configurations and rules is called a _path_ of
$\mathsf{ACS(\overline{A})}=(\overline{\Sigma},\overline{\Sigma}_{0},\overline{\mathcal{T}})$,
if $\overline{\sigma}_{0}\in\overline{\Sigma}_{0}$ and
$(\overline{\sigma}_{i},\overline{r}_{i},\overline{\sigma}_{i+1})\in\overline{\mathcal{T}}$
for $0\leq i\leq k$. In this case we also write
$\overline{\sigma}_{0}\rightarrow^{*}\overline{\sigma}_{k}$. We denote by
$Paths(\mathsf{ACS(\overline{A})})$ the set of all paths of
$\mathsf{ACS(\overline{A})}$.

###### Example 4

Let $I_{0}=[0,1[,I_{1}=[1,t[,I_{2}=[t,n-t[,I_{3}=[n-t,\infty[$. The following
is a valid path of the abstract counter system of the TA in Figure 1:
$[(4,0,0,0,0)(I_{0},I_{0})],\overline{r}_{0},[(3,0,1,0,0)(I_{1},I_{0})],\overline{r}_{0},[(2,0,2,0,0)(I_{2},I_{0})],\overline{r}_{0}$,
$[(1,0,3,0,0)(I_{3},I_{0})],\overline{r}_{2},[(1,0,2,1,0)(I_{3},I_{0})]$.

Relation between $\mathsf{ACS(\overline{A})}$ and $\mathsf{CS(A)}$. In
comparison to $\mathsf{CS}$, in $\mathsf{ACS}$ we drop the resilience
condition, as well as the function $N$ that determines the number of processes
to be modeled. Moreover, a transition in $\mathsf{ACS}$ may jump from one
interval to the next too early and may stay in the same interval although it
had to move. We will formalize the relation between the two models in Sect. 4.

##  3 Specifications

We consider three kinds of specifications: _general coverability_ , which
refers to the notion of coverability that is widely used in parameterized
verification, e.g., Petri nets [30] or VASS [50], (non-general) _coverability_
and _reachability_. The latter two are specifications used in prior work on
threshold automata [8, 42, 46]. Note that general coverability can express
mutual exclusion, e.g., that there cannot be two leaders at the same time,
while coverability cannot.

###### Definition 5

The _general parameterized coverability problem_ is: Given $\mathsf{CS(A)}$
and a _general coverability specification_ $\Sigma_{spec}\subseteq\Sigma$,
decide if there is a path in $\mathsf{CS(A)}$ that covers $\Sigma_{spec}$
(i.e., decide if there is some configuration $\sigma_{r}\in\Sigma$ reachable
from $\sigma_{0}\in\Sigma_{0}$ and $\exists\sigma_{spec}\in\Sigma_{spec}$
where $\forall i\>\sigma_{spec}.\mathbf{k}[i]\leq\sigma_{r}.\mathbf{k}[i]$).

###### Definition 6

The _parameterized coverability problem_ is: Given a TA and _coverability
specification_ $L_{spec}=L_{>0}$, decide if there is a path of its
$\mathsf{CS(A)}$ that satisfies $L_{spec}$ (i.e., decide if there is some
configuration $\sigma_{r}\in\Sigma$ reachable from $\sigma_{0}\in\Sigma_{0}$
and $\sigma_{r}$ satisfies $\forall i\in L_{>0}\>\sigma_{r}.\mathbf{k}[i]>0$).

###### Definition 7

The _parameterized reachability problem_ is: Given a TA and a _reachability
specification_ $L_{spec}=(L_{=0},L_{>0})$, decide if there is a path of
$\mathsf{CS(A)}$ that satisfies $L_{spec}$ (i.e., decide if there is some
configuration $\sigma_{r}\in\Sigma$ reachable from $\sigma_{0}\in\Sigma_{0}$
and $\sigma_{r}$ satisfies $\forall i\in L_{=0}\>\sigma_{r}.\mathbf{k}[i]=0$
and $\forall i\in L_{>0}\>\sigma_{r}.\mathbf{k}[i]>0$).

We define similarly all three types of problems for an abstract TA and its
abstract counter system. Usually, our specifications are definitions of error
configurations, and therefore paths that satisfy them, are called _error
paths_.

##  4 $\mathsf{CS}$ vs $\mathsf{ACS}$

We now show that the abstraction from $\mathsf{CS}$ to $\mathsf{ACS}$ is
complete with respect to the specifications introduced in the previous
section.

A path
$\mathsf{\bar{\pi}}=\overline{\sigma}_{0},\overline{r}_{0},\ldots,\overline{r}_{m-1},\overline{\sigma}_{m}$
in
$\mathsf{ACS(\overline{A})}=(\overline{\Sigma},\overline{\Sigma}_{0},\overline{\mathcal{T}})$
_corresponds_ to the paths
$\pi=\sigma_{0},r_{0}^{c_{0}},\ldots,r_{m-1}^{c_{m-1}},\sigma_{m}$ (where
$r_{i}^{c_{i}}$ simulates applying $r_{i}$ $c_{i}$ times) of
$\mathsf{CS(A)}=(\Sigma,\Sigma_{0},\mathcal{T})$ that satisfy the following
conditions:

  * •

$RC\land(\textstyle\sum_{j\in\mathcal{I}}\sigma_{0}.\mathbf{k}[j]=N(n,t,f))$

  * •

$\forall
i<m\;\sigma_{i}.\mathbf{k}[r_{i}.\textit{from}]=c_{i}+\sigma_{i+1}.\mathbf{k}[r_{i}.\textit{from}]\land\sigma_{i+1}.\mathbf{k}[r_{i}.\textit{to}]=c_{i}+\sigma_{i}.\mathbf{k}[r_{i}.\textit{to}]$

  * •

$\forall i<m\;\forall x_{j}\in\Gamma\;x_{j}\notin
r_{i}.\tau\implies\sigma_{i+1}.\mathbf{g}[j]=\sigma_{i}.\mathbf{g}[j]+c_{i}\cdot
r_{i}.\mathbf{uv}[j]$

  * •

$\forall i<m\;\forall x_{j}\in r_{i}.\tau\;\sigma_{i+1}.\mathbf{g}[j]=0$

  * •

$\forall i<m\;\forall
x_{j}\in\Gamma\;\sigma_{i}.\mathbf{g}[j]\in\overline{\sigma}_{i}.\overline{\mathbf{g}}[j]\land\sigma_{i+1}.\mathbf{g}[j]\in\overline{\sigma}_{i+1}.\overline{\mathbf{g}}[j]$

  * •

$\forall
i<m\;c_{i}>1\implies((\sigma_{i+1}.\mathbf{g}-r_{i}.\mathbf{uv})\models
r_{i}.\varphi)$111This is needed only in cases where an update affects any of
the guards of $r_{i}.\varphi$

Let $Concretize(\mathsf{\bar{\pi}})$ be the conjunction of the constraints
above, where quantified formulas are instantiated to a finite conjunction of
quantifier-free formulas. Note that $Concretize(\mathsf{\bar{\pi}})$ is a
quantifier-free formula in linear integer arithmetic, and a satisfying
assignment for $Concretize(\mathsf{\bar{\pi}})$ (that can be computed by an
SMT solver) represents a path of $\mathsf{CS(A)}$ that corresponds to
$\mathsf{\bar{\pi}}$. We say that a path $\mathsf{\bar{\pi}}\in
Paths(\mathsf{ACS(\overline{A})})$ is _spurious_ if
$Concretize(\mathsf{\bar{\pi}})$ is unsatisfiable.

For a given $\mathsf{\bar{\pi}}\in Paths(\mathsf{ACS(\overline{A})})$, let
$Cover(\mathsf{\bar{\pi}})=\forall l\in
L\;\sigma_{m}.\mathbf{k}[l]\geq\overline{\sigma}_{m}.\mathbf{k}[l]$. We can
show the following connection between error paths in $\mathsf{CS(A)}$ and
$\mathsf{ACS(\overline{A})}$:

######  Lemma 1 ()

$\mathsf{ACS(\overline{A})}$ has a non-spurious path that covers a set of
configurations $\Sigma_{spec}\subseteq\Sigma$ iff $\mathsf{CS(A)}$ has a path
that covers $\Sigma_{spec}$.

Note that Lemma 1 subsumes the case of non-general coverability.

Similarly, if $\mathsf{\bar{\pi}}$ is a non-spurious path of
$\mathsf{ACS(\overline{A})}$ that satisfies a reachability specification
$L_{spec}$, let $Reach(\mathsf{\bar{\pi}})=\forall l\in
L\;\sigma_{m}.\mathbf{k}[l]>0\Leftrightarrow\overline{\sigma}_{m}.\mathbf{k}[l]>0$.
Then we can show the following with a similar proof as above, where we replace
$Cover(\mathsf{\bar{\pi}})$ with $Reach(\mathsf{\bar{\pi}})$ and reason
accordingly.

###### Lemma 2

$\mathsf{ACS(\overline{A})}$ has a non-spurious path that satisfies a
reachability specification $L_{spec}$ iff $\mathsf{CS(A)}$ has a path that
satisfies $L_{spec}$.

##  5 Checking General Parameterized Coverability

In this section, we show how abstract counter systems (including ours) can be
framed as well-structured transition systems. We also introduce a
parameterized model checking algorithm for checking general parameterized
coverability in $\mathsf{ACS}$.

###  5.1 Well-structured transition systems

_Well-structured transition systems_ [31] (WSTS) are a class of infinite-state
systems for which the general parameterized coverability problem is decidable
[1, 38]. In the following, we recap the standard definitions of WSTS.

Well-quasi-order. Given a set $S$, a binary relation $\preceq\>\subseteq
S\times S$ is a _well-quasi-order_ (wqo) if $\preceq$ is reflexive,
transitive, and if any infinite sequence $s_{0},s_{1},\ldots\in S^{\omega}$
contains a pair $s_{i}\preceq s_{j}$ with $i<j$. A subset $R\subseteq S$ is an
_anti-chain_ if any two distinct elements of $R$ are incomparable wrt.
$\preceq$. Therefore, $\preceq$ is a wqo on $S$ if and only if it is
reflexive, transitive, and has no infinite anti-chains. The _upward closure_
of a set $R\subseteq S$, denoted ${\uparrow}R$, is the set $\\{s\in
S\mid\exists s^{\prime}\in R:s^{\prime}\preceq s\\}$. We say that $R$ is
_upward-closed_ if ${\uparrow}R=R$, and we call $B\subseteq S$ a _basis_ of
$R$ if ${\uparrow}B=R$. If $\preceq$ is also anti-symmetric, then any basis of
$R$ has a unique subset of minimal elements. We call this set the _minimal
basis_ of $R$, denoted $minBasis(R)$.

Compatibility. Given a transition system $M=(S,S_{0},\mathcal{T})$, we say
that a wqo $\preceq\;\subseteq S\times S$ is _compatible_ with the transition
relation $\mathcal{T}$ if the following holds:

$\forall s,s^{\prime},s_{x}\in S:\text{ if }s\xrightarrow{}s^{\prime}\text{
and }s\preceq s_{x}\text{ then }\exists s_{x}^{\prime}\text{ with
}s^{\prime}\preceq s_{x}^{\prime}\text{ and
}s_{x}\xrightarrow{}^{*}s_{x}^{\prime},$

where $s\xrightarrow{}s^{\prime}$ is a transition in $\mathcal{T}$, and
$s_{x}\xrightarrow{}^{*}s_{x}^{\prime}$ is a path in $M$.

WSTS. We say that $(M,\preceq)$ with $M=(S,S_{0},\mathcal{T})$ is a _well-
structured transition system_ if $\preceq$ is a wqo on $S$ that is compatible
with $\mathcal{T}$. The set of _immediate predecessors_ of a set $R\subseteq
S$ is $pred(R)=\\{s\in S\mid\exists s^{\prime}\in
R:s\xrightarrow{}s^{\prime}\\}.$ We say that a WSTS $(M,\preceq)$ _has
effective $pred$-basis_ if there exists an algorithm that takes as input any
finite set $R\subseteq S$ and returns a finite basis of $pred({\uparrow}R)$.

###  5.2 Abstract Counter Systems as WSTS

To prove that the general parameterized coverability problem is decidable for
abstract TAs, we show that an $\mathsf{ACS}$ can be framed as WSTS. Here, for
a given set $E^{\prime}\subseteq\overline{\Sigma}$ we define
$pred(E^{\prime})=\\{\overline{\sigma}\in\overline{\Sigma}\mid\overline{\sigma}^{\prime}\in
E^{\prime}\land\exists\overline{r}\in\overline{\mathcal{R}}\text{ s.t.
}(\overline{\sigma},\overline{r},\overline{\sigma}^{\prime})\in\overline{\mathcal{T}}\\}$.

######  Lemma 3 ()

Given an abstract counter system
$\mathsf{ACS(\overline{A})}=(\overline{\Sigma},\overline{\Sigma}_{0},\overline{\mathcal{T}})$
let $\lesssim\;\subseteq\overline{\Sigma}\times\overline{\Sigma}$ be the
binary relation defined by:

$(\mathbf{k},\overline{\mathbf{g}})\lesssim(\mathbf{k}^{\prime},\overline{\mathbf{g}}^{\prime})\Leftrightarrow\mathbf{k}\leq\mathbf{k}^{\prime}\land\overline{\mathbf{g}}=\overline{\mathbf{g}}^{\prime}$

where $\leq$ is the component-wise ordering of vectors. Then
$(\mathsf{ACS(\overline{A})},\lessapprox)$ is a WSTS.

Note also that the order $\lesssim$ is anti-symmetric, and therefore every
upward-closed set of configurations has a unique minimal basis.

######  Lemma 4 ()

Given an abstract counter system
$\mathsf{ACS(\overline{A})}=(\overline{\Sigma},\overline{\Sigma}_{0},\overline{\mathcal{T}})$,
the WSTS
$((\overline{\Sigma},\overline{\Sigma}_{0},\overline{\mathcal{T}}),\lesssim)$
has effective pred-basis.

Let $BasisTrans$ be the transitions from which we computed $CPredBasis$ in the
proof of Lemma 4. Concretely, let $\mathbf{u}_{j}$ be the unit vector with
$\mathbf{u}_{j}(j)=1$ and $\mathbf{u}_{j}(i)=0$ for $i\neq j$ then
$BasisTrans(E^{\prime})$ is the set

$\left\\{\begin{array}[]{l|l}((\mathbf{k},\overline{\mathbf{g}}),\overline{r},(\mathbf{k}^{\prime},\overline{\mathbf{g}}^{\prime}))\in\overline{\mathcal{T}}&(\mathbf{k}^{\prime},\overline{\mathbf{g}}^{\prime})\in
E^{\prime}\land\overline{r}=(l_{i},l_{j},\overline{\varphi},\mathbf{uv},\tau)\land\\\
&\left[(\mathbf{k},\overline{\mathbf{g}})\xrightarrow{\overline{r}}(\mathbf{k}^{\prime},\overline{\mathbf{g}}^{\prime})\lor((\mathbf{k},\overline{\mathbf{g}})\xrightarrow{\overline{r}}(\mathbf{k}^{\prime}{+}\mathbf{u}_{j},\overline{\mathbf{g}}^{\prime}){\land}\mathbf{k}^{\prime}[j]{=}0)\right]\end{array}\right\\}.$

The following corollary, derived from the aforementioned definitions, will be
instrumental in establishing the correctness of our algorithms.

###### Corollary 1

Given
$\overline{\sigma}^{\prime}_{1},\overline{\sigma}^{\prime}_{2}\in\overline{\Sigma}$,
if $\overline{\sigma}^{\prime}_{1}\lesssim\overline{\sigma}^{\prime}_{2}$ then
$\\{\overline{r}\in\overline{\mathcal{R}}\mid(\overline{\sigma}_{1},\overline{r},\overline{\sigma}^{\prime}_{1})\in
BasisTrans(\overline{\sigma}^{\prime}_{1})\\}=\\{\overline{r}\in\overline{\mathcal{R}}\mid(\overline{\sigma}_{2},\overline{r},\overline{\sigma}^{\prime}_{2})\in
BasisTrans(\overline{\sigma}^{\prime}_{2})\\}$.

###  5.3 WSTS-based General Parameterized Coverability Checking

In this section, we present our algorithm for solving the general
parameterized coverability problem (see Definition 5). Given an abstract
counter system $\mathsf{ACS(\overline{A})}$ and a finite set of error
configurations $ERR\subseteq\overline{\Sigma}$, we say that a path of
$\mathsf{ACS(\overline{A})}$ is an _error path_ if it starts in
$\overline{\Sigma}_{0}$ and ends in the upward closure of $ERR$. Lemma 4
enables us to use the transitive closure of $CPredBasis(ERR)$ to compute a set
of error paths in $\mathsf{ACS(\overline{A})}$ or a fixed-point in which no
initial configuration occurs. As defined in Section 4, we can examine whether
any of these abstract error paths corresponds to error paths in
$\mathsf{CS(A)}$. The detailed algorithm is given in Algorithm 1, which we
explain in the following.

Algorithm 1 General Parameterized Coverability Checking

1:procedure CheckCoverability(_Abstract Counter System_ $ACS$,$ERR$)

2: $E_{0}\leftarrow ERR,i\leftarrow 1$, $errGraph\leftarrow\emptyset$

3: $visitedTrans\leftarrow\emptyset$ //set of visited transitions

4: while $E_{i-1}\neq\emptyset$ do //has a fixed-point been reached?

5:
$E_{i},visitedTrans\leftarrow\textsc{ComputePredBasis}(E_{i-1},visitedTrans)$

6: $i\leftarrow i+1$

7: $visitedInitialConfigs\leftarrow\bigcup_{j<i}(E_{j}\cap\Sigma_{0})$

8: if $visitedInitialConfigs\neq\emptyset$ then //intersects with initial
configurations?

9:
$errGraph\leftarrow\textsc{ConstructErrGraph}(visitedInitialConfigs,visitedTrans)$

10: $nonSpuriousCE=CheckforNonSpuriousCEs(errGraph)$

11: if $nonSpuriousCE\neq\emptyset$ then //at least one CE is non-spurious

12: return $nonSpuriousCE$ //an error is found!

13: return “ The system is safe! ”

14:procedure ComputePredBasis($E_{i-1}$,$visitedTrans$)

15: Compute $BasisTrans(E_{i-1})$ as explained at the end of Section 5.2

16:
$E_{i}=\\{\overline{\sigma}\in\overline{\Sigma}\mid\exists(\overline{\sigma},\overline{r},\overline{\sigma}^{\prime})\in
BasisTrans(E_{i-1})\\}$

17: $visitedTrans.add(BasisTrans(E_{i-1}))$

18: $finalE_{i}\leftarrow\emptyset$

19: for all $\overline{\sigma}\in E_{i}$ do //remove visited bigger
configurations to ensure termination

20: if $\exists j\leq i,\overline{\sigma}_{s}\in E_{j}$ s.t.
$\overline{\sigma}_{s}\lesssim\overline{\sigma}$ then //smaller
configurations, maybe $\geq$ 1

21:
$visitedTrans.add(\\{(\overline{\sigma}_{s},\overline{r},\overline{\sigma}^{\prime})\mid(\overline{\sigma},\overline{r},\overline{\sigma}^{\prime})\in
BasisTrans(E_{i-1})\\})$

22: else

23: $finalE_{i}.add(\overline{\sigma})$

24: if $\exists\overline{\sigma}_{b}\in finalE_{i}$ s.t.
$\overline{\sigma}\lesssim\overline{\sigma}_{b}$ then //bigger configurations,
maybe $>1$

25:
$visitedTrans.add(\\{(\overline{\sigma},\overline{r},\overline{\sigma}^{\prime})\mid(\overline{\sigma}_{b},\overline{r},\overline{\sigma}^{\prime})\in
BasisTrans(E_{i-1})\\})$

26: $finalE_{i}.remove(\overline{\sigma}_{b})$

27: return $finalE_{i},visitedTrans$

Procedure CheckCoverability takes as argument an $\mathsf{ACS(\overline{A})}$
and a basis for a set of error configurations $ERR$. After initializing local
variables, the procedure enters a while loop that, given $E_{i-1}$, invokes
ComputePredBasis (Line 5), a sub-procedure to compute $E_{i}\supseteq
minBasis(pred({\uparrow}E_{i-1}))$ such that
$\forall\overline{\sigma}\in{\uparrow}E_{i}\>\;\forall
j<i\>\;\overline{\sigma}\not\in{\uparrow}E_{j}$. ComputePredBasis also updates
$visitedTrans$ which represents the set of transitions explored so far. The
loop breaks once a fixed-point has been reached. Line 7 computes the visited
set of initial configurations $visitedInitialConfigs$. If
$visitedInitialConfigs$ is not empty then the procedure extracts all computed
error paths (Line 9). ConstructErrGraph starts from the discovered initial
configuration(s) and uses $visitedTrans$ to construct the error graph
$errGraph$ which encodes all error paths. In a breadth-first fashion, the
procedure CheckforNonSpuriousCEs then unfolds $errGraph$ and evaluates the
spuriousness of uncovered error paths that starts in $\overline{\Sigma}_{0}$
and ends in $ERR$ (Line 10). A path
$\mathsf{\bar{\pi}}=\overline{\sigma}_{0},\overline{r}_{0},\ldots,\overline{r}_{j-1},\overline{\sigma}_{j}$
in $errGraph$ is spurious if $Concretize(\mathsf{\bar{\pi}})\land
Cover(\mathsf{\bar{\pi}})$ is unsatisfiable (see Sect. 4). In the presence of
cycles222A _cycle_ is a sub-sequence of a path that starts and ends in the
same configuration., unfolding may not terminate in the presence of shared-
variable decrements and/or resets (see Theorem 5.1). If all error paths are
spurious, we conclude that the system is safe. Otherwise a concrete path is
returned as a witness of the buggy system (Line 12).

Procedure ComputePredBasis takes as argument the current set $E_{i-1}$, and
the set of visited transitions $visitedTrans$. We compute $E_{i}$ as the
predecessors of $E_{i-1}$ as explained at the end of Section 5.2 (Line 16). At
this point, $E_{i}$ may contain configurations larger than those we have
already explored. To ensure termination, they must be removed. However, before
removing these configurations, we collect their visited transitions since
these may introduce new, unexplored behaviors. The computation of a
comprehensive set of visited transitions, denoted as $visitedTrans$ in this
context, is crucial for the correctness of our algorithm. The importance of
this lies in the necessity to address spurious counterexamples, which mandates
retrieving all paths from an initial configuration to an error configuration.
This is in contrast to ordinary backward model checking, where a single
counterexample suffices. After adding all computed transitions to
$visitedTrans$ (Line 17), we check for each configuration $\overline{\sigma}$
in $E_{i}$ the following:

  * •

For every configuration $\overline{\sigma}_{s}$ with
$\overline{\sigma}_{s}\lesssim\overline{\sigma}$, we add from
$BasisTrans(E_{i-1})$ transitions that start in $\overline{\sigma}$ to
$visitedTrans$ after replacing $\overline{\sigma}$ with
$\overline{\sigma}_{s}$.

  * •

Otherwise, we add $\overline{\sigma}$ to $finalE_{i}$. Also, for every
$\overline{\sigma}_{b}\in finalE_{i}$ with
$\overline{\sigma}\lesssim\overline{\sigma}_{b}$, we add from
$BasisTrans(E_{i-1})$ transitions that start in $\overline{\sigma}_{b}$ to
$visitedTrans$ after replacing $\overline{\sigma}_{b}$ with
$\overline{\sigma}$, and we remove $\overline{\sigma}_{b}$ from $finalE_{i}$.

###  5.4 Correctness.

Algorithm 1 is sound, complete, and terminates when the TA is restricted as in
[8, 43, 46, 42, 45]. Soundness follows directly from encoding non-spuriousness
into the constraint $Concretize(\mathsf{\bar{\pi}})\land
Cover(\mathsf{\bar{\pi}})$, as defined in Section 4.

######  Corollary 2 (Soundness)

Algorithm 1 is sound. That is, if the algorithm computes a non-spurious error
path, then there is a configuration in $\hskip 2.84544pt\uparrow ERR$ that is
reachable in $\mathsf{CS(A)}$.

With Lemma 1, the following lemma proves the algorithm’s completeness.

######  Lemma 5 (Completeness)

If $\mathsf{ACS(\overline{A})}$ has a non-spurious error path
$\mathsf{\bar{\pi}}$, then Algorithm 1 will find it.

Termination. Since Algorithm 1 is sound and complete, it will terminate
whenever $\mathsf{CS}$ has a path that covers $\Sigma_{spec}$. However, Lines
21 and 25 of the algorithm could create cycles in $errGraph$. In the presence
of cycles however, the algorithm could compute an infinite sequence of error
paths. Therefore, we proved the following theorem.

######  Theorem 5.1 ()

If
$\forall\overline{r}\in\overline{\mathcal{R}}:\overline{r}.\mathbf{uv}\in|\mathbb{N}_{0}|^{|\Gamma|}\land\overline{r}.\tau=\emptyset$,
then Algorithm 1 terminates.

It is important to note that if $errGraph$ is acyclic, the algorithm is also
guaranteed to terminate. This includes the case when $errGraph$ is empty,
i.e., the corresponding $\mathsf{ACS}$ has neither spurious nor non-spurious
error paths. The algorithm also terminates if no cycle in $errGraph$ has
decrements or resets.

##  6 Reachability via $(0,1)$-Abstraction

Two configurations $\sigma,\sigma^{\prime}$ may be comparable with respect to
order $\lesssim$ even if some location $l$ is occupied in $\sigma$ while it is
not occupied in $\sigma^{\prime}$. This implies that an algorithm based on
upward-closed sets wrt. $\lesssim$ cannot be used to decide reachability
properties. Furthermore, note that coverability and reachability
specifications (Def. 6 and 7) are agnostic to the precise number of processes
in each location, i.e., they require only to distinguish between locations
that are occupied by one or more processes and those that are not occupied.

To enable reachability checking and to enhance the performance of our
algorithm for (non-general) coverability checking, we introduce a second,
similar abstraction of our system model as in [38], where each counter can
only assume one of two values: $1$ to indicate that the location is currently
occupied by at least one process; and $0$ to indicate that it is not occupied.

$(0,1)$-configuration. Given an abstract threshold automaton
$\overline{A}=(L,\mathcal{I},\overline{\Gamma},\Pi,$
$\overline{\mathcal{R}})$, a _$(0,1)$ -configuration_ is a tuple
${\sigma^{z}}=(\mathbf{k}^{z},\overline{\mathbf{g}})$, where
$\mathbf{k}^{z}\in\mathbb{B}^{\left|{L}\right|}$, and $\overline{\mathbf{g}}$
is defined as before. That is $\mathbf{k}^{z}[i]$ indicates the presence ($1$)
or absence ($0$) of at least one process at location $i$.

###### Definition 8

A _$(0,1)$ -counter system_ (or $\mathsf{ZCS}$) of
$\overline{A}=(L,\mathcal{I},\overline{\Gamma},\Pi,\overline{\mathcal{R}})$,
is a _transition system_
$\mathsf{ZCS(\overline{A})}=(\Sigma^{z},\Sigma^{z}_{0},\mathcal{T}^{z})$,
where:

  * •

$\Sigma^{z}=\mathbb{B}^{\left|{L}\right|}\times\mathcal{D}^{|\overline{\Gamma}|}$,
is the set of $(0,1)$-configurations

  * •

$\Sigma^{z}_{0}\subseteq\Sigma^{z}$ is the set of $(0,1)$-configurations
${\sigma^{z}}$ that satisfy the following:

    * –

$\forall i\in\Gamma:\>\>{\sigma^{z}}.\overline{\mathbf{g}}[i]=I_{0}$

    * –

$\forall i\in L:\>\>{\sigma^{z}}.\mathbf{k}^{z}[i]=1\implies i\in\mathcal{I}$

  * •

the transition relation $\mathcal{T}^{z}$ is the set of transitions
$({\sigma^{z}},\overline{r},{\sigma^{z}}^{\prime})$ with:

    * –

$\overline{r}=\\{\textit{from},\textit{to},\overline{\varphi},\mathbf{uv}\\}\in\overline{\mathcal{R}}$

    * –

${\sigma^{z}}.\overline{\mathbf{g}}\models\overline{r}.\overline{\varphi}$

    * –

${\sigma^{z}}.\mathbf{k}^{z}[\overline{r}.\textit{from}]=1$ and
$({\sigma^{z}}^{\prime}.\mathbf{k}^{z}[\overline{r}.\textit{from}]=0$ or
${\sigma^{z}}^{\prime}.\mathbf{k}^{z}[\overline{r}.\textit{from}]=1)$

    * –

${\sigma^{z}}^{\prime}.\mathbf{k}^{z}[\overline{r}.\textit{to}]=1$

    * –

${\sigma^{z}}^{\prime}.\overline{\mathbf{g}}={\sigma^{z}}.\overline{\mathbf{g}}\dot{+}\mathbf{uv}$

    * –

$\forall
x_{i}\in\overline{r}.\tau:\>\>{\sigma^{z}}^{\prime}.\overline{\mathbf{g}}[i]=I_{0}$

Paths. A sequence
${\sigma^{z}}_{0},\overline{r}_{0},{\sigma^{z}}_{1},\ldots,{\sigma^{z}}_{k-1},\overline{r}_{k-1},{\sigma^{z}}_{k}$
of alternating $(0,1)$-configur-ations and abstract rules is a _path_ of
$\mathsf{ZCS(\overline{A})}$ if $\forall i<k$ we have
$({\sigma^{z}}_{i},\overline{r}_{i},{\sigma^{z}}_{i+1})\in\mathcal{T}^{z}$. We
denote by $Paths(\mathsf{ZCS(\overline{A})})$ the set of all paths of
$\mathsf{ZCS(\overline{A})}$.

We say that a $01$-configuration ${\sigma^{z}}$ satisfies a reachability
specification $L_{spec}$, denoted ${\sigma^{z}}\models L_{spec}$, if for all
$i\in L_{=0}$, ${\sigma^{z}}.\mathbf{k}^{z}[i]=0$, and for all $i\in L_{>0}$,
${\sigma^{z}}.\mathbf{k}^{z}[i]>0$. We say that $\mathsf{ZCS(\overline{A})}$
satisfies $L_{spec}$, denoted $\mathsf{ZCS(\overline{A})}\models L_{spec}$, if
there is a non-spurious path of $\mathsf{ZCS(\overline{A})}$ that ends in
${\sigma^{z}}$ with ${\sigma^{z}}\models L_{spec}$.

Together with Lemma 2, the following lemma shows that our $(0,1)$-abstraction
is precise for reachability and coverability specifications. In other words,
we have $\mathsf{ZCS(\overline{A})}\models L_{spec}$ if and only if
$\mathsf{CS(A)}\models L_{spec}$, given that $L_{spec}$ is a reachability or
coverability specification.

######  Lemma 6 ()

Let
$\overline{A}=(L,\mathcal{I},\overline{\Gamma},\Pi,\overline{\mathcal{R}})$ be
an abstract TA, and $L_{spec}$ a reachability or coverability specification.
We assume w.l.o.g. that $\mathcal{I}=\\{l_{0}\\}$.

Then, there exists a path
${\sigma^{z}}_{0},\overline{r}_{0},{\sigma^{z}}_{1},\ldots,\overline{r}_{n-1},{\sigma^{z}}_{n}\in
Paths(\mathsf{ZCS(\overline{A})})$ such that ${\sigma^{z}}_{n}\models
L_{spec}$ if and only if there exists a path
$\overline{\sigma}_{0},\overline{r}_{0},\overline{\sigma}_{1},\ldots,\overline{r}_{m-1},\overline{\sigma}_{m}\in
Paths(\mathsf{ACS(\overline{A})})$ such that $\overline{\sigma}_{m}\models
L_{spec}$.

###  6.1 Parameterized Reachability Algorithm (PRA)

Our algorithm PRA for solving the parameterized reachability problem accepts
two input parameters: a $01$-counter system $\mathsf{ZCS(\overline{A})}$ and a
finite set of error configurations $ERR\subseteq\Sigma^{z}$. It outputs either
“The system is safe” to indicate that no $(0,1)$-configuration in $ERR$ is
reachable, or an error path of $\mathsf{ZCS(\overline{A})}$. PRA (see App.
0.B) is very similar to Algorithm 1, differing primarily in the approach to
computing the predecessor set. Instead of checking if two configurations are
comparable, we look for equality. Moreover, in contrast to Algorithm 1,
checking whether an error path $\mathsf{\pi^{z}}$ in
$\mathsf{ZCS(\overline{A})}$ is spurious is based on constraint
$Reach(\mathsf{\pi^{z}})$ instead of $Cover(\mathsf{\pi^{z}})$, as described
in Section 4.

Just like Algorithm 1, we have demonstrated soundness and completeness of PRA
in a general context, along with termination, subject to the restrictions
outlined in Theorem 5.1 (see App. 0.B). Moreover, with minimal adjustments to
the reachability algorithm, we can also check coverability within a
$\mathsf{ZCS}$ (see App. 0.C).

##  7 Implementation and Experimental Evaluation

We implemented Algorithm 1 with explicit, unbounded integer counters and PRA
symbolically, leveraging CUDD Decision Diagrams [54] as BDD package. Both use
Z3 [24] as SMT solver back-end. We evaluated our implementations on an AMD
Ryzen 7 5800X CPU, running at 3.8GHz with 32GiB memory of system memory. For
comparisons with ByMC [45], the state-of-the-art model checker for threshold
automata, we executed the tool in the VM provided by the authors on the same
machine, with 6 out of 8 cores and 25GiB of the total system memory. To ensure
an equal environment, we also executed our tool in a virtual machine with the
same restrictions.333The benchmark files and a container image with our tool
are available on Zenodo [9].

Table 1: Comparison of execution time (in s) between ByMC [45] and our
symbolic implementation of PRA. In the Prop. column, $A$ denotes agreement, V
denotes validity, and U denotes unforgeability. TO denotes a timeout after
1.5h.

table]tab:benchmark-bymc-vs-impl  Benchmark Prop. ByMC PRA aba U 0.52 0.12
bcrb U 0.30 0.06 bosco V 42.22 0.73 c1cs V TO 0.23 cc A,V 0.24 0.24 cf1s V
380.81 0.42 frb U 0.19 0.07 nbacg A 0.18 0.36 nbacr V 0.19 0.14 strb U 0.17
0.12 RB-bc A,V 0.32 0.49 RB V TO 1.03 RB-Simpl V TO 61.77

As benchmarks in our decidable fragment, we used the following threshold-based
algorithms from the literature [41]: folklore reliable broadcast (frb) [19],
one-step consensus with zero-degradation (cf1s) [17], consensus in one
communication step (c1cs) [18], consistent broadcast (strb), asynchronous
byzantine agreement (aba) [16], non-blocking atomic commit (nbacr [52] and
nbacg [33]), condition-based consensus (cc) [49], and byzantine one step
consensus (bosco) [55]. Moreover, we considered the following parts of the Red
Belly blockchain [21], which have already been modeled as TA in [11]: the
broadcast protocol (RB-bc), the one-round consensus protocol (RB), and a
simplified one-round consensus protocol (RB-Simpl).

We verified interesting safety specifications: _agreement_ (consistent
decisions among correct processes), _validity_ (the value that has been
decided must have been proposed by some process ), and _unforgeability_ (if
all correct processes have an initial value of 0, then no correct process ever
accepts).

LABEL:tab:benchmark-bymc-vs-impl compares execution times of ByMC and our
implementation of PRA. It shows that PRA significantly outperforms ByMC on all
benchmarks except two. Except for Red Belly protocols, our non-symbolic
implementation can verify all the benchmarks above in less than 2 minutes.

For the undecidable fragment, we used our extended model of TA to model the
following FTDAs from the literature: reliable broadcast [56], k-set agreement
[20], multi-round simplified Red Belly blockchain consensus [21], multi-round
full Red Belly blockchain consensus [21], and phase king consensus [10]. Note
that, in [11], only the one-round protocols were modeled, and only the simple
version was verified. In contrast, we can model the multi-round versions, and
were able to verify all (single- and multi-round) versions except one.

Table 2: Execution time (in s) for PRA on multi-round protocols. TO denotes a
timeout after 2h.

table]tab:benchmark-our-impl  Benchmark PRA multiR-floodMin 0.3 multiR-RelBrd
0.1 multiR-RB-Simpl 6859 multiR-RB TO phase-king-buggy 120 phase-king-partial
300

For the aforementioned TAs, we conducted our experiments on a machine with 2x
AMD EPYC 7773x - 128 Cores, 256 Threads and 2TB RAM. LABEL:tab:benchmark-our-
impl presents execution for running our symbolic implementation on all the
aforementioned multi-round protocols. For the phase-king protocol, PRA was
able to locate a bug in an incorrect model of the algorithm within $2$
minutes, and was also able to prove partial correctness properties, for
example that consensus is actually reachable, in around 5 minutes. We verified
_validity_ for all the remaining benchmarks, and for floodmin we verified
additionally _agreement_. During benchmarking, memory usage peaked at 73 GB.

##  8 Related work

After presenting an approach for verifying FTDAs based on abstraction [39],
Konnov et al. [43, 44, 42, 45] developed several approaches and algorithms
specifically tailored for verifying the safety and liveness properties of
threshold automata. Starting from an acyclic CFA (control flow automaton),
they construct in [39] a finite counter system using parametric interval
abstraction for variables and counters. To refine the abstraction, they detect
spurious transitions using ordinary model checking and user-defined
invariants. Subsequent works [44, 42] improve on the efficiency when verifying
reachability properties in TAs. In [44], they showed the existence of an upper
bound on the distance between states within counter systems of TAs, hence,
demonstrating the completeness of bounded model checking. In [42], the authors
use partial order reduction to generate a finite set of sequences comprising
sets of guards and rules. Each of these sequences represents a possibly
infinite set of error traces. An SMT solver is employed to validate the
existence of concrete error traces. Extending [42], Konnov et al. presented an
approach capable of detecting lasso-shaped traces that violate a given
liveness property [43]. The latter two approaches have been implemented in the
tool ByMC [45]. To enable the functionality of all aforementioned approaches,
the authors found it necessary to impose constraints on threshold automata.
This involved explicitly prohibiting cycles and variable decrements.

A verification tool for parameterized distributed algorithms has been
introduced in [58]. The tool relies on layered threshold automata [13] as a
system model, which can be seen as an infinitely repeating threshold automata.
However, the tool requires users to identify layers (rounds) in the model,
their sequence (infinite interleaving or lasso-shaped sequences), and to
provide predicates.

Decidability and the complexity of verification and synthesis of threshold
automata have also been studied in [8]. Their decision procedure is based on
an SMT encoding of potential error paths, where in general the size of the SMT
formula grows exponentially with the length of the paths. While having
achieved good results with some heuristics that avoid this exponential blow-up
in practice, we believe that these heuristics would not work for threshold
automata with decrements and/or resets444We could not verify this conjecture
since their code is not publicly available.. Moreover, their method requires a
bound on the number of changes in the valuation of thresholds. However, such a
constraint does not apply in the presence of decrements and/or resets.

##  9 Conclusion

In this paper, we have introduced an extension of the computational model
known as threshold automata, to support decrements and resets of shared
variables. This extension in general comes at the cost of decidability, even
for simple state-reachability properties. We developed a semi-decision
procedure for this extended notion of TA, supporting not only the simple
coverability properties from the TA literature, but also general coverability
properties as known from Petri nets or well-structured systems. To support
also reachability properties, we presented an additional abstraction, called
$(0,1)$-abstraction, which is the basis for a semi-decision procedure for
reachability properties of extended TAs.

We have implemented our techniques and evaluated them on examples from the
literature, and on several round-based algorithms that cannot be modeled with
canonical TAs. We show that our semi-decision procedure can find bugs in a
faulty protocol and prove correctness of protocols, even outside the known
decidable fragment. Moreover, on a set of benchmarks in the decidable
fragment, it matches or outperforms the TA model checker ByMC [45].

####  9.0.1 Acknowledgements

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

## References

  * [1] Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. pp. 313–321. IEEE (1996)
  * [2] Abdulla, P.A., Haziza, F., Holík, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf. 18(5), 495–516 (2016). https://doi.org/10.1007/S10009-015-0406-X, https://doi.org/10.1007/s10009-015-0406-x
  * [3] Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: VMCAI. LNCS, vol. 8318, pp. 262–281. Springer (2014). https://doi.org/10.1007/978-3-642-54013-4_15
  * [4] Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: CONCUR. LNCS, vol. 8704, pp. 109–124. Springer (2014). https://doi.org/10.1007/978-3-662-44584-6_9
  * [5] Außerlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: VMCAI. LNCS, vol. 9583, pp. 476–494. Springer (2016). https://doi.org/10.1007/978-3-662-49122-5_23
  * [6] Balasubramanian, A.R., Bertrand, N., Markey, N.: Parameterized verification of synchronization in constrained reconfigurable broadcast networks. In: TACAS (2). Lecture Notes in Computer Science, vol. 10806, pp. 38–54. Springer (2018). https://doi.org/10.1007/978-3-319-89963-3_3
  * [7] Balasubramanian, A.R., Guillou, L., Weil-Kennedy, C.: Parameterized analysis of reconfigurable broadcast networks. In: FoSSaCS. Lecture Notes in Computer Science, vol. 13242, pp. 61–80. Springer (2022). https://doi.org/10.1007/978-3-030-99253-8_4
  * [8] Balasubramanian, A., Esparza, J., Lazić, M.: Complexity of verification and synthesis of threshold automata. In: International Symposium on Automated Technology for Verification and Analysis. pp. 144–160. Springer (2020)
  * [9] Baumeister, T., Eichler, P., Jacobs, S., Sakr, M., Völp, M.: Parameterized verification of round-based distributed algorithms via extended threshold automata - Artifact (2024). https://doi.org/10.5281/zenodo.12513748
  * [10] Berman, P., Garay, J.A., Perry, K.J., et al.: Towards optimal distributed consensus. In: FOCS. vol. 89, pp. 410–415 (1989)
  * [11] Bertrand, N., Gramoli, V., Konnov, I., Lazic, M., Tholoniat, P., Widder, J.: Holistic verification of blockchain consensus. In: DISC. LIPIcs, vol. 246, pp. 10:1–10:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
  * [12] Bertrand, N., Thomas, B., Widder, J.: Guard automata for the verification of safety and liveness of distributed algorithms. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. LIPIcs, vol. 203, pp. 15:1–15:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPICS.CONCUR.2021.15, https://doi.org/10.4230/LIPIcs.CONCUR.2021.15
  * [13] Bertrand, N., Thomas, B., Widder, J.: Guard automata for the verification of safety and liveness of distributed algorithms. In: Concur 2021-International Conference on Concurrency Theory. pp. 1–17 (2021)
  * [14] Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2015). https://doi.org/10.2200/S00658ED1V01Y201508DCT013
  * [15] Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: CAV. LNCS, vol. 1855, pp. 403–418. Springer (2000). https://doi.org/10.1007/10722167_31
  * [16] Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. Journal of the ACM (JACM) 32(4), 824–840 (1985)
  * [17] Brasileiro, F., Greve, F., Mostéfaoui, A., Raynal, M.: Consensus in one communication step. In: Parallel Computing Technologies: 6th International Conference, PaCT 2001 Novosibirsk, Russia, September 3–7, 2001 Proceedings 6. pp. 42–50. Springer (2001)
  * [18] Brasileiro, F., Greve, F., Mostéfaoui, A., Raynal, M.: Consensus in one communication step. In: Parallel Computing Technologies: 6th International Conference, PaCT 2001 Novosibirsk, Russia, September 3–7, 2001 Proceedings 6. pp. 42–50. Springer (2001)
  * [19] Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. Journal of the ACM (JACM) 43(2), 225–267 (1996)
  * [20] Chaudhuri, S., Erlihy, M., Lynch, N.A., Tuttle, M.R.: Tight bounds for k-set agreement. Journal of the ACM (JACM) 47(5), 912–943 (2000)
  * [21] Crain, T., Gramoli, V., Larrea, M., Raynal, M.: Dbft: Efficient leaderless byzantine consensus and its application to blockchains. In: 2018 IEEE 17th International Symposium on Network Computing and Applications (NCA). pp. 1–8. IEEE (2018)
  * [22] Crain, T., Natoli, C., Gramoli, V.: Red belly: A secure, fair and scalable open blockchain. In: SP. pp. 466–483. IEEE (2021)
  * [23] Czerwinski, W., Orlikowski, L.: Reachability in vector addition systems is ackermann-complete. In: 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022. pp. 1229–1240. IEEE (2021). https://doi.org/10.1109/FOCS52979.2021.00120, https://doi.org/10.1109/FOCS52979.2021.00120
  * [24] De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer (2008)
  * [25] Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: CONCUR. LNCS, vol. 6269, pp. 313–327. Springer (2010). https://doi.org/10.1007/978-3-642-15375-4_22
  * [26] Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS. pp. 361–370. IEEE Computer Society (2003). https://doi.org/10.1109/LICS.2003.1210076
  * [27] Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Foundations of Computer Science 14(4), 527–549 (2003). https://doi.org/10.1142/S0129054103001881
  * [28] Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CADE. LNCS, vol. 1831, pp. 236–254. Springer (2000). https://doi.org/10.1007/10721959_19
  * [29] Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS. pp. 352–359. IEEE Computer Society (1999). https://doi.org/10.1109/LICS.1999.782630
  * [30] Finkel, A.: The minimal coverability graph for petri nets. In: Applications and Theory of Petri Nets. Lecture Notes in Computer Science, vol. 674, pp. 210–243. Springer (1991)
  * [31] Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)
  * [32] German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992). https://doi.org/10.1145/146637.146681
  * [33] Guerraoui, R.: Non-blocking atomic commit in asynchronous distributed systems with failure detectors. Distributed Computing 15(1), 17–25 (2002)
  * [34] 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, https://doi.org/10.1145/3068608
  * [35] Jaber, N., Jacobs, S., Wagner, C., Kulkarni, M., Samanta, R.: Parameterized verification of systems with global synchronization and guards. In: CAV (1). Lecture Notes in Computer Science, vol. 12224, pp. 299–323. Springer (2020)
  * [36] 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, https://doi.org/10.1145/3485534
  * [37] Jacobs, S., Sakr, M.: Analyzing guarded protocols: Better cutoffs, more systems, more expressivity. In: International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 247–268. Springer (2018)
  * [38] Jacobs, S., Sakr, M., Völp, M.: Automatic repair and deadlock detection for parameterized systems. In: CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN–FMCAD 2022. p. 225
  * [39] John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: 2013 Formal Methods in Computer-Aided Design. pp. 201–209. IEEE (2013)
  * [40] Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: CAV. LNCS, vol. 6174, pp. 645–659. Springer (2010). https://doi.org/10.1007/978-3-642-14295-6_55, http://dx.doi.org/10.1007/978-3-642-14295-6_55
  * [41] Konnov, I.: Fault-tolerant benchmarks. https://github.com/konnov/fault-tolerant-benchmarks/tree/master/cav15
  * [42] Konnov, I., Lazić, M., Veith, H., Widder, J.: Para 2: parameterized path reduction, acceleration, and smt for reachability in threshold-guarded distributed algorithms. Formal Methods in System Design 51(2), 270–307 (2017)
  * [43] Konnov, I., Lazić, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. pp. 719–734 (2017)
  * [44] Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation 252, 95–109 (2017)
  * [45] Konnov, I., Widder, J.: Bymc: Byzantine model checker. In: International Symposium on Leveraging Applications of Formal Methods. pp. 327–342. Springer (2018)
  * [46] Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: all flavors of threshold automata. In: CONCUR 2018-29th International Conference on Concurrency Theory (2018)
  * [47] Maric, O., Sprenger, C., Basin, D.A.: Cutoff bounds for consensus algorithms. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10427, pp. 217–237. Springer (2017). https://doi.org/10.1007/978-3-319-63390-9_12, https://doi.org/10.1007/978-3-319-63390-9_12
  * [48] 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, https://doi.org/10.1007/978-3-030-53291-8_12
  * [49] Mostéfaoui, A., Mourgaya, E., Parvédy, P.R., Raynal, M.: Evaluating the condition-based approach to solve consensus. In: 2003 International Conference on Dependable Systems and Networks, 2003. Proceedings. pp. 541–541. IEEE Computer Society (2003)
  * [50] Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6(2), 223–231 (1978)
  * [51] 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, https://doi.org/10.14279/tuj.eceasst.72.1013
  * [52] Raynal, M.: A case study of agreement problems in distributed systems: non-blocking atomic commitment. In: Proceedings 1997 High-Assurance Engineering Workshop. pp. 209–214. IEEE (1997)
  * [53] Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D’Argenio, P.R., Melgratti, H.C. (eds.) CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8052, pp. 5–24. Springer (2013). https://doi.org/10.1007/978-3-642-40184-8_2, https://doi.org/10.1007/978-3-642-40184-8_2
  * [54] Somenzi, F.: Cudd: Cu decision diagram package release 2.3. 0. University of Colorado at Boulder 621 (1998)
  * [55] Song, Y.J., van Renesse, R.: Bosco: One-step byzantine asynchronous consensus. In: International Symposium on Distributed Computing. pp. 438–450. Springer (2008)
  * [56] Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Computing 2(2), 80–94 (1987)
  * [57] Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988). https://doi.org/10.1016/0020-0190(88)90211-6, https://doi.org/10.1016/0020-0190(88)90211-6
  * [58] Thomas, B., Sankur, O.: Pylta: A verification tool for parameterized distributed algorithms. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 28–35. Springer (2023)
  * [59] 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, https://doi.org/10.1145/2737924.2737958

##  Appendix 0.A Proofs

See 1

###### Proof

$\Rightarrow$: Let $\mathsf{\bar{\pi}}$ be a non-spurious path of
$\mathsf{ACS(\overline{A})}$ that covers $\sigma_{spec}\in\Sigma_{spec}$. Then
$Concretize(\mathsf{\bar{\pi}})\land Cover(\mathsf{\bar{\pi}})$ is satisfiable
and its satisfying assignment is a path in $\mathsf{CS(A)}$ that covers
$\sigma_{spec}$.

  * •

$RC\land\textstyle\sum_{j\in\mathcal{I}}\sigma_{0}.\mathbf{k}[j]=N(n,t,f)$,
makes sure that we have admissible parameters and we start from a valid
initial configuration.

  * •

$\forall
i<m\;\sigma_{i}.\mathbf{k}[r_{i}.\textit{from}]=c_{i}+\sigma_{i+1}.\mathbf{k}[r_{i}.\textit{from}]\land\sigma_{i+1}.\mathbf{k}[r_{i}.\textit{to}]=c_{i}+\sigma_{i}.\mathbf{k}[r_{i}.\textit{to}]$,
ensures that, for each local transition, exactly one process makes a move.

  * •

$\forall i<m\;\forall x_{j}\in\Gamma\;x_{j}\notin
r_{i}.\tau\implies\sigma_{i+1}.\mathbf{g}[j]=\sigma_{i}.\mathbf{g}[j]+c_{i}\cdot
r_{i}.\mathbf{uv}[j]$, guarantees correct updates for all the variables that
haven’t been reset.

  * •

$\forall i<m\;\forall x_{j}\in r_{i}.\tau\;\sigma_{i+1}.\mathbf{g}[j]=0$,
resets all the variables in $r_{i}.\tau$.

  * •

$\forall i<m\;\forall
x_{j}\in\Gamma\;\sigma_{i}.\mathbf{g}[j]\in\overline{\sigma}_{i}.\overline{\mathbf{g}}[j]\land\sigma_{i+1}.\mathbf{g}[j]\in\overline{\sigma}_{i+1}.\overline{\mathbf{g}}[j]$

  * $\land$ $\forall i<m\;c_{i}>1\implies((\sigma_{i+1}.\mathbf{g}-r_{i}.\mathbf{uv})\models r_{i}.\varphi)$, ensures that a guard is satisfied before it is executed.

$\Leftarrow$: Let $\pi$ be a path of $\mathsf{CS(A)}$ that covers
$\sigma_{spec}\in\Sigma_{spec}$. Let us construct
$\mathsf{\bar{\pi}}=\overline{\sigma}_{0},\overline{r}_{0},\ldots,\overline{r}_{m-1},\overline{\sigma}_{m}$
from $\pi$ by replacing concrete rules and configurations with their
corresponding abstract versions, and by then replacing any sub-sequence of
repeating abstract configurations and rules
$\overline{\sigma},\overline{r},\overline{\sigma},\overline{r},\overline{\sigma}$
with $\overline{\sigma},\overline{r},\overline{\sigma}$. Then
$\overline{\sigma}_{0}\in\overline{\Sigma}_{0}$, $\forall
i\>\sigma_{spec}.\mathbf{k}[i]\leq\overline{\sigma}_{m}.\mathbf{k}[i]$, and
$\mathsf{\bar{\pi}}$ is a path of $\mathsf{ACS(\overline{A})}$.

∎

See 3

###### Proof

The order $\lesssim$ is reflexive and transitive, and it has no infinite
antichain due to the fact that $\leq$ is a wqo. To see that $\lesssim$ is
strongly compatible with $\mathcal{T}$, let
$(\mathbf{k}_{1},\overline{\mathbf{g}}_{1})\xrightarrow{\overline{r}}(\mathbf{k}^{\prime}_{1},\overline{\mathbf{g}}^{\prime}_{1})$,
and let
$(\mathbf{k}_{1},\overline{\mathbf{g}}_{1})\lesssim(\mathbf{k}_{2},\overline{\mathbf{g}}_{2})$.
Then we have
$(\mathbf{k}_{2},\overline{\mathbf{g}}_{2})\xrightarrow{\overline{r}}(\mathbf{k}^{\prime}_{2},\overline{\mathbf{g}}^{\prime}_{2})$
due to the fact that
$\overline{\mathbf{g}}_{1}=\overline{\mathbf{g}}_{2}\land\mathbf{k}_{1}\leq\mathbf{k}_{2}$.
We also have
$(\mathbf{k}^{\prime}_{1},\overline{\mathbf{g}}^{\prime}_{1})\lesssim(\mathbf{k}^{\prime}_{2},\overline{\mathbf{g}}^{\prime}_{2})$
by resolving the non-determinism for obtaining
$\overline{\mathbf{g}}_{2}^{\prime}$ in the same way as in the transition
$(\mathbf{k}_{1},\overline{\mathbf{g}}_{1})\xrightarrow{\overline{r}}(\mathbf{k}^{\prime}_{1},\overline{\mathbf{g}}^{\prime}_{1})$
(i.e., whether to change an interval or not). ∎

See 4

###### Proof

Let $E^{\prime}\subseteq\overline{\Sigma}$ be finite. Note that $pred(\hskip
2.84544pt\uparrow E^{\prime})$ is upward-closed due to the strong
compatibility of $\lesssim$ established in the proof of Lemma 3, and therefore
it has a finite minimal basis, denoted $minBasis(pred(\hskip 2.84544pt\uparrow
E^{\prime}))$.

Let $\mathbf{u}_{i}$ be the unit vector with $\mathbf{u}_{i}(i)=1$ and
$\mathbf{u}_{i}(j)=0$ for $j\neq i$. Consider the set
$CPredBasis(E^{\prime})$, defined as

$\left\\{\begin{array}[]{l|l}(\mathbf{k},\overline{\mathbf{g}})\in\overline{\Sigma}{}&~{}\exists(\mathbf{k}^{\prime},\overline{\mathbf{g}}^{\prime})\in
E^{\prime},\exists\overline{r}=(l_{i},l_{j},\overline{\varphi},\mathbf{uv},\tau)\in\overline{\mathcal{R}}\text{
such that }\\\
&~{}~{}\left[(\mathbf{k},\overline{\mathbf{g}})\xrightarrow{\overline{r}}(\mathbf{k}^{\prime},\overline{\mathbf{g}}^{\prime})\lor\left((\mathbf{k},\overline{\mathbf{g}})\xrightarrow{\overline{r}}(\mathbf{k}^{\prime}+\mathbf{u}_{j},\overline{\mathbf{g}}^{\prime})\land\mathbf{k}^{\prime}[j]=0\right)\right]\end{array}\right\\}.$

First, note that we have $CPredBasis(E^{\prime})\subseteq pred(\hskip
2.84544pt\uparrow E^{\prime})$, which follows by definition of
$CPredBasis(E^{\prime})$ and the fact that, if
$(\mathbf{k}^{\prime},\overline{\mathbf{g}}^{\prime})\in E^{\prime}$, then
$(\mathbf{k}^{\prime}+\mathbf{u}_{j},\overline{\mathbf{g}}^{\prime})\in\hskip
2.84544pt\uparrow E^{\prime}$. To see that $CPredBasis(E^{\prime})\supseteq
minBasis(pred(\hskip 2.84544pt\uparrow E^{\prime}))$, assume towards a
contradiction that it is not. Then, there exist
$(\mathbf{k}_{1},\overline{\mathbf{g}}_{1})\in(minBasis(pred(\hskip
2.84544pt\uparrow E^{\prime}))\cap\neg CPredBasis(E^{\prime}))$,
$(\mathbf{k}^{\prime}_{1},\overline{\mathbf{g}}^{\prime}_{1})\in\hskip
2.84544pt\uparrow E^{\prime}$, and
$(\mathbf{k}^{\prime}_{2},\overline{\mathbf{g}}^{\prime}_{2})\in E^{\prime}$
with
$(\mathbf{k}_{1},\overline{\mathbf{g}}_{1})\xrightarrow{\overline{r}}(\mathbf{k}^{\prime}_{1},\overline{\mathbf{g}}^{\prime}_{1})$
and
$(\mathbf{k}^{\prime}_{2},\overline{\mathbf{g}}^{\prime}_{2})\lesssim(\mathbf{k}^{\prime}_{1},\overline{\mathbf{g}}^{\prime}_{1})$.
We differentiate between two cases:

  * •

Case $\mathbf{k}^{\prime}_{2}[j]=0$: Let
$\mathbf{k}_{2}=\mathbf{k}^{\prime}_{2}+\mathbf{u}_{i}$, and
$\overline{\mathbf{g}}_{2}=\overline{\mathbf{g}}_{1}$. Then
$\overline{\mathbf{g}}_{2}\models\overline{r}.\overline{\varphi}$, and
$((\mathbf{k}_{2},\overline{\mathbf{g}}_{2}),\overline{r},(\mathbf{k}^{\prime}_{2}+\mathbf{u}_{j},\overline{\mathbf{g}}^{\prime}_{2}))\in\overline{\mathcal{R}}$.
Hence $(\mathbf{k}_{2},\overline{\mathbf{g}}_{2})\in CPredBasis(E^{\prime})$,
and
$(\mathbf{k}_{2},\overline{\mathbf{g}}_{2})\lesssim(\mathbf{k}_{1},\overline{\mathbf{g}}_{1})$.
Contradiction.

  * •

Case $\mathbf{k}^{\prime}_{2}[j]>0$: Let
$\mathbf{k}_{2}=\mathbf{k}^{\prime}_{2}+\mathbf{u}_{i}-\mathbf{u}_{j}$, and
$\overline{\mathbf{g}}_{2}=\overline{\mathbf{g}}_{1}$. Then
$\overline{\mathbf{g}}_{2}\models\overline{r}.\overline{\varphi}$, and
$((\mathbf{k}_{2},\overline{\mathbf{g}}_{2}),\overline{r},(\mathbf{k}^{\prime}_{2},\overline{\mathbf{g}}^{\prime}_{2}))\in\overline{\mathcal{R}}$.
Hence $(\mathbf{k}_{2},\overline{\mathbf{g}}_{2})\in CPredBasis(E^{\prime})$,
and
$(\mathbf{k}_{2},\overline{\mathbf{g}}_{2})\lesssim(\mathbf{k}_{1},\overline{\mathbf{g}}_{1})$.
Contradiction. ∎

See 5.1 Proof sketch. Suppose we have
$\forall\overline{r}\in\overline{\mathcal{R}}:\overline{r}.\mathbf{uv}\in|\mathbb{N}_{0}^{|\Gamma|}\land\overline{r}.\tau=\emptyset$.
In this case, once a rule changes its status (enabled/disabled), it will
retain it forever. Suppose
$\mathsf{\bar{\pi}}^{e}=\overline{\sigma}^{e}_{0},\overline{r}_{0},\ldots,\overline{r}_{m-1},\overline{\sigma}^{e}_{m}$
is a path in $errGraph$ and let
$C_{e}=\overline{\sigma}^{e}_{i},\overline{r}_{i},\ldots,\overline{r}_{j},\overline{\sigma}^{e}_{j}$
be a sub-sequence of $\mathsf{\bar{\pi}}^{e}$ with
$\overline{\sigma}^{e}_{i}=\overline{\sigma}^{e}_{j}$. Note that a cycle
$\overline{\sigma}^{e}_{i},\overline{r}_{i},\ldots,\overline{r}_{j},\overline{\sigma}^{e}_{i}$
in $errGraph$ does not necessarily correspond to a concrete cycle. It just
indicates that the sequence of transitions $r_{i},\ldots,r_{j}$ may be
executed an arbitrary number of times. In the general case, the algorithm
checks if $\mathsf{\bar{\pi}}^{e}$ is spurious (see Section 4) and whether
paths, formed by unfolding $C_{e}$ in $\mathsf{\bar{\pi}}^{e}$ an arbitrary
number of times, are spurious. However, in the absence of shared variable
decrements and resets, it suffices to check $\mathsf{\bar{\pi}}^{e}$. This is
because, regardless of how we unfold the cycle $C_{e}$, the initial
configuration, the final configuration, and all intermediate configurations
will consistently have the same vector $\overline{\mathbf{g}}$. Please note
that if the TA contains cycles with upper guards, then while only a finite
number of processes may traverse it, they can do so an unbounded number of
times. Therefore, the strategy outlined above may not suffice in such cases.
Consequently, in such a case, we need to use a simplified variant of the
reachability formula used in [8]. This formual would be relatively concise,
since it uses only the transitions that appear on the cycle of the error path
and leverages the total order on the transitions of the TA cycle.

∎It’s worth noting that none of the TA benchmarks in Table
LABEL:tab:benchmark-bymc-vs-impl have cycles. Furthermore, all the computed
error graphs for the benchmarks in LABEL:tab:benchmark-our-impl were empty.

See 6

###### Proof

$\Rightarrow$:

Suppose there exists
$\mathsf{\pi^{z}}={\sigma^{z}}_{0},\overline{r}_{0},{\sigma^{z}}_{1},\ldots,\overline{r}_{n-1},{\sigma^{z}}_{n}\in
Paths(\mathsf{ZCS(\overline{A})})$ such that ${\sigma^{z}}_{n}\models
L_{spec}$. Let $b$ be the number of transitions
$({\sigma^{z}}_{k},\overline{r}_{k},{\sigma^{z}}_{k+1})$ in $\mathsf{\pi^{z}}$
with ${\sigma^{z}}_{k+1}.\mathbf{k}^{z}[\overline{r}.\textit{from}]=1$, i.e.,
the transitions where we keep a $1$ in location $\overline{r}.\textit{from}$.
Then we construct the corresponding path
$\mathsf{\bar{\pi}}=\overline{\sigma}_{0},\overline{r}_{0},\ldots,\overline{r}_{m-1},\overline{\sigma}_{m}$
as follows:

  1. 1.

Let $\overline{\sigma}_{0}$ be the initial configuration in
$\mathsf{\bar{\pi}}$ with $\overline{\sigma}_{0}.\mathbf{k}[l_{0}]=2^{b}$.

  2. 2.

For every transition $({\sigma^{z}}_{k},\overline{r}_{k},{\sigma^{z}}_{k+1})$
in $\mathsf{\pi^{z}}$:

     * •

if ${\sigma^{z}}_{k+1}.\mathbf{k}^{z}[\overline{r}_{k}.\textit{from}]=0$, then
we obtain $\overline{\sigma}_{k+1}$ from $\overline{\sigma}_{k}$ by executing
$\overline{r}_{k}$ until location $\overline{r}_{k}.\textit{from}$ becomes
empty. If
${\sigma^{z}}_{k+1}.\overline{\mathbf{g}}\neq{\sigma^{z}}_{k}.\overline{\mathbf{g}}$,
then in $\mathsf{\bar{\pi}}$ we only change the valuation of shared variables
$\overline{\mathbf{g}}$ with the last execution of $\overline{r}_{k}$.

     * •

if ${\sigma^{z}}_{k+1}.\mathbf{k}^{z}[\overline{r}_{k}.\textit{from}]=1$, then
we execute $\overline{r}_{k}$ $\frac{c_{k}}{2}$ times, where $c_{k}$ is the
number of processes that are in location $\overline{r}_{k}.\textit{from}$
(i.e., we move half of the processes to $\overline{r}_{k}.\textit{to}$, and
keep the other half in $\overline{r}_{k}.\textit{from}$). As before, we change
$\overline{\mathbf{g}}$ only with the last execution of $\overline{r}_{k}$.
Since we started with $2^{b}$ processes in the initial configuration, this is
possible $b$ times, which is exactly the number of such transitions in the
path.

By construction of $\mathsf{\bar{\pi}}$, the same locations in
${\sigma^{z}}_{n}$ and $\overline{\sigma}_{m}$ are occupied, and hence,
$\overline{\sigma}_{m}\models L_{spec}$.

$\Leftarrow$:

Suppose there is
$\overline{\sigma}_{0},\overline{r}_{0},\overline{\sigma}_{1},\ldots\overline{r}_{m-1}\overline{\sigma}_{m}\in
Paths(\mathsf{ACS(\overline{A})})$ such that $\overline{\sigma}_{m}\models
L_{spec}$. Then the corresponding path of $\mathsf{ZCS(\overline{A})}$ is
obtained by simply replacing each configuration $\overline{\sigma}_{j}$ with a
$(0,1)$-configuration ${\sigma^{z}}_{j}$ such that for each location $i$,
$\overline{\sigma}_{j}.\mathbf{k}[i]\geq
1\Leftrightarrow{\sigma^{z}}_{j}.\mathbf{k}^{z}[i]=1$ and
$\overline{\sigma}_{j}.\mathbf{k}[i]=0\Leftrightarrow{\sigma^{z}}_{j}.\mathbf{k}^{z}[i]=0$.
The result is a valid path of $\mathsf{ZCS(\overline{A})}$ with
${\sigma^{z}}_{m}\models L_{spec}$. ∎

See 5

###### Proof

Since $\lesssim$ is a wqo, any infinite increasing sequence of upward-closed
sets eventually stabilizes [31]. Therefore, Algorithm 1 is guaranteed to
converge to a fixed-point. Note that for increasing $j$, the sequence
$\bigcup_{0\leq i\leq j}E_{i}$, which is based on the sets $E_{i}$ computed by
Algorithm 1, is an increasing sequence of upward-closed sets. Therefore, the
algorithm will converge to a fixed-point.

In order to reach a contradiction, suppose the algorithm reached a fixed-point
without computing any non-spurious error path, and let
$E_{i},\ldots,E_{0}=\Sigma_{spec}$ be the computed sets of predecessor bases.
Let
$\mathsf{\bar{\pi}}=\overline{\sigma}_{0},\overline{r}_{0},\ldots,\overline{r}_{j-1},\overline{\sigma}_{j}$.
Since $\mathsf{\bar{\pi}}$ is an error path that was not computed by Algorithm
1, then $\overline{\sigma}_{j}\in{\uparrow}E_{0}$ and there exists $i>0$ where
$\forall k>i\;\forall l\leq
i:\>\overline{\sigma}_{j-k}\not\in{\uparrow}E_{l}$, i.e.
$\\{\overline{\sigma}_{0},\ldots,\overline{\sigma}_{j-(i+1)}\\}\cap({\uparrow}E_{i}\cup\ldots\cup{\uparrow}E_{0})=\emptyset$.
Due to procedure ComputePredBasis we have $\forall k\leq
i:\>\overline{\sigma}_{j-k}\in E_{l}$ with $l\leq k$. We assume that $i<j$
since other cases are trivial. Executing the procedure
$\textsc{ComputePredBasis}(E_{i},visitedTrans)$ (based on Lemma 4) must have
resulted in an empty set. Then, $\overline{\sigma}_{j-(i+1)}\in E_{l}$ with
$l\leq i$.Furthermore, the algorithm guarantees also that the transition
$(\overline{\sigma}_{j-(i+1)},\overline{r}_{j-(i+1)},\overline{\sigma}_{j-i})\in
visitedTrans$ is computed (check Line 17). Therefore, due to Corollary 1,
$\mathsf{\bar{\pi}}$ is a path in $errGraph$. Contradiction. ∎

##  Appendix 0.B Parameterized Reachability Algorithm

This section introduces our algorithm for solving the parameterized
reachability problem (see Definition 7). Algorithm 2 accepts two input
parameters: a $01$-counter system $\mathsf{ZCS(\overline{A})}$ and a finite
set of error configurations $ERR\subseteq\Sigma^{z}$. It outputs either “The
system is safe” to indicate that no $(0,1)$-configuration in $ERR$ is
reachable, or an error path of $\mathsf{ZCS(\overline{A})}$.

Algorithm 2 is very similar to Algorithm 1, differing primarily in the method
for computing the predecessor set. As before, error paths may be spurious, and
the algorithm needs to keep track of all possible paths on which a
configuration may be reached. In contrast to Algorithm 1, checking whether
error path $\mathsf{\pi^{z}}$ in $\mathsf{ZCS(\overline{A})}$ is spurious is
based on constraint $Reach(\mathsf{\pi^{z}})$ instead of
$Cover(\mathsf{\pi^{z}})$, as described in Section 4.

Algorithm 2 Parameterized Reachability Checking (PRA)

1:procedure CheckReachability(_$01$ -Counter System_ $\mathsf{ZCS}$, $ERR$)
//same approach as CheckCoverability in Algorithm 1 but instead of
//ComputePredBasis we have ComputePred

2:procedure ComputePred($E_{i-1}$,$visitedTrans$)

3:
$TrPred(E_{i-1})\leftarrow\\{({\sigma^{z}},\overline{r},{\sigma^{z}}^{\prime})\in\mathcal{T}^{z}\mid{\sigma^{z}}^{\prime}\in
E_{i-1}\\}$

4:
$E_{i}=\\{{\sigma^{z}}\mid\exists({\sigma^{z}},\overline{r},{\sigma^{z}}^{\prime})\in
TrPred(E_{i-1})\\}$

5: $visitedTrans.appendAll(TrPred(E_{i-1}))$

6: $finalE_{i}\leftarrow\emptyset$

7: for all ${\sigma^{z}}\in E_{i}$ do //remove visited equal configs to ensure
termination

8: if $\exists j\leq i,{\sigma^{z}}_{e}\in E_{j}$ s.t.
${\sigma^{z}}_{e}={\sigma^{z}}$ then

9:
$visitedTrans({\sigma^{z}}_{e}).append(\\{({\sigma^{z}}_{e},\overline{r},{\sigma^{z}}^{\prime})\mid({\sigma^{z}},\overline{r},{\sigma^{z}}^{\prime})\in
TrPred(E_{i-1})\\})$

10: else

11: $finalE_{i}.append({\sigma^{z}})$

12: return $finalE_{i},visitedTrans$

Procedure ComputePred takes as argument the set $E_{i-1}$, and the set of
visited transitions $visitedTrans$. We begin by obtaining the set of
predecessors, denoted as $E_{i}$, from the incoming transitions of the
configurations in $E_{i-1}$ (Lines 3-4). The set $E_{i}$ may contain
configurations that are equal to configurations that have been already
explored. Hence, after adding all computed transitions to $visitedTrans$ (Line
5), we check if there is a configuration ${\sigma^{z}}_{e}$ with
${\sigma^{z}}_{e}={\sigma^{z}}$. If such a configuration is found, we add
${\sigma^{z}}$’s transitions to ${\sigma^{z}}_{e}$ (Line 9).

Combining Lemmas 5 and 6 yields the following corollary:

######  Corollary 3 (Soundness, Completeness)

Algorithm 2 is sound and complete, i.e., Algorithm 2 computes a non-spurious
error path if and only if $\mathsf{CS(A)}$ includes a reachable configuration
that violates a given reachability specification.

Termination. Unfortunately, Algorithm 2 may compute an error graph with cycles
($errGraph$), and checking for non-spurious error paths may not terminate
because there may be infinitely many paths to check.

###### Theorem 0.B.1

If
$\forall\overline{r}\in\overline{\mathcal{R}}:\overline{r}.\mathbf{uv}\in|\mathbb{N}_{0}|^{|\Gamma|}\land\overline{r}.\tau=\emptyset$,
then Algorithm 2 terminates.

The proof is very similar to Theorem 5.1, and thus has been omitted.
Similarly, in this scenario, the algorithm terminates if
$\mathsf{CS(A)}\models L_{spec}$ or if $errGraph$ is acyclic, empty, or all
its cycles have neither decrements nor resets.

##  Appendix 0.C Checking Coverability in $\mathsf{ZCS(\overline{A})}$

Let $\lesssim^{z}\;\subseteq\Sigma^{z}\times\Sigma^{z}$ be the binary relation
defined by:

$(\mathbf{k}^{z},\overline{\mathbf{g}})\lesssim^{z}(\mathbf{k}^{z}{{}^{\prime}},\overline{\mathbf{g}}^{\prime})\Leftrightarrow\mathbf{k}^{z}\leq\mathbf{k}^{z}{{}^{\prime}}\land\overline{\mathbf{g}}=\overline{\mathbf{g}}^{\prime}$

where $\leq$ is the component-wise ordering of vectors. Then, we say that a
$(0,1)$-configuration ${\sigma^{z}}$ satisfies a coverability specification
$L_{spec}$ (see Definition 6), denoted ${\sigma^{z}}\models L_{spec}$, if for
all $i\in L_{>0}$, ${\sigma^{z}}.\mathbf{k}^{z}[i]>0$. Thus, out of a
coverability specification $L^{\prime}_{spec}=L_{>0}$, we can generate a
reachability specification $L_{spec}=L_{>0}\cup L_{=0}$ and use Algorithm 2 to
check it. Alternatively, a variant of Algorithm 1 can be used, in which the
ComputePredBasis procedure uses $\lesssim^{z}$ in place of the previously used
$\lesssim$.