Modular Parameterized Model Checking of Threshold-Based Distributed Algorithms

Modular Parameterized Model Checking of Threshold-Based Distributed Algorithms Paul Eichler1

and Swen Jacobs1

arXiv:2611.07919v1 [cs.DC] 5 Nov 2026

CISPA Helmholtz Center for Information Security, Saarbrücken, Germany { paul.eichler, jacobs }@cispa.de

Abstract. We present a novel approach for model checking fault-tolerant distributed algorithms: instead of building large, monolithic algorithm models, we propose a modular approach where the user decomposes the algorithm into modules, verifies them individually, and replaces them with a synchronous abstraction. To enable our technique, we introduce a new system model that combines aspects of threshold automata and global synchronization protocols. We investigate the expressiveness of our new model, and present a (bounded) model checking procedure as well as a method for checking the correctness of the abstraction step. We implemented the technique and report on promising experimental results on a case study. Keywords: Model Checking, Parameterized Verification, Distributed Algorithms

1

Introduction

Large-scale distributed systems, such as cloud platforms or blockchain systems, increasingly form the backbone of much of our industry and society. Bugs or failures in these systems can lead to significant harm, which encouraged a wide range of efforts to formally verify their correctness [28, 30, 42, 46–48, 56]. However, the task remains challenging because of the intrinsic complexity of the setting. Distributed systems and their underlying algorithms are usually required to scale to an arbitrary number of participants. Since the probability of a failure in such a system increases with the number of components, to be practical, distributed algorithms also need to be fault-tolerant. In settings like blockchain protocols, where arbitrary untrusted nodes can join, the algorithms need to withstand arbitrary failures referred to as Byzantine failures [41]. One of the main techniques for verifying the correctness of distributed algorithms is parameterized model checking [1, 8, 21], where the number of participants is treated as a parameter and verification is conducted for any parameter value. Even though the parameterized model checking problem (PMCP) is undecidable in general [2], even for very restricted classes of systems [53], many system classes for which the problem is decidable have been identified [17, 18, 22, 25]. In particular, threshold automata (TA) [35,38,39] provide a framework for the modeling and verification of (threshold-based) distributed algorithms with Byzantine fault-tolerance, where processes communicate via shared variables to model

2

P. Eichler, S. Jacobs

message-passing, and decisions can depend on these shared variables meeting certain (parametric) threshold values. TA have been used to verify correctness of a wide range of consensus and broadcast algorithms [6, 10–12, 33, 34, 44]. A major challenge of parameterized model checking is the requirement to create a faithful model of the algorithm under consideration. Since distributed algorithms can be very complex, the resulting models can become so large that they are effectively impossible to understand or mechanically verify, even in a decidable fragment. A potential solution to this problem is to model such systems at different levels of granularity in order to keep the verification problem manageable at every separate level. Global synchronization protocols (GSPs) [29–31] are a suitable high-level model for (applications built on) distributed algorithms, abstracting from individual message passing between processes by summarizing the result as a synchronous global step.1 However, modeling an application as a GSP requires hard trade-offs in precision. In particular, the effects of Byzantine failures are not modeled explicitly, but are assumed to be completely encapsulated in synchronous steps. Moreover, modeling on different levels of precision requires additional correctness arguments connecting the different levels, which may be hard to obtain. To facilitate truly modular parameterized model checking, this work proposes a system model that supports both fine-grained modeling of individual process steps and high-level synchronous steps, with explicit support of Byzantine faults. This enables the modeling of complex applications at different levels of abstraction within the same framework, using synchronous module abstraction to replace multiple asynchronous steps by one synchronous step. We determine conditions under which parameterized model checking problems in our setting are decidable, and show how to automatically verify the correctness of a synchronous module abstraction. To the best of our knowledge, this is the first modular parameterized model checking approach that directly supports different levels of abstraction, and automatically produces a correctness argument for the abstraction. Contributions. In this paper, we introduce the model of threshold automata with synchronous actions, which is an extension of TA with global steps that are inspired by GSPs, but adapted to a setting with shared variables and Byzantine fault-tolerance (Section 3). We show that adding this type of synchronous actions to TA in general makes the PMCP undecidable, even for simple specifications like state reachability (Section 4). In Section 5, we establish a bounded model checking procedure, which becomes a decision procedure if we can statically bound the number of synchronous steps in any execution of the protocol. We argue that this will be the case for many of our intended applications. We then introduce the technique of synchronous module abstraction, which combines our bounded model checking technique at different levels of abstraction with an automatic correctness check for the abstractions (Section 6), and 1

Note that this is different from synchronous threshold automata [50–52], where processes execute in lock-step, but the algorithm is still modeled on the level of individual message passing.

Modular Parameterized Model Checking

3

demonstrate how to apply it to a case study. Finally, we report on a prototype implementation of our technique and promising experimental results on the modeling and verification of a modular king consensus algorithm (Section 7).

2

Preliminaries

Before presenting our new system model, we recapitulate the main definitions for threshold automata, an existing model for Byzantine fault-tolerant algorithms, i.e., algorithms where faulty nodes can behave maliciously. Threshold automata communicate via shared integer variables. Their transitions can be guarded with constraints over these variables and the parameters. Parameters are determined by the environment and used to, for example, represent the number of participating processes (usually n) or the bound on the number of faulty processes (usually t). Definition 1 (Environment [3]). An environment of a TA is a tuple E = ⟨Π, RC, N ⟩, where Π denotes the set of parameters, which are variables over N0 , RC is the resilience condition, a linear arithmetic formula over the parameters, and N : ΠRC → N0 a linear function, where ΠRC are the parameter valuations that satisfy RC. The resilience condition reflects assumptions on the parameters, for example bounding the number of faults. For the Byzantine fault model, a typical resilience condition is n > 3t. The function N determines the number of correct processes. If not stated otherwise we assume N(p) = n−f . Definition 2 (Threshold Automaton [36, 39]). A threshold automaton over environment E = ⟨Π, RC, N ⟩ is a tuple A = ⟨L, LI , Γ, R⟩ where L is a finite set of locations, with LI ⊆ L the initial locations, Γ the set of shared variables over N0 , 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 and upper guards. A lower guard is a constraint P|Π| q0 + i=1 qi ·pi ≤ x, with x ∈ Γ , q0 , . . . , q|Π| ∈ Z, p1 , . . . , p|Π| ∈ Π. An upper P|Π| guard is a constraint q0 + i=1 qi ·pi > x. The left-hand side of a guard is called a threshold. Algorithm Consensus → (y1 , . . . , yn )

1: Weak (x1 , . . . , xn )

∀Pi : send xi to every Pj 2 ∀Pi : yi =   0 if #0 received ≥ n − t

x0

c0 +

+, v +

+

lcnt

1

1 if #1 received ≥ n − t   ⊥ else 3 ∀Pi return yi

f∧ −t−

x1

++ +, v c 1+

v≥

f

n−

n c0 ≥ c0 < n−t ∧ c1 < n−t ∧v ≥ n−f c1 ≥ n− t−f ∧v ≥n −f

y0

y⊥

y1

Fig. 1: Weak consensus threshold automaton AW C , with Π = {n, t, f }, and RC = n > 3t ∧ t ≥ f

4

P. Eichler, S. Jacobs

Example 1. Algorithm 1 shows the weak consensus algorithm from [14,23]. Each process Pi starts with initial value xi ∈ {0, 1} and the goal is to either agree on value 0 or 1 or return ⊥ if no agreement is reached. To this end, each process sends its input value xi to all other processes and counts how many votes it received for each value. If any value gets at least n−t votes, it will be written to yi , otherwise yi is set to ⊥. The threshold automaton AW C modelling the algorithm is presented in Fig. 1. The two shared variables c0 , c1 count the votes for each value, and variable v tracks the overall number of votes. The parameter n represents the number of processes, t bounds the number of faults, and f is the actual number of faults. All (correct) processes start in x0 or x1 depending on their initial value. They then move into lcnt incrementing v and either c0 or c1 , and can transition to y0 or y1 if the corresponding variable reaches the threshold n−t−f and n−f votes have been cast. Otherwise, they can only move on to location y⊥ . Note that the TA here models only the honest processes, and parameter f is used in thresholds to model the effects of Byzantine faults. In particular, since Byzantine processes can send votes for any value, an honest process may see up to f additional votes for any value, reflected by the threshold n−t−f . Semantics of TA. The TA model assumes that N(p) honest processes are running concurrently, and that the effects of faulty processes are modeled in the guard conditions. Let un denote the unit vector, which is one at position n and zero otherwise. The semantics of TA is then defined by their counter system representation: Definition 3 (TA Counter System [4, 20, 36, 39]). The counter system of a TA A = ⟨L, LI , Γ, R⟩ under environment E = ⟨Π, RC, N ⟩ is the tuple CS(E, A) = ⟨C, CI , → − ⟩ where – C is the set of configurations. A configuration is a triple c = (k, g, p) where |L| • k ∈ N0 assigns a number of processes to each location. We use c.k[l] to denote the processes currently in location l. |Γ | • g ∈ N0 is the valuation of the shared variables. For x ∈ Γ , we use c.g[x] to denote the valuation of x in c. |Π| • p ∈ N0 is a parameter valuation such that p |= RC, i.e., RC holds after substituting each parameter with its value in p. – The set of initial configurations CI contains all initial configurations, i.e., configurations c that satisfy X ∀x ∈ Γ : c.g[x] = 0 ∧ c.k[l] = N (c.p) ∧ ∀l ∈ / LI .c.k[l] = 0 l∈LI

– The transition relation → − ⊆ C×R×C contains a transition (c, r, c′ ) (denoted r ′ as c − → c ) iff the following conditions hold: • c.p = c′ .p, i.e., the valuation of parameters did not change. • c.k[r.from] > 0 and c′ .k = c.k − ur.from + ur.to , i.e., a process moves from r.from to r.to.

Modular Parameterized Model Checking

5

• c.g |= r.φ, i.e., φ holds after replacing shared variables with values c.g • c′ .g = c.g + r.uv r

Run & Computation. The execution of a transition c − → c′ is called a step ′ from c to c using rule r. A run ρ of CS(E, A) is a sequence of configurations and rules c0 r0 c1 . . . rn−1 cn , where for every i ∈ 0, ..., n − 1 there exists a rule ri ∈ R, r such that ci − → ci+1 . We call ρ a computation if c0 ∈ CI . A configuration c is reachable if there exists a computation that ends in c.

3

Threshold Automata with Synchronous Actions

To motivate our new model with synchronous actions, we start with an example that highlights challenges when modeling a modular algorithm as a TA. Algorithm 2: Graded Consensus (x1 , . . . , xn )→((y1 , g1 ), . . . , (yn , gn )) (z1 , . . . , zn ) = WeakConsensus(x1 , . . . , xn ) 2 ∀Pi : send zi to every Pj 3 ∀Pi : ( 0 if #0 ≥ #1 yi = 1 if #1 > #0 ( 1 if max(#1, #0) ≥ n−t gi = 0 else 4 ∀Pj : return (yj , gj )

l0,0 c1

++

,v

1

z⊥

++

v++ ,v ++

c1

z1

lcnt ++

)

1∨ c0 ≥ ∧ ( n−f t n− ∧v ≥ c0 < f f ∧ v ≥ n− c0 ≥ n−t−

z0 c0

≤f

l0,1

c1 < n−t ∧ c1 ≥

(c1 ≥ 1 ∨ c 0 <f) ∧v ≥ n−f

n−

t−f

∧v

l1,0

≥n

−f

l1,1

Fig. 2: Graded-consensus threshold automaton AGC , with Π = {n, t, f } and RC = n > 3t ∧ t ≥ f

Example 2. Algorithm 2 shows the pseudocode of graded consensus [23] which uses weak consensus (Example 1) as a module. The algorithm calls weak consensus, re-shares the computed result among all processes, and decides on a value 0 or 1, depending on which value the majority accepted. Additionally, it assigns a grade to the result, which is set to 1 if at least n−t processes accepted the chosen value in the weak consensus step, and 0 otherwise. The TA AGC depicted in Fig. 2 models graded consensus except for the call to weak consensus. Instead, the initial states z0 , z1 and z⊥ correspond to the final locations y0 , y1 and y⊥ from the TA for weak consensus (Fig. 1), and a full description of graded consensus is obtained by appending AGC to AW C , identifying the respective locations (see Fig. 4a). Example 2 shows that, while the pseudo code uses weak consensus as an abstract module, the TA representation does not have an equivalent mechanism, and instead requires including a full copy of weak consensus. We will see that graded consensus is in turn a module of the king consensus algorithm, the TA for king consensus will include the full TAs of both weak and graded consensus. This leads to complex models that are difficult to check (for details see Section 7). We propose a different approach that allows us to abstract modules into synchronous steps and thus reduce the complexity of the overall model.

6

P. Eichler, S. Jacobs

3.1

Formal Model

The synchronous actions we introduce are inspired by broadcast protocols [19,22] and global synchronization protocols (GSPs) [29, 30]. A threshold automaton with synchronous actions is a TA that, in addition to the regular asynchronous transitions, can have synchronous actions where all processes take a step at the same time. We define a finite set of global actions Σ. Definition 4 (Threshold Automaton with Synchronous Actions). A threshold automaton with synchronous actions (TAS) is a tuple A = ⟨L, LI , Γ, R, G⟩, where L, LI , Γ, R are as in Definition 2 and G contains for every a ∈ Σ one global rule (a, Send, Recv, type, low, high), where – Send is a finite set of local send transitions (li , ai !!, li′ ), with 0 ≤ i < k for some k ∈ N. – Recv is a finite set of local receive transitions of the form (l, a??, l′ ). – type is either each or max. Intuitively, if type is each, then each sending transition needs to be taken by at least one process, and if it is max then the maximum number of available processes need to take the sending transitions. – the lower bound low and the upper bound high are given as thresholds (as defined in Definition 2) and define (in addition to type) the minimum and maximum numbers of senders that can execute a concurrently. For a given action a ∈ Σ, we will refer to the components of the global rule as α a.Send, a.Recv, etc. and write l − → l′ if there exists a global rule with some action ′ a such that (l, ai !!, l ) ∈ a.Send or (l, a??, l′ ) ∈ a.Recv. Local send transitions and local receive transitions will also be called synchronous transitions. Labels ai !! will be called local send actions, and a?? local receive actions. To separate them from the global rules, we will refer to rules from R as local ϵ rules and write l → − l′ if there exists r ∈ R with r.from = l and r.to = l′ . Example 3. Fig. 3 depicts a model of the z!!, mz!!, z?? weak consensus algorithm from Example 1 y0 mz?? using only synchronous actions. Global z??, x0 mz!!, b!!, mo ?? action z is an each action with local sendy⊥ ing action z!! which transitions from x0 ? !!, mz??, b? mo x1 to y0 and local receiving actions z?? that o??, mo?? y1 transition to y0 . The action z is enabled if o!!, mo!!, o?? at least n−t−f (z.low) processes start in x0 and when z is executed, all processes move to y0 . Action z intuitively represents Fig. 3: TAS AW C of Algorithm 1 acceptance of value zero by all processes. with z, o, b each actions with = o.low = n−t−f , The action o is the analog action for ac- z.low b.low = 1, b.high = n−t−f −1 cepting value one. and mz, mo max actions with Actions mo and mz represent an execution where no value has n−t, therefore the mo.low = mz.low = n−t−f and upper bound, but enough such that with mz.high = mo.high = n−t−1. votes by the faulty processes some process could accept a value. The action b

Modular Parameterized Model Checking

7

represents the case where no value can be accepted (even with votes from faulty processes). Therefore, all processes must transition to y⊥ . Note that, in the depicted automaton, not every location has a receive action for every global action. This will be discussed later in more detail. Semantics of TA with Synchronous Actions. In a TAS A, the transition relation from Definition 3 is extended with global transitions (c, a, c′ ) for a ∈ Σ a (denoted as c − → c′ ) that satisfy the following conditions: 1. for each (li , ai !!, li′ ) ∈ a.Send, nai !! ∈ N0 is a send acceleration factor that specifies how many processes take the given send transition, 2. for each r = (l, a??, l′ ) ∈ a.Recv, nr is a receive acceleration factor that specifies how many processes take the given receive transition, 3. for all locations l ∈ L, X X c.k[l] = nai !! + nr , (l,ai !!,l′ )∈a.Send

r=(l,a??,l′ )∈a.Recv

i.e., the number of outgoing senders and outgoing receivers must sum up to the number of processes currently in l. Intuitively, this means that every process needs to execute either a send or receive action. 4. X a.low ≤ nai !! ≤ a.high, 0≤i<k

i.e., the number of senders is inside the action’s lower and upper bound, 5. if type is each thenP nai !! ≥ 1 for 0 ≤ i < k, and P P 6. if type is max then nai !! = min(a.high, c.k[l])∧ nai !! ≥ 1, i.e., (l,ai !!,l′ )∈a.Send

0≤i<k

0≤i<k

sending transitions are taken by the maximum number of available processes within the upper bound a.high. 7. for all l ∈ L, X X c′ .k[l] = nai !! + nr , (l′ ,ai !!,l)∈a.Send

r=(l′ ,a??,l)∈a.Recv

8. c′ .g = c.g and c′ .p = c.p, i.e., shared variables and parameters are unchanged. a

For a given transition c − → c′ , we will in the following use N ! to denote the set of send acceleration factors N ! = {nai !! | (li , ai !!, li′ ) ∈ a.Send} and analogously N ? = {nr | r ∈ a.Recv}. Such a transition on a synchronous action is also called a synchronous step. ϵ r Analogously, we will write c → − c′ if there exists a rule r ∈ R and c − → c′ and refer to it as an asynchronous step. Remark 1 (Undefined Receive Transitions). Note that the semantics is blocking if a process is in a location that does not have a receive transition for the given action (and this process does not take a sending action). This follows from the third condition, which requires all processes to take some local actions.

8

4

P. Eichler, S. Jacobs

(Un)Decidability of Model Checking

In this section, we examine the complexity of the PMCP for TAS. To this end, we first define different problem classes and recap existing complexity results for models closely related to TAS. To characterize different classes of the PMCP, we use a variant of cardinality constraints [13, 16]. Definition 5 (Cardinality Constraint [13, 16]). A cardinality constraint φ is a formula in the following grammar, with l ∈ L and x ∈ N: φ ::= #l ≥ x | #l = 0 | φ ∧ φ | φ ∨ φ The satisfaction of a cardinality constraint by a configuration c is defined in the natural way, e.g., c |= #l ≥ x iff c.k[l] ≥ x. Definition 6 (Cardinality Reachability Problem [13,16]). Given a counter system of a threshold automaton (with synchronous actions) CS(E, A) and cardinality constraint φ, the cardinality reachability problem (CRP) asks whether a configuration c with c |= φ is reachable in the system. We denote by CC[≥ x, = 0] the class of all cardinality constraints, and by CC[≥ x] the class of cardinality constraints in which atomic propositions are only of the form #l ≥ x. In [4], specifications from CC[≥ x] are called (general) parameterized coverability specifications, and those from CC[≥ x, = 0] parameterized reachability specifications. Intuitively, a parameterized coverability specification specifies a set of locations and asks whether there exists a run that reaches a configuration such that in all the specified locations there is at least one process. In a parameterized reachability constraint, one can additionally specify a set of locations that need to be empty in the target configuration. PMCP for TAs. For threshold automata (according to Definition 2), problems of the class CC[≥ x, = 0] have been proven NP-complete [3, 4]. 4.1

Undecidability for Synchronous Actions

We now investigate decidability of the CRP for TAS. As mentioned in Remark 1, in our semantics an action is blocked when there are processes that are not assigned to a send action and that cannot execute any local receive action. This blocking semantics can be seen as equivalent to the addition (see Appendix A) of a conjunctive guard, which is known to make safety problems undecidable for systems with synchronous (broadcast) steps [18]. It follows that problems of the class CC[≥ x] are undecidable for TAS under the blocking semantics. A natural question is whether this undecidability result can be circumvented by relaxing the semantics to be non-blocking, or by restricting TAS such that blocking cannot occur. In the following we show that undecidability even arises when blocking cannot occur (and therefore also under a non-blocking semantics). For a given TAS we say that receive actions are total if every location l has at least one outgoing rule with receive action a?? for every action a ∈ Σ.

Modular Parameterized Model Checking

9

Theorem 1. The CRP for CC[≥ x] is undecidable for TA with synchronous actions, even if receive actions are total. Proof (Sketch). We prove undecidability by reducing from the halting problem in two counter machines (2CM) [43]. For the reduction, we reuse the construction from [22, Section 5], which proved that liveness properties in broadcast protocols are undecidable. First note that an action in a broadcast protocol is equivalent to an each action with upper and lower bound 1. Therefore, we can utilize the same construction, replacing broadcast actions with an equivalent each action. By the definition of broadcast protocols in [22], all receives are total. The construction simulates state changes, increments and decrements of the 2CM faithfully by letting one process simulate the control state of the 2CM and all others simulate a unary encoding of the two counter values. Only zero tests are not simulated faithfully: instead of blocking when the given counter is nonzero, the simulation moves all processes representing a 1 in the unary encoding of the counter to a sink location. Building on this idea, in a TAS we can implement a check whether all zero tests along a run were faithful. Let the parameter n, and therefore N(p) = n denote the number of processes executing the system. We add a new max action check which on every location except the sink location, has a send and receive self-loop transition. The sink location only has a receive self-loop (making all receives total again). Additionally, we add an auxiliary location that can be reached from the halting location with local send action check!!. We set the upper and lower bound of the action check to check.low = check.high = n. Since an execution of check requires all processes to be in a location besides the sink location, it can only be executed if no process ever moved to the sink location. Therefore, the auxiliary location can be reached iff the 2CM can reach a halting state. It follows that problems of the class CC[≥ x] are undecidable. ⊔ ⊓

5

Recovering Decidability

We have shown that even a very restricted class of the CRP is undecidable in presence of synchronous actions. In the following we introduce a bounded model checking (BMC) procedure that checks correctness up to a bounded number of synchronous steps. Afterward, we introduce a class of TAS with a static bound on the number of synchronous steps that can appear on any run, recovering decidability for this class. 5.1

Bounded Model Checking

To obtain a BMC procedure, we encode the reachability relation of a TAS into SMT constraints. We first recapitulate a similar approach for TA that we build upon.

10

P. Eichler, S. Jacobs

Recap: Reachability in TA [3]. The encoding presented in [3] relies on the observation that shared variables can only increase along a run of a TA. Consequently, on any run of a TA, lower guards can only become enabled along an execution, and when enabled, they remain enabled forever. Similarly, upper guards can only become disabled, and then remain disabled forever. It follows that on any run of a TA with k distinct guards, there can be at most k steps where a guard changes its valuation. Such a step is referred to as a context switch, and the set of enabled guards is referred to as a context. Note that a context determines which rules are currently enabled in a run. The SMT encoding then encodes all possible executions between context switches and combines it with an encoding of an explicit step where one guard changes its valuation. The result is a formula ϕasyn (c, c′ ) (called ϕreach in [3]) in Presburger arithmetic, which is true if and only if c′ is reachable from c in threshold automaton A. SMT Encoding for Synchronous Steps. To encode a single synchronous a step c − → c′ with acceleration factors N !, N ?, first let ϕacc (c, c′ , N !, N ?, a) be a straightforward encoding of conditions 3, 4 and 7 from the definition of the semantics of TAS (see Section 3.1). The full formula can be found in Appendix B.1. Then a synchronous step of type each, with arbitrary acceleration factors, additionally requires that each sending action is executed by at least one process. This can be encoded as ! ^ ϕeach (c, c′ , a) := ∃N !, N ?. n ≥ 1 ∧ ϕacc (c, c′ , N !, N ?, a) n∈N !

For steps of type max, the maximum number of available senders has to execute the action. We encode this as X ϕmax (c, c′ , a) :=∃N !, N ?.ϕacc (c, c′ , N !, N ?, a) ∧ N! ≥ 1    X X X ∧  N ! = a.high ∨  N ! = c.k[l] l∈{l|(l,ai !!,l′ )∈a.Send} a

ϕeach and ϕmax evaluate to true for (c, c′ , a) if and only if c − → c′ is a valid synchronous step of the given type. Both formulas can be combined into ϕsync , which intuitively allows selecting one action from all potential actions. To distinguish which action has been executed and to ensure that at most one action is executed, we introduce another set of variables S = {sa | a ∈ Σ}. X ^ ϕsync (c, c′ ) := ∃S. sa ≤ 1 ∧ (sa =1 ⇒ ϕeach (c, c′ , a)) a∈Σ

a∈{a∈Σ|a.type=each}

^

∧

(sa =1 ⇒ ϕmax (c, c′ , a))

a∈{a∈Σ|a.type=max}

! ∧

X a∈Σ

sa = 0 ⇒

^ l∈L

′

c.k[l] = c .k[l]

∧ c.g = c′ .g ∧ c.p = c′ .p

Modular Parameterized Model Checking

11

ϕsync is constructed such that an action a is chosen iff sa is set to one, and either ϕeach or ϕmax has to hold, depending on the type of a. Note that ϕsync also allows no action to be selected, and then requires that processes remain in their locations. This will become useful, as an encoding with k instances of ϕsync can directly represent runs with k or fewer synchronous steps. Combining Synchronous and Asynchronous Steps. Now we combine our encoding for synchronous steps with the encoding for reachability of asynchronous steps. Let A be a threshold automaton with synchronous actions and kA = k +1, where k is the number of distinct guards that appear in A. For a bound ks ∈ N on the number of synchronous steps and for configurations c, c′ of A, we define ϕreach (ks , c, c′ ) := ∃c0 , . . . , cks , c10 , . . . , ckkA . c = c0 ∧ c′ = ckkA s s ^  kA kA ϕasyn (ci , ci ) ∧ ϕsync (ci , ci+1 ) ∧ 0≤i<ks

∧ ϕasyn (cks , ckkA ) s By construction, ϕreach evaluates to true if configuration c′ is reachable from c within ks synchronous steps. Note that ϕreach allows for up to kA context switches between every synchronous step. This is because without additional arguments, it is not possible to infer how context switches interleave with synchronous steps, see Appendix B.2 for more details. A more formal correctness argument for the SMT encoding can be found in Appendix B.3. Note that ϕreach is still a formula in existential Presburger arithmetic. 5.2

Bounded Synchronous Steps

While bounded model checking can be useful in practice, it cannot certify correctness. To address this limitation, we introduce a class of TAS for which a static bound on the number of synchronous steps across all runs exists. This class is inspired by the observation that modules often represent isolated steps that are executed by all processes before the system can make further progress. This is, for example, the case for the weak consensus module within graded consensus (Examples 1 to 3). We therefore partition the set of locations into layers, such that every synchronous step moves all processes into the next layer. Definition 7 (Layered TAS). A TAS A is layered if there exists a partition P = {L1 , . . . , Lm } or P = {L1 , . . . , Lm , L⊘ } of the set of locations L, and for every Li , – local rules cannot transition toSa lower layer, i.e., for every l ∈ Li , l′ ∈ L ϵ s.t. l → − l′ , it holds that l′ ∈ Lj ∪ L⊘ . j∈i,...,m

– every global rule must transition to a higher layer or L⊘ , i.e., for every S α l ∈ Li , l′ ∈ L s.t. l − → l′ , it must hold that l′ ∈ Lj ∪ L⊘ . j∈i+1,...,m

– for all locations in L⊘ (if any), all outgoing transitions are synchronous α receive self-loops, i.e., for all l ∈ L⊘ , l′ ∈ L with l − → l′ it holds that l = l′ and α = a?? for some a ∈ Σ. We also call L⊘ the sink layer.

12

P. Eichler, S. Jacobs

We define the number of layers as |P|. Regular TA are by definition layered, with a single layer. Note that Definition 7 requires all local receive actions to transition to a higher layer or the sink layer, which implies that receive self-loops are only allowed in the sink layer. We will show in Section 7 that many synchronous abstractions are layered. We can automatically check whether a given TAS is layered, and compute the layers if it is. The following result provides the theoretical basis of the algorithm, more details and a proof of the lemma are provided in Appendix B.4. Lemma 1. A TAS A is layered iff there does not exist a synchronous transition within any SCC of the underlying graph, except for the synchronous receive selfloops in sink locations. Observing that every synchronous step moves all processes either to a strictly higher layer, or to L⊘ , and that locations in L⊘ do not have send actions, we get a bound on the number of synchronous steps in any run of a layered TAS. Lemma 2. Let A be a layered TAS with |P| = m. Then every run of A has at most m − 1 synchronous steps. Since the number of synchronous steps in a layered TAS is bounded, our BMC procedure instantiated with the proper bound is a decision procedure for the CRP. Theorem 2. Problems in CC[≥ x, = 0] for a layered TAS are decidable in NP. Proof (Sketch). Decidability follows from Lemma 2 and correctness of ϕreach . The complexity bound follows from the fact that ϕreach is a polynomial-size formula in existential Presburger arithmetic which can be checked in NP [9, 24, 27, 49].

6

Modular Models & Replacement

The idea of synchronous module abstraction is to reduce the complexity by replacing modules with a concise synchronous abstraction. Before applying this technique we first formally define the notion of replacement. 6.1

Replacement Operations

In the following, we fix an environment E in which all automata are executed. Then for a TAS a replacement operation R is defined by – Lrm ⊆ L, the set of locations to remove from the automaton, – Ladd the set of locations to add to the automaton, – the set of rules Radd and global rules Gadd to add, – and the set of shared variables to remove2 Γrm . 2

Since none of our examples requires it, we do not allow the addition of shared variables. This could be supported at the cost of notational complexity.

Modular Parameterized Model Checking

13

For a replacement R, we define the set of entry locations Lent as Lent = {l ∈ ϵ α L \ Lrm | ∃l′ ∈ Lrm . l → − l′ or l − → l′ }. Intuitively, it contains the locations with transitions into the replaced locations. Analogously, we define the exit locations ϵ α Lext = {l′ ∈ L \ Lrm | ∃l ∈ Lrm . l → − l′ or l − → l′ }, which describe locations with transitions out of the replaced locations. To be well-defined, variables in Γrm cannot be referenced by any rule kept by the replacement, and initial locations cannot be removed, i.e., LI ∩ Lrm = ∅. Definition 8. For a TAS A = ⟨L, LI , Γ, R, G⟩ and replacement R = ⟨Lrm , Ladd , Radd , Gadd , Γrm ⟩, the resulting TAS after applying replacement R, denoted as A
R = ⟨L′ , L′I , Γ ′ , R′ , G ′ ⟩ is defined as – L′ = (L \ Lrm ) ∪ Ladd and L′I = LI – Γ ′ = Γ \ Γrm – R′ = Radd ∪ {r ∈ R | r.from ∈ / Lrm ∧ r.to ∈ / Lrm }, and / Lrm }. – G ′ = Gadd ∪ {(a, , , , , ) ∈ G | ∀(l, , l′ ) ∈ a.Send ∪ a.Recv. l, l′ ∈

AW C

AGC y0

x0

...

lcnt x1

...

...

...

...

...

...

y1

z!!, mz!!, z?

l0,0

...

y⊥

AW C

lcnt

... ... ... ...

x0 l0,1

AGC

?

?? , mz z?? mz!!, b!!,

y0 ... mo??

y⊥ ??, b??

l1,0 x1 l1,1

mo!!, mz o?? , mo ??

o!!, mo!!, o?

(a) Full graded consensus as TA. Locations in Lrm are depicted in gray.

l0,0 ... ...

y1

lcnt

... ... ... ...

l0,1 l1,0 l1,1

?

(b) Graded consensus after replacement. New transitions are depicted in blue.

Fig. 4: Replacement of weak consensus (AW C , Fig. 1) in graded consensus (AGC , Fig. 2) by its synchronous model (AW C , Fig. 3). Gadd marked in blue, Lent and transitions into the module in red, Lext and transitions out of the module green.

Example 4. Fig. 4 depicts the replacement of weak consensus by its synchronous abstraction in graded consensus (from Example 2). The replacement removes the shared variables Γrm = {c0 , c1 , v}, the counting location Lrm = {lcnt }, and 5 local rules, all of which are internal to the weak consensus TA AW C . It adds the 5 global rules from AW C , but no locations or local rules. 6.2

Faithful Replacements

Replacements allow us to create automata with entirely different behavior than the original automaton. To be practical for model checking, a replacement needs to preserve properties of interest. To this end, we introduce the notion of a reachability-preserving replacement: Definition 9 (Reachability-Preserving Replacement). For TAS A, a replacement operation R = ⟨Lrm , Ladd , Radd , Gadd , Γrm ⟩ is reachability-preserving

14

P. Eichler, S. Jacobs

(rp) if for every reachable configuration c with ∀l ∈ Lrm . c.k[l] = 0, there exists a reachable configuration c′ in A
R with c.p = c′ .p, ∀x ∈ Γ \ Γrm . c.g[x] = c′ .g[x], ∀l ∈ L \ Lrm . c.k[l] = c′ .k[l] and ∀l ∈ Ladd . c′ .k[l] = 0. It is strongly reachability-preserving (srp) if the other direction holds too. Intuitively, Definition 9 requires that for any reachable configuration where no process is in Lrm , an equivalent configuration must be reachable after the V replacement. It follows that if a configuration satisfying φ ∧ l∈Lrm #l = 0, for someVcardinality constraint φ, is reachable in A, then a configuration satisfying φ ∧ l∈Ladd #l = 0 is reachable in A
R. The restriction that locations Lrm must be empty is necessary since a synchronous step is executed by all processes, whereas asynchronous steps move one process at a time. Therefore, asynchronous steps create many intermediate configurations, which the synchronous action abstracts from. Note that a reachability-preserving replacement can add new behavior, i.e., it allows A
R to be an overapproximation of A. Overapproximations can be easier to check, as we will see in Section 7, and if an overapproximation is safe, the original system is also guaranteed to be safe. However, reported counterexamples might not be valid behavior of A. The stronger notion of strongly reachability preserving-replacement prevents such spurious counterexamples. Whether a replacement is reachability preserving can again be expressed by an SMT formula. Theorem 3. Let A and A
R be layered TAS with ks = |PA |−1 and ks′ = |PA
R |−1. Then R is reachability-preserving iff the following formula holds:  l ^ c.k[l] = 0 ϕrp (A, R) := ∀cI , c ∈ CA . ϕI (cI ) ∧ ϕreach (ks , cI , c) ∧ Lrm ′ ′ ′ ′ ′ ⇒ ∃cI , c ∈ CA
R . ϕI (cI ) ∧ ϕreach (ks , cI , c′ ) ∧ c.p = c′ .p

∧

l ^

c.k[l] = c′ .k[l] ∧

L\Lrm

l ^ Ladd

c′ .k[l] = 0 ∧

x ^

 c.g[x] = c′ .g[x]

Γ \Γrm

Here, ϕI (c) denotes the formula that evaluates to true iff c is an initial configuration. The details of ϕI and an encoding for strongly reachability-preserving can be found in Appendix C.1. If A or A
R are not layered, ϕrp can only check that the replacement is reachability-preserving for a bounded length of runs. Note that the SMT formula ϕrp contains a quantifier alternation. Deciding the validity of such a formula is coNEXP-complete [26] .3 In the following we will present techniques and conditions that enable a practical use of replacements despite this worst-case complexity, and Section 7 will show that our approach is efficient on practical examples. 3

ϕrp contains quantifier alternation ∀∃ (with no free variables). The formula is therefore in Π2 and its negation in Σ2 . Since deciding a formula in Σ2 is NEXPcomplete [26, Thm. 1], it follows that deciding formulas in Π2 is coNEXP-complete.

Modular Parameterized Model Checking

6.3

15

Practical Synchronous Module Abstraction

Formula ϕrp contains a quantifier alternation and encodes the full reachability relations of A and A
R, making it inefficient to check if used naively. However, under the following conditions the checks can be done locally on the replaced part of the automaton: (i) Lent = LI , (ii) processes can pass through the replacement only once, (iii) R does not modify shared variables used in the rest of A, and (iv) Gadd ∩ GA = ∅. More details can be found in Appendix C.2. When checking ϕrp locally, the required reachability checks can be much simpler, and the quantifier alternation can effectively disappear: if Ladd = Radd = ∅, then the exit locations will always be reached after a single synchronous step. In this case, the values of all existentially quantified configurations in ϕrp are fixed by the universally quantified configurations, and ϕreach (ks′ , c′I , c′ ) becomes a finite disjunction over Gadd . While these conditions are a significant restriction, they are satisfied in Example 4 and most of the cases considered in Section 7. This is not surprising, as a standard use of such modules is to replace a part of A by something that amounts to a function call in the algorithm, and that can be modeled as a single synchronous step.

7

Experimental Evaluation

Applying Synchronous Module Abstraction. To evaluate our technique, we study the king consensus algorithm [5] as presented in [23]. The algorithm is split into three modules: weak consensus (Algorithm 1), graded consensus (Algorithm 2), and lastly king consensus (presented in detail in Appendix D.1). To verify the algorithm, we start at the lowest layer, the weak consensus algorithm, and construct a TA AW C (Fig. 1). After verifying its desired properties (using the procedure from Section 5), instead of directly proceeding with the next module, we construct a synchronous abstraction AW C . We verify that AW C constitutes a faithful replacement of AW C (via Theorem 3), ensuring that AW C is an overapproximation of AW C and can be used as a module when constructing the automaton for graded consensus. Optionally, we can check whether AW C is strongly reachability preserving to avoid spurious counterexamples later. In this case, it is—if it was not, we could refine the model further. We continue this approach, next using AW C as a module in the definition of graded consensus, verify its properties and obtaining a synchronous abstraction that is in turn used as a module in the definition of king consensus. We will see in the following that this synchronous module abstraction technique leads to much smaller models, which additionally can be checked much quicker. Models. For our evaluation, we also construct the full TA models for each algorithm. All automata are encoded in the file format of ByMC [37], extended with constructs for synchronous actions: AW C (Fig. 1) is encoded in weak.ta, AW C (Fig. 3) in weak.sta, and the combination of AW C and AGC (Fig. 4b) in graded-wc.sta. For graded consensus, we construct two different synchronous

16

P. Eichler, S. Jacobs

abstractions, an overapproximation (graded-over.sta) and an exact representation (graded-exact.sta). Additional details can be found in Appendix D.1. Table 1: Model size for synchronous and asynchronous algorithm models. “over” denotes an overapproximation and “exact” an exact representation of an algorithm. |L|

TA |R|

Weak 6 Graded (over) 11 Graded (exact) 11 King 13

5 12 12 22

Algorithm

TAS |L| |G| 5 6 7 4

5 5 7 3

Table 2: Model Checking on TAS (.sta), TA (.ta), timeout 30min Model weak.ta weak.sta graded.ta graded-wc.sta graded-over.sta graded-exact.sta king.ta king-gc-over.sta king-gc-exact.sta king.sta

Time [s] Mem. [MiB] 0.17 0.06 8.73 2.49 0.04 0.07 41.39 0.46 1.23 0.03

37.2 34.1 80.9 62.2 35.0 35.4 204.6 50.5 63.8 34.6

Model Complexity. We compare the size of the respective models in Table 1. We observe that the synchronous abstractions (in column TAS) have significantly fewer locations, e.g., king consensus shrinks from 13 locations to just 4. Also the number of synchronous actions required is usually small and all synchronous models are layered. In summary, the synchronous abstractions are far less complex than their asynchronous counterparts. Model Checking Performance. We implemented a prototype of the decision procedure presented in Section 5.1 and checked correctness properties of every algorithm, encoded as reachability constraints. As an example, for weak consensus we check weak consistency: if some honest process accepts 0 or 1, other honest processes can only accept the same value or move to y⊥ , corresponding to unreachability of constraint φ = y0 ≥ 1 ∧ y1 ≥ 1. Table 2 presents the runtime results of our prototype (see Appendix D.2 for more details on the setup). Overall, checking synchronous modules, or models based on synchronous abstraction, is significantly faster than checking the full TA. For example, the king consensus TA is checked in 41s compared to just 0.03s on the fully synchronous version, and 1.2s when the graded consensus module is replaced by an exact synchronous abstraction. We can also see that using an overapproximation (that still satisfies all correctness properties) can further improve the performance dropping the runtime from 1.2s for king-gc-exact to 0.5s on king-gc-over. Reachability-Preserving Checks. Table 3 presents the runtime results for verifying that the synchronous abstractions are faithful. All reachability-preserving checks terminate within one minute, most cases in under 15s. Therefore, we argue that these checks even with their theoretical worst case complexity, are quite efficient in practice. Although not necessary for checking our safety properties, we also evaluate performance on checking whether a replacement is strong reachabilitypreserving takes significantly longer. We see that this takes significantly longer, with one case running into a timeout. Furthermore, we note that the benefits of our synchronous module abstraction also show in the reachability-preserving

Modular Parameterized Model Checking

17

Table 3: Runtime for reachability-preserving checks with timeout of 30min Reachability-preserving Original

Replacement

weak.ta weak.sta graded.ta graded-wc.sta graded.ta graded-over.sta graded.ta graded-exact.sta graded-wc.sta graded-over.sta graded-wc.sta graded-exact.sta king.ta king-gc-over.sta king.ta king-gc-exact.sta king.ta king.sta king-gc-over.sta king.sta king-gc-exact.sta king.sta

Strongly reachability-pres.

holds Time [s] Mem. [MiB] holds Time [s] Mem. [MiB] ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

0.23 0.35 11.25 12.39 2.50 2.06 10.77 13.40 52.49 0.67 3.04

43.4 45.4 99.2 108.4 69.6 68.6 98.0 113.5 307.9 56.6 79.7

✓ ✓ ✗ ✓ ✗ ✓ ✗ ✓ ✓ ✓

0.72 45.1 1.00 46.0 18.54 103.5 61.65 147.9 5.19 77.8 7.91 102.4 18.61 98.5 66.24 159.7 timeout 2.59 65.4 5.76 95.8

checks: while checking directly whether king.sta is an exact abstraction of king.ta times out, the checks from king.ta to king-gc-exact.sta and from king-gc-exact.sta to king.sta succeed, implying that king.sta is an exact abstraction of king.ta. Finally, note that the models that are overapproximations are not strong reachability-preserving, as expected. Summary. We have seen that our synchronous modular abstraction technique can drastically improve model checking performance while also reducing the complexity of the individual models. We argue that our technique therefore makes parameterized model checking significantly more practical, even though the synchronous abstraction currently needs to be designed manually.

8

Related Work

Parameterized Model Checking. The fully automatic verification of concurrent system models with a parametric number of processes is a long-standing and active area of research [1,8,21]. Many approaches use automata-based models, with different types of communication such as pairwise synchronization [25], broadcast [19, 22], or guarded transitions [17, 18]. An inspiration for our synchronous actions are global synchronization protocols, which combine a generalization of broadcast synchronization with guarded transitions [29, 30]. However, like the other models mentioned so far, GSPs do not support the modeling of Byzantine fault-tolerant algorithms. Threshold Automata. An important system model that directly supports modeling and verification of Byzantine fault-tolerant algorithms are threshold automata [32, 35, 38, 40]. Notably, threshold automata have also received significant tool support, first with the model checker ByMC [34, 37], then an SMTbased implementation by Balasubramanian et al. that lifted some restrictions of ByMC [3], and recently with the model checker TACO [15] that re-implements existing techniques along with new extensions of the TA model [4].

18

P. Eichler, S. Jacobs

The SMT-based approach of Balasubramanian et al. is of particular interest to us, as the technique we present is also based on an SMT encoding, re-uses some of their constraints and extends the approach to support synchronous actions. Synchronous steps in TA have been considered before in the model of synchronous threshold automata (STA) [50–52], which are TA in which processes execute all transitions in lockstep. In contrast, our model allows to mix synchronous and asynchronous steps, which is essential for the modular verification approach we present. Another model derived from TA and close to ours are layered automata (LTA) and their abstraction called guard automata [7]. LTA require a user to divide an algorithm into layers and require each transition to move a process into the next layer. For cyclic LTA, which are LTA that repeat a finite sequence of layers forever, so-called guard automata can be constructed as overapproximations. Thus, in contrast to our approach, the framework does support algorithms over multiple rounds. However, the abstraction is not complete, therefore it might report spurious counterexamples, and similar to STA, communication via actions is not supported. The tool PyLTA [55] implements a decision procedure for LTL properties on guard automata.

9

Conclusion

In this work we have introduced threshold automata with synchronous steps, a computational model that combines asynchronous actions from threshold automata with expressive global synchronous actions. While the addition of synchronous steps results in an undecidable PMCP in general, we introduced a bounded model checking procedure. Moreover, we identified a subclass of automata for which a static completeness bound can be computed, making the PMCP decidable for this subclass. The addition of synchronous actions enables our new technique of synchronous module abstraction: instead of combining modular algorithm descriptions into complex monolithic models, our technique allows the designer to replace modules by concise synchronous abstractions. We implemented our techniques in a prototype, and demonstrated its effectiveness on the example of the king consensus. Using synchronous module abstraction, we reduced the model complexity and the model checking time significantly. We believe that this technique can be even more effective on larger, more complex distributed algorithms. Therefore, in the future we plan to evaluate our techniques systematically on more complex algorithms, closer to real-world distributed systems. In addition, we plan to extend our line of work in two directions: we will investigate the automatic synthesis of the abstractions from the module description and its correctness properties, and we hope to make progress towards supporting multi-round algorithms, potentially by utilizing similar overapproximations as the line of work on guard automata [7].

Modular Parameterized Model Checking

19

AI Usage AI has been used in the creation of this work. Specifically, it has been used to review drafts of this paper and in the prototype implementation, for example, to generate test cases from natural language inputs, but also to implement a GUI which we consider supplementary to our artifact. More details will be provided in the artifact. Models that have been used: Deepseek-v4-flash, Deepseek-v4.1-flash, GLM-5.3-flash, GLM-5.3, hosted on Ollama cloud; Fable 5.1, Opus 5.5 provided by Anthropic. Acknowledgments. We thank Julian Loss for initial discussions on modularly defined distributed algorithms. P. Eichler carried out this work as a member 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 497132954. Disclosure of Interests. The authors have no competing interests to declare that are relevant to the content of this article.

References 1. Abdulla, P.A., Sistla, A.P., Talupur, M.: Model checking parameterized systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 685–725. Springer (2018). https://doi.org/10.1007/ 978-3-319-10575-8_21 2. Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986). https://doi.org/10.1016/ 0020-0190(86)90071-2 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. 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 5. Berman, P., Garay, J.A., Perry, K.J.: Towards optimal distributed consensus (extended abstract). In: 30th Annual Symposium on Foundations of Computer Science, Research Triangle Park, North Carolina, USA, 30 October - 1 November 1989. pp. 410–415. IEEE Computer Society (1989). https://doi.org/10.1109/ SFCS.1989.63511 6. Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: Fokkink, W.J., van Glabbeek, R. (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

20

P. Eichler, S. Jacobs

7. 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, Virtual Conference, August 24-27, 2021. 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 8. 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 9. Borosh, I., Treybig, L.B.: Bounds on positive integral solutions of linear diophantine equations. vol. 55, pp. 299–304 (1976). https://doi.org/10.2307/2041711 10. Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824–840 (1985). https://doi.org/10.1145/4221.214134 11. 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 12. 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 13. Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012) 14. Dolev, D.: The byzantine generals strike again. J. Algorithms 3(1), 14–30 (1982). https://doi.org/10.1016/0196-6774(82)90004-9 15. Eichler, P., Baumeister, T., Sakr, M., Dowlati, M.K., Völp, M., Jacobs, S.: TACO: A toolsuite for the verification of threshold automata. In: Darulova, E., Lin, A.W., Rümmer, P. (eds.) Computer Aided Verification - 38th International Conference, CAV 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings, Part II. Lecture Notes in Computer Science, vol. 16683, pp. 403–417. Springer (2026). https://doi.org/ 10.1007/978-3-032-32526-6_19 16. 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 17. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D.A. (ed.) Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1831, pp. 236–254. Springer (2000). https://doi.org/10.1007/10721959_19 18. Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings. pp. 361–370. IEEE Computer Society (2003). https://doi. org/10.1109/LICS.2003.1210076

Modular Parameterized Model Checking

21

19. Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinitestate systems. In: Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998. pp. 70–80. IEEE Computer Society (1998). https://doi.org/10.1109/LICS.1998.705644 20. Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME ’99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1703, pp. 142–156. Springer (1999). https://doi.org/10.1007/3-540-48153-2_12 21. Esparza, J.: Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In: Mayr, E.W., Portier, N. (eds.) 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, Lyon, France, March 5-8, 2014. LIPIcs, vol. 25, pp. 1–10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014). https://doi.org/10.4230/LIPICS.STACS.2014.1 22. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 25, 1999. pp. 352–359. IEEE Computer Society (1999). https://doi.org/10.1109/ LICS.1999.782630 23. Fitzi, M., Maurer, U.M.: From partial consistency to global broadcast. In: Yao, F.F., Luks, E.M. (eds.) Proceedings of the Thirty-Second Annual ACM Symposium on Theory of Computing, May 21-23, 2000, Portland, OR, USA. pp. 494–503. ACM (2000). https://doi.org/10.1145/335305.335363 24. Gathen, J., Sieveking, M.: A bound on solutions of linear integer equalities and inequalities. Proceedings of The American Mathematical Society - PROC AMER MATH SOC 72, 155–155 (10 1978). https://doi.org/10.2307/2042554 25. 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 26. Haase, C.: Subclasses of presburger arithmetic and the weak EXP hierarchy. In: Henzinger, T.A., Miller, D. (eds.) Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSLLICS 2014, Vienna, Austria, July 14 - 18, 2014. pp. 47:1–47:10. ACM (2014). https://doi.org/10.1145/2603088.2603092 27. Haase, C.: A survival guide to presburger arithmetic. ACM SIGLOG News 5(3), 67–82 (2018). https://doi.org/10.1145/3242953.3242964 28. 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 29. Jaber, N., Jacobs, S., Wagner, C., Kulkarni, M., Samanta, R.: Parameterized verification of systems with global synchronization and guards. 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 I. Lecture Notes in Computer Science, vol. 12224, pp. 299–323. Springer (2020). https: //doi.org/10.1007/978-3-030-53288-8_15 30. 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

22

P. Eichler, S. Jacobs

31. Jaber, N., Wagner, C., Jacobs, S., Kulkarni, M., Samanta, R.: Synthesis of distributed agreement-based systems with efficiently-decidable verification. 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. 289–308. Springer (2023). https://doi.org/10.1007/978-3-031-30820-8_19 32. 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 2023, 2013. pp. 201–209. IEEE (2013), https://ieeexplore.ieee.org/document/ 6679411/ 33. 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 34. 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 35. 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 36. 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 37. 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 38. 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 39. 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 40. 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,

Modular Parameterized Model Checking

23

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 41. 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 42. 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 43. Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1967), https://dl.acm.org/doi/book/10.5555/1095587 44. 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 45. 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 46. Otoni, R., Feder, S., Kukovec, J., Kupriyanov, A., Moreira, G., Offtermatt, P., Pani, T., Tran, T., Konnov, I.: The TLA+ model checker apalache. In: Darulova, E., Lin, A.W., Rümmer, P. (eds.) Computer Aided Verification - 38th International Conference, CAV 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings, Part I. Lecture Notes in Computer Science, vol. 16682, pp. 151–166. Springer (2026). https://doi.org/10.1007/978-3-032-32519-8_8 47. 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 48. 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 49. Scarpellini, B.: Complexity of subcases of presburger arithmetic. Transactions of the American Mathematical Society 284, 203–218 (1984). https://doi.org/10. 2307/1999283 50. 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. pp. 357–374. Lecture Notes in Computer Science, Springer (2019). https://doi.org/10.1007/978-3-030-17465-1_20

24

P. Eichler, S. Jacobs

51. 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 52. 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 53. 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 54. Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972). https://doi.org/10.1137/0201010 55. 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 2023, 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 56. 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

Modular Parameterized Model Checking

A

25

Conjunctive Guards and Blocking Receives

Our blocking semantics and conjunctive guards are closely related. Specifically, the blocking semantics can be used to simulate the effects of a conjunctive guard: For a concrete action a that is guarded with set of locations L∀ , we can remove all local actions of a from locations that do not appear in the guard L \ L∀ . As a consequence, a can only be enabled iff all processes are in L∀ . If an action appears in combination with different conjunctive guards, we can copy the action with all of its local actions, assign each copy a unique name, and perform the removal for the different set of locations on the copy. Proposition 1. Synchronous actions with partially defined receive actions under the blocking semantics can simulate conjunctive guards. Similarly, conjunctive guards can be used to simulate a blocking semantics by adding guards that ensure all processes are in locations where receives are defined. We instead chose the blocking semantics, as it simplifies the presentation in the paper and the specifications.

B

Appendix: Recovering Decidability

This section provides more details on the details of the bounded model checking procedure presented in Section 5.1. B.1

Complete SMT Encoding

We start by completing the SMT formula ϕacc which ensures that on every synchronous step the conditions three, four, and seven of Section 3.1 are satisfied. The formula is again split into three parts. The first part ϕloc , which constrains the acceleration factor choices for outgoing local actions to match the number of processes present in a location l, i.e., it implements the constraint three in Section 3.1: X

ϕloc (c, N !, N ?, l, a) := c.k[l] =

X

nai !! +

(l,ai !!,l′ )∈a.Send

nr

r=(l,a??,l′ )∈a.Recv

ϕsuc then constrains the successor configuration c′ , determining how many processes are in location l after a is executed, encoding constraint four of the semantics of synchronous actions: ϕsuc (c′ , N !, N ?, l, a) := c′ .k[l] =

X

nai !! +

(l′ ,ai !!,l)∈a.Send

X

nr

r=(l′ ,a??,l)∈a.Recv

ϕacc then requires that ϕloc and ϕacc hold for all locations and also ensures that the upper and lower bounds on the number of senders associated with action a are satisfied (i.e., constraint 4 in Section 3.1):

26

P. Eichler, S. Jacobs

ϕacc (c, c′ , N !, N ?, a) :=

X

X N ! ≥ a.low ∧ N ! ≤ a.high ^
∧ ϕloc (c, N !, N ?, l, a) ∧ ϕsuc (c′ , N !, N ?, l, a) l∈L

B.2

Context Switches in TAS

Before providing a proof of the correctness of the constructed formula, we first examine effect of synchronous actions on the number of context switches on local rules. As mentioned in Section 5.1, for threshold automata, the encoding described in [3] relies on the fact that a threshold automaton with k distinct guards can have at most k + 1 different contexts. Here, a context refers to a set of guards being enabled or disabled along the execution. As the guards are monotonic, as explained in Section 5.1, for every guard this can only happen once during any run. Since synchronous steps preserve the monotonicity property of the shared variable guards and [3, Proposition 1], there can again be only k context switches: Proposition 2. Every path of a threshold automaton with synchronous steps with k guards can have at most kA = k + 1 context switches. The design of ϕreach then allows up to kA context switches between every synchronous step. This is because, in general, with only a bound on the number of synchronous steps, one cannot deduce constraints on the interleaving of synchronous steps and context switches. Example 5 demonstrates this. In the future, we plan to investigate structural conditions to improve the size of the encoding.

x++ l0

x++ a!!; a??

l1

x > 42

l2

l0

a!!; a??

l1

x > 42

l2

(a) TAS where context switch needs to oc- (b) TAS where context switch needs to occur before synchronous step cur after synchronous step

Fig. 5: TAS with ks = 1 and kA = 2 but in Fig. 5a and Fig. 5b the context switches happen at different points of an execution reaching l2 .

Example 5. Consider the TAS depicted in Fig. 5. For both TAs we can see that ks = 1 (since there is only one synchronous transition and the transition is not part of a loop) and kA = 2. In the first TAS, on a run covering l2 , first the variable x must be increased using the self-loop on l0 (which is an asynchronous transition) to enable the

Modular Parameterized Model Checking

27

guard from l1 to l2 . Only afterwards the synchronous transition from l0 to l1 should be taken, as incrementing x is not possible in l1 . In this case the context switch must occur before executing a synchronous step. Conversely, for the TA depicted in Fig. 5b, the context switch can only appear after the synchronous step has been executed, as x can now only be increased in l1 . B.3

Correctness of the SMT Encoding

We can now state the full correctness proof for ϕreach presented in Section 5.1. We split the proof in three lemmas, the first two for the correctness of ϕeach and ϕmax , the third one for formula ϕsync combining the two. We then present the main correctness theorem for ϕreach . Lemma 3. Let A be a TA with synchronous actions, E its associated environment, CS(E, A) its counter system, a ∈ Σ an each action and let c, c′ be two a configurations of CS(E, A) with c.g = c′ .g and c.p = c′ .p. Then c − → c′ if and ′ only if ϕeach (c, c , a) evaluates to true. a

Proof. ⇒: Let c − → c′ be a valid synchronous step. Let N !, N ? be the acceleration factors chosen for this transition. We V show that ϕeach is true because N !, N ? is a satisfying assignment for ϕeach . n ≥ 1 must be satisfied because, by definition, at least one sender is n∈N !

required to execute every action. Left to show is that ϕacc is satisfied: The first two conjuncts must be satisfied because the upper and lower guards of the action must be satisfied. The conditions ϕloc and ϕsuc must be satisfied by definition of the semantics Section 3.1 . ⇐: Let N !, N ? be a valid assignment of ϕeach (c, c′ , a). We show that N !, N ? is a valid set of acceleration factors by Section 3.1. The first conjunction of ϕeach ensures that there is at least one sender per sending action. Then the other conditions of Section 3.1are ensured by ϕacc : By definition, ϕsuc ensures the conditions on the successor configuration, ϕloc on the other hand ensures that the acceleration factors match the constraints of c. The remaining conjuncts ensure that the send acceleration factors N ! fulfill the upper and lower guards of the action. ⊔ ⊓ Lemma 4. Let A be a threshold automaton with synchronous actions, E its associated environment, and let CS(E, A) denote its counter system. Let c, c′ be a two configurations of CS(E, A) with c.g = c′ .g and c.p = c′ .p. Then c − → c′ with a a max action if and only if there exists a valuation for which ϕmax (c, c′ , a) evaluates to true. Proof (Sketch). Analogously to Lemma P 3 except that the second conjunct ensures the condition min(a.high, c.k[l]): When the minimum is equal (l,ai !!,l′ )∈a.Send

to a.high the first condition of the inner disjunction holds, if the minimum is

28

P. Eichler, S. Jacobs

determined by the number of available senders, only the second condition of the disjunction can become true, and it evaluates to true if and only if all available senders are used. ⊓ ⊔ Lemma 5. Let A be a TA with synchronous actions, E its associated environment, and c, c′ be two configurations of CS(E, A) with c.p = c′ .p. Then a ϕsync (c, c′ ) evaluates to true if and only if c = c′ or c − → c′ for some a ∈ Σ of A. Proof (Sketch). Since synchronous actions cannot update shared variables, the conjunct c.g = c′ .g ensures that the of c and c′ are equal. P variable valuations ′ Then ϕsyncPevaluates to true with S = 0 iff c = c . Otherwise, ϕsync evaluates to true if S = 1 and therefore exactly one sa = 1. As ϕeach and respectively ϕmax by Lemma 3 (Lemma 4) only evaluate to true if a valid synchronous step a between c and c′ exists ϕsync holds iff c − → c′ . ⊔ ⊓ Theorem 4. Let A be a threshold automaton with synchronous actions and ks ∈ N. Then a configuration c′ of A is reachable from configuration c with at most ks synchronous steps, if and only if ϕreach (ks , c, c′ ) is satisfiable. Proof (Sketch). Let A be a threshold automaton with synchronous action and ks ∈ N. Let kA = k + 1 where k denotes the number of distinct guards of local rules, see Appendix B.2. Every run from c to c′ with j ≤ ks synchronous steps can be divided along its synchronous steps: ∗

a

∗

aj−1

∗

0 c = c0 − → c0kA −→ c1 − → . . . −−−→ cj − → ckj A = c′ ,

∗

where every ci − → cki A is a (possibly empty) path only executing local rules. By correctness of ϕasyn [3], ϕasyn (ci , cki A ) holds iff such a path exists. Lemma 5 ai and Proposition 2 implies that ϕsync (cki A , ci+1 ) holds iff cki A −→ ci+1 or cki A = ci+1 . Since all paths can be divided into a form as stated above, it follows that ϕreach holds if and only if a path from c to c′ with at most ks steps exists. ⊔ ⊓ B.4

Layering Algorithm

After having established the correctness of our bounded model checking procedure, this section introduces a practical algorithm to compute layers in a TAS. The algorithm in pseudo code is presented in Algorithm 3. It works by first computing the strongly connected components (SCCs) of the underlying graph of the automaton and sorting them in topological ordering. This can be achieved by utilizing Tarjan’s algorithm [54] and reversing the order of SCCs computed. In a layered TAS, all locations of an SCC must be in the same layer, because every location l of an SCC is reachable from every other location l′ of an SCC and vice versa. Therefore, if one were to assign l and l′ to two different layers and assign an order between those layers, there would be some path from a higher layer to a lower layer, which directly violates the layeredness assumption.

Modular Parameterized Model Checking

Algorithm 3: Compute layer partition of A = ⟨L, LI , Γ, R, G⟩ {S0 , . . . , Sm } ← tarjanSCC(A); L⊘ = ∅; // Check A is layered and determine the sink layer 2 for S ∈ S0 , . . . , Sm do // sync. transition between distinct locations of one SCC: cannot be layered α 3 if ∃l, l′ ∈ S. l − → l′ then // Only receive self-loops are allowed 4 if l = l′ ∧ isSink(l) then // Move to sink layer 5 L⊘ ← L⊘ ∪ {l}; 6 S ← S \ {l}; 7 else 8 return ERROR; // A is not layered // Process SCCs in topological order and assign them to layer 9 for S ∈ S0 , . . . , Sm do 10 if S has no incoming transition then 11 ℓ(S) ← 1; // add to layer 1 12 else // take max over index of incoming α 13 ℓ(S) ← max({ℓ(S ′ ) + weight(a) | S ′ ̸= S s.t. ∃l ∈ S ′ , l′ ∈ S. l − → l′ }); // Return layers as partition 14 P ← []; 15 for i ∈ 1, . . . , max({ℓ(S) | S ∈ S0 , . . . , Sm ∧ S ̸= ∅}) + 1 do S 16 Li ← S; 1

S∈S0 ,...,Sm ∧ℓ(S)=i

P ← P :: [Li ]; 18 if L⊘ ̸= ∅ then 19 P ← P :: [L⊘ ]; 20 return P; 17

// Weight of a rule: 0 if asynchronous, 1 if synchronous Function weight(a ∈ Σ ∪ {ϵ}) 22 if a = ϵ then 23 return 0 24 else 25 return 1

21

// Compute SCCs of A using Tarjan’s algorithm and return SCCs in topological order 26 Function tarjanSCC(A) 27 ... // Check that l is a sink location with only receive self-loops 28 Function isSink(l) 29 ...

29

30

P. Eichler, S. Jacobs

Note that since all locations inside an SCC are always part of the same layer, by Definition 7, within one SCC no synchronous transitions are allowed. After explaining the intuition behind the correctness of Algorithm 3, we can formally state the correctness argument in detail: Lemma 1. A TAS A is layered iff there does not exist a synchronous transition within any SCC of the underlying graph, except for the synchronous receive selfloops in sink locations. Proof (Sketch). ⇒: Proof by contradiction. Let A be threshold automaton with synchronous steps A, and P be a valid partitioning of A according to Definition 7. a Suppose there exists an SCC S with a synchronous transition l − → l′ with l, l′ ∈ S, a ∈ Σ which is not a receive self-loop on a sink location. By definition of a layered automaton (Definition 7), l must be in a lower layer than l′ (as synchronous transition can only transition to a higher layer). However, since l and l′ are part of the same SCC there must also exist a path from l′ to l. On this path, there must consequently exist a transition (asynchronous or synchronous) that transitions to a lower layer. Such a transition is not allowed within a valid partition by Definition 7, which contradicts our assumption. ⇐: Let A threshold automaton for which the underlying graph SCC contains no synchronous transition within an SCC (except for receive self-loops in sink locations). We prove that the automaton is layered by constructing a valid partition using Algorithm 3. Note that all locations, which only have receive self-loops and are sink locations, are moved to L⊘ by the instructions in lines 4 to 6. Therefore, next we have to consider the computation of the other layers. Let S0 , . . . , Sm be the SCCs in topological order (which is ensured by Tarjan’s algorithm [54]) of the graph of the automaton. Algorithm 3 assigns each SCC S to the layer index as one for all source layers and a ℓ(S) = max({ ℓ(S ′ ) + weight(a) | ∃l ∈ S ′ , l′ ∈ S. l − → l′ }), where weight(ϵ) = 0 and weight(a) = 1 for a ∈ Σ, otherwise. Since the algorithm starts with the source SCCs as the SCCs are processed in topological order, i.e., any predecessor of an SCC must have been already processed before the SCC, as otherwise the SCCs would not be topologically ordered. Note that in particular in a topological ordering of SCCs, there are no edges to a previous SCC. Therefore, this processing order also ensures that the two conditions of Definition 7 are upheld: ϵ

– Asynchronous rule. For l → − l′ with l ∈ S, l′ ∈ S ′ : ℓ(S ′ ) ≥ ℓ(S) + 0, so l′ is in the same or a higher layer. If this was not the case, there would exist an edge into a previous SCC and therefore topological ordering would be violated.

Modular Parameterized Model Checking

31

a

– Synchronous rule. For l − → l′ with a ∈ Σ: by assumption l and l′ lie in distinct ′ SCCs, so ℓ(S ) ≥ ℓ(S) + 1 > ℓ(S), meaning l′ is in a strictly higher layer. If this was not the case, there would exist either an edge into a previous SCC and therefore topological ordering would again be violated or there would be a synchronous transition within one SCC violating our assumption. Hence A is layered.

C

Appendix: Modular Models & Replacement

C.1

SMT Encoding Reachability-Preserving Replacements

This section provides the SMT encodings omitted in Section 6. We start with the definition of ϕI (c) which is true if and only if a configuration c is an initial configuration: ^ X ^ c.k[l] = 0 ∧ c.g[x] = 0 ϕI (c) := c.k[l] = N (c.p) ∧ l∈LI

l∈L\LI

x∈Γ

Next, the following theorem provides the encoding for checking whether a replacement is strongly reachability-preserving: Theorem 5. Let A and A
R be layered TAS with ks = |PA |−1 and ks′ = |PA
R |−1. Then R is strongly reachability-preserving iff the following formula holds: ϕsrp (A, R) := ϕrp (A, R) ∧ ∀cI , c ∈ CA
R . ϕI (cI ) ∧ ϕreach (ks′ , cI , c) ∧

l ^

c.k[l] = 0 =⇒ ∃c′I , c′ ∈ CA . ϕI (c′I ) ∧ ϕreach (ks′ , c′I , c′ )

Ladd

∧

l ^

c.k[l] = c′ .k[l] ∧

l ^ Lrm

L\Lrm ′

∧ c.p = c .p

c′ .k[l] = 0 ∧

x ^

c.g[x] = c′ .g[x]

Γ \Γrm

We can now also describe more precisely which properties transfer after a reachability-preserving replacement: Lemma 6. Let A be a threshold automaton with synchronous actions and R a reachability-preserving replacement, E the environment, and let φ be a cardinality constraint, V which only references locations in LA \ Lrm . If a configuration satisfying φ ∧ l∈Lrm #l = 0 is reachable in A, then a configuration satisfying V φ∧ l∈Ladd #l = 0 is reachable in A
R. If R is strongly reachability preserving, the converse direction holds as well. V Proof (Sketch). Let c be a reachable configuration of A with c |= φ∧ l∈Lrm #l = 0. By Definition 9, there is a reachable configuration c′ of A
R with c′ .k[l] = 0 for all l ∈ Ladd and c′ .k[l] = c.k[l] for all l ∈ L \ Lrm . As φ only constrains locations in L \ Lrm , also c′ |= φ. For strong reachability-preserving replacements, the other direction follows analogously. ⊓ ⊔

32

P. Eichler, S. Jacobs

C.2

Local Replacement Condition

We have seen, that the SMT formulas for checking whether a replacement is (strong) reachability preserving essentially encode the whole reachability relation of both automata. This is necessary because the replacement definition is very general, in practice replacements only concern a limited set of the locations of an automaton. To obtain a more local property, we examine the benchmarks and make the following observations: – Modules are typically replaced at the beginning of an automaton. In our examples, the algorithms are usually built upon the results of the execution of a previous module. Consequently, the replacement usually starts at the initial states, i.e., LI = Lent . – Processes pass through the module at most once. Most algorithms do not need to execute a module multiple times, after the processes leave the state space of the module they cannot return. We first define Achng (A, R) which is exactly the (sub-) automaton which gets replaced by a replacement R. Definition 10. For a TAS A = ⟨L, LI , Γ, R, G⟩ and a replacement R = ⟨Lrm , Ladd , Radd , Gadd , Γrm ⟩. Let RR = {r ∈ R | r.from ∈ Lrm ∨ r.to ∈ Lrm }, GR = {(a, , , , , ) ∈ G | ∃(l, , l′ ) ∈ a.Send ∪ a.Recv. l ∈ Lrm ∨ l′ ∈ Lrm } and LR = Lrm ∪ Lent ∪ Lext . We denote by Achng (A, R) = ⟨LR , LI , Γ, RR , GR ⟩ the replacement automaton. We also define – Rpost = R ∩ R′ , where R′ denotes the rules of A
R, i.e., the rules which are not updated by the replacement, and – Gpost = G ∩ G ′ , where G ′ denotes the rules of A
R, i.e., the rules which are not updated by the replacement. Also, let vars(R) denote the shared variables appearing on R, acts(G) the set of global actions appearing on G, and, for a set T of rules and global rules, let src(T ) and tgt(T ) denote the sets of all source and target locations of the rules and local transitions in T . Definition 11. Let A be an automaton, R a replacement, we call R local reachability-preserving if it satisfies (R1)-(R4) below and R is reachability-preserving on Achng (A, R). If R satisfies R1-R4 below and is strongly reachability-preserving on Achng (A, R), we call it strongly local reachability-preserving. – (R1) LI = Lent , i.e., the replaced part is the beginning of the automaton. – (R2) tgt(Rpost ∪ Gpost ) ∩ Lent = ∅, src(RR ∪ Radd ∪ GR ∪ Gadd ) ⊆ Lent ∪ Lrm ∪ Ladd , and tgt(RR ∪ Radd ∪ GR ∪ Gadd ) ⊆ LR ∪ Ladd , i.e., the replaced part only acts inside the module, and once a process has left Lent ∪ Lrm ∪ Ladd , it never returns.

Modular Parameterized Model Checking

33

– (R3) vars(RR ∪ Radd ) ∩ vars(Rpost ) = ∅, i.e., the replaced part does not share variables with the rest of the automaton. – (R4) acts(GR ∪ Gadd ) ∩ acts(Gpost ) = ∅, i.e., the replaced part does not share synchronous actions with the rest of the automaton. R1 - R4 are simple syntactic checks on the automaton, and the reachabilitypreserving conditions now only have to be checked on the parts of the automaton that are replaced. Depending on the size of the replacement compared to the original automaton, this can drastically reduce the size of the encoding. Next we show that checking local reachability preserving is enough: Lemma 7. Let E be an environment, A be an automaton and R a replacement in A. If R is (strong) local reachability-preserving then R is also (strong) reachability preserving. Proof. Proof by contradiction, i.e., assume there exists a reachable configuration c (with Lrm empty) in A such that no matching configuration is reachable in A
R. Let ρ = c0 → − ... → − c denote the computation reaching c. We show that it is possible to find a run ρ′ in A
R reaching a configuration equivalent to c, contradicting the assumption: We first show that we can reorder and split the run ρ into two parts ρ1 , ρ2 where ρ1 only executes rules that are replaced by R and the second half ρ2 , only executes rules that are not replaced. Reordering the run. By R2 and the definition of Rpost and Gpost , rules that are not replaced never move a process into Lent ∪ Lrm , and all replaced rules start in Lent ∪ Lrm . Note that as soon as a process moves out of Lent ∪ Lrm it disables all actions of GR for the rest of the run. Assume the run ρ is not yet in the shape ρ = ρ1 ρ2 , i.e., there must exist a step which executes a rule in Rpost or Gpost , which is followed by a step of a rule or action removed by the replacement. The step using a replaced rule cannot be synchronous, since for the previous step to have been enabled, there must have been some process in L \ Lrm , which stays outside the module by R2. By R3 it follows that every synchronous action must be disabled, by the process, since the process has no corresponding receive action. Similarly, the first step executing a rule from Rpost and Gpost cannot be synchronous either, since it would require all processes to be in L \ Lrm (or there would again be some blocking process), disabling any step using a replaced rule. Hence, both steps are asynchronous. The source of the second step lies in Lent ∪ Lrm and is therefore not the target of the first step, and by R4 neither step can update a variable of the other’s guard, so we can swap the execution of the rules. Let cmid be the configuration between ρ1 and ρ2 . As ρ2 does not move processes into or out of Lrm , also cmid .k[l] = 0 for all l ∈ Lrm . Simulating ρ1 . By R1 c0 is an initial configuration of Achng (A, R) and A
R, and by R2 ρ1 is a run of Achng (A, R). Since the replacement is local reachability preserving, we therefore know that there must exist a run reaching a configuration equivalent to cmid in Achng (A, R)
R and since by R2 all processes remain

34

P. Eichler, S. Jacobs

in the locations of Achng (A, R)
R, the run consequently also has to exist in A
R. We refer to this run as ρ′1 . Simulating ρ2 . Since ρ′1 ends in a configuration equivalent to cmid , we can replay ρ2 step by step. By definition, rules in Rpost and Gpost do not interfere with Lrm ∪ Ladd . Therefore, they remain in A
R and only refer to locations and variables on which both agree. By R4, both automata have the same rules for every action of Gpost , so synchronous steps remain enabled as well. Hence, the resulting run reaches a configuration equivalent to c, contradicting our assumption. The strong direction follows analogously. ⊔ ⊓

D

Appendix: Evaluation & Case Study

D.1

TA Models & Synchronous Abstractions

This section will provide more detail on the king consensus and king consensus algorithms, and it will introduce the remaining threshold automata and synchronous models, and the properties that have been checked for each. Again the algorithm representations and correctness properties are taken from [23]. Weak Consensus. The weak consensus TA has been discussed in Example 1 and its synchronous abstraction in Example 3. The correctness properties of weak consensus are – Weak Consistency: If the output yi ∈ {0, 1} for some honest player Pi , then yj ∈ {⊥, yi } for all other honest players Pj . We translate this to □(y0 > 0 ⇒ y1 = 0) and □(y1 > 0 ⇒ y0 = 0). – Weak Persistency: If all honest players have the same input value x, then all honest players output yi = x. We translate this to x1 = 0 ⇒ □(y1 = 0 ∧ y⊥ = 0) and x0 = 0 ⇒ □(y0 = 0 ∧ y⊥ = 0).

z!!, mz!!, z??

x0

mz!!, b!! mo??, b!! o?? , mo ?? ? mz?

x1

, z?? b?? mz??, b? mo!!, ?

l0,1 l0,0 l1,0 l1,1

o!!, mo!!, o??

Fig. 6: Synchronous overapproximation of graded consensus with z, o each actions with lower bound n−t−f and mz, mo max actions with lower bounds n−t−f , upper bound n−t−1 and b also a max action with lower bound t−f +1 and upper bound n−t−1.

Graded Consensus. We start with the synchronous overapproximation of the graded consensus algorithm presented in Fig. 6. Similar to the weak consensus

Modular Parameterized Model Checking

35

algorithm introduced in Example 3, the actions z and o represent the acceptance of value zero or one, and mz, mo the case where one value might be accepted by some processes using the votes of Byzantine processes. Again, the action b can fire when no value can be accepted with grade one. In this case, b moves processes directly to l0,0 or l1,0 , so processes can reach l1,0 even if f = 0. z!!, mz!!, z??

mz!!

x0

l0,1 b!!

mo??

o?? , mo ??

k!!,

, k??

? fl?

l0,0

l⊥ ??

, mz

z?? b??

x1

mz??

fl!!

, fl

??

l1,0

l1,1

mo!! o!!, mo!!, o??

Fig. 7: Exact synchronous model of graded consensus with z, o, mz, mo as in Fig. 6, b a max action with b.low = t−f +1 and b.high = n−t−1, and k, fl each actions with k.low = fl.low = 1 and fl.high = f .

Fig. 7 shows an exact synchronous model, which coincides with the overapproximation except for the action b. In this case, b moves all processes to the intermediate location l⊥ . From there, either the action k moves all processes to l0,0 , or the action fl moves all its senders to l1,0 and all other processes to l0,0 or l1,0 . However, since action fl has upper bound f , it can only be enabled if f ≥ 1 and therefore the model is exact. The graded consensus guarantees the following properties: – Graded Consistency: If an honest player Pi outputs (yi , 1), then yj = yi for all other honest players Pj . We translate this to □(l0,1 > 0 ⇒ l1,0 = 0 ∧ l1,1 = 0) and □(l1,1 > 0 ⇒ l0,0 = 0 ∧ l0,1 = 0). – Graded Persistency: If all honest players have the same input value x, then all honest players output (yi , gi ) = (x, 1). We translate this to x1 = 0 ⇒ □(l0,0 = 0 ∧ l1,0 = 0 ∧ l1,1 = 0) and x0 = 0 ⇒ □(l0,0 = 0 ∧ l0,1 = 0 ∧ l1,0 = 0).

36

P. Eichler, S. Jacobs l0,1

Algorithm 4: King ConsensusPk (x1 , . . . , xn ) → (y1 , . . . , yn ) ((z1 , g1 ), . . . , (zn , gn )) = GradedConsensus(x1 , . . . , xn ) 2 Pk : send zk to every Pj 3 ∀Pi : ( zi if gi = 1 yi = zk else 4 ∀Pi : return yi

1

c=0

∧ fk

⊤ = 0; v0 ++, c++

v0 ≥ 1 ∨ f k ≥ 1 c = 0 ∧ f k = 0; v0 ++, c++

l0,0

l1,0

l1,1

v1 ≥ 1

v0 ≥ 1

k0 ∨ fk

≥1

∨ fk

≥1

k1

c = 0 ∧ f k = 0; v1 ++, c++ v1 ≥ 1 ∨ f k ≥ 1 c++ v1++, = 0; ∧ fk c=0 ⊤

Fig. 8: King consensus threshold automaton AK , where Π = {n, t, f, pk} and RC = n > 3t ∧ t ≥ f ∧ pk ≤ 1 and initial condition pk = vk.

King Consensus. z!!, b!!, z??, b?? Fig. 8 depicts the additional locations x0 k0 o?? , b? that a threshold automaton adds on top of ? the graded consensus automaton. Note that ? , b? the model uses an additional parameter pk, z?? x1 k1 with an additional initial condition pk = vk. o!!, b!!, o??, b?? The parameter is used to model whether the algorithm assumes an honest king (if pk = 0 Fig. 9: King consensus and therefore vk = 0) or whether the round synchronous module with z, o assumes a faulty king (pk = vk = 1), which each actions with lower bound 1 can send different king votes to every pro- and b also an each action with cess. lower bound 2 and upper bound The synchronous abstraction of a king 2 ∗ pk consensus algorithm is depicted in Fig. 9 and only has three actions, o and z which correspond to reaching consensus on value one or value zero and action b. The action b requires at least one process starting in location x0 and one in x1 , and pk = 1, i.e., an honest king round. If b is fired, processes can transition to an arbitrary output location. The correctness properties of king consensus are – King Persistency: If all honest players have the same input value x, then all honest players output yi = x, even if the king is faulty. We translate this to x1 = 0 ⇒ □(k1 = 0) and x0 = 0 ⇒ □(k0 = 0). – King Consistency: If the king Pk is honest, then all honest players output the same value y ∈ {0, 1}. We translate this to pk = 0 ⇒ □(k0 = 0 ∨ k1 = 0). D.2

Benchmark Setup

All experiments have been conducted on a machine with two AMD EPYC 7773x processors, with 64 cores each and 2TB RAM, running Ubuntu 24.04.5 as host OS with kernel version 5.15.0. As SMT solver Z3 [45] v.4.16.0 has been used. The reported execution time is the measured wall clock time rounded to two decimal places. To measure the memory consumption, our benchmarking

Modular Parameterized Model Checking

37

script samples the sum of VmRSS, i.e., the reported resident set size, of all child processes every 1ms, and takes the maximum with the reported VmHWM, i.e., the reported peak resident set size.

Related documents

• Model Checking of Distributed Algorithm Implementations#1361784
• CUA-Recovery: Benchmarking Error Recovery in Long-Horizon Computer-Use Agents#1403441
• Modelstamp: Pre-Deserialization Verification of Machine-Learning Artifacts and Runtime Environment State#822208
• Distributed Algorithms#3468
• dSTAR: Straggler Tolerant and Byzantine Resilient Distributed SGD#1035272