Jure Kukovec
email: jkukovec@forsyte.at

Thanh-Hai Tran
email: tran@forsyte.at

Igor Konnov
email: konnov@forsyte.at

Extracting Symbolic Transitions from TLA + Specifications

In TLA + , a system specification is written as a logical formula that restricts the system behavior. As a logic, TLA + does not have assignments and other imperative statements that are used by model checkers to compute the successor states of a system state. Model checkers compute successors either explicitly -by evaluating program statementsor symbolically -by translating program statements to an SMT formula and checking its satisfiability. To efficiently enumerate the successors, TLA's model checker TLC introduces side effects. For instance, an equality x = e is interpreted as an assignment of e to the yet unbound variable x . Inspired by TLC, we introduce an automatic technique for discovering expressions in TLA + formulas such as x = e and x ∈ {e1, . . . , e k } that can be provably used as assignments. In contrast to TLC, our technique does not explicitly evaluate expressions, but it reduces the problem of finding assignments to the satisfiability of an SMT formula. Hence, we give a way to slice a TLA + formula in symbolic transitions, which can be used as an input to a symbolic model checker. Our prototype implementation successfully extracts symbolic transitions from a few TLA + benchmarks.

Introduction

TLA is a general language introduced by Leslie Lamport for specifying temporal behavior of computer systems. It was later extended to TLA + [START_REF] Lamport | Specifying systems: the TLA + language and tools for hardware and software engineers[END_REF], which provides the user with a concrete syntax for writing expressions over sets, functions, integers, sequences, etc. TLA + does not fix a model of computation, and thus it found applications in the design of concurrent and distributed systems, e.g., see [START_REF] Gafni | Disk paxos[END_REF][START_REF] Newcombe | How Amazon web services uses formal methods[END_REF][START_REF] Ongaro | Consensus: Bridging theory and practice[END_REF][START_REF] Moraru | There is more consensus in egalitarian parliaments[END_REF][START_REF] Azmy | A rigorous correctness proof for pastry[END_REF].

A specification alone brings almost no guarantees of system correctness. As it is an untyped language, TLA + allows for expressions such as 1 ∪ {2}, which are considered ill-typed in statically-typed programming languages. To formally prove specification properties such as safety and liveness, one can use TLAPS -a proof Fig. 1: A simple producer-consumer system for TLA + [START_REF] Chaudhuri | The TLA + proof system: Building a heterogeneous verification platform[END_REF]. Although progress towards proof automation was made in the last years [START_REF] Merz | Automatic verification of TLA + proof obligations with SMT solvers[END_REF], writing formal proofs is still a challenging task [START_REF] Newcombe | How Amazon web services uses formal methods[END_REF][START_REF] Ongaro | Consensus: Bridging theory and practice[END_REF].

On the other side of the spectrum are model checkers that require little user effort to run. Indeed, TLA + users debug their specifications with TLC [START_REF] Yu | Model checking TLA + specifications[END_REF]. Beyond simple debugging, TLC found serious bugs in specifications of distributed algorithms [START_REF] Newcombe | How Amazon web services uses formal methods[END_REF]. Although TLC contains remarkable engineering solutions, its core techniques enumerate reachable states and inevitably suffer from state explosion.

Instead of enumerating states, software model checkers run SAT and SMT solvers in the background to reason about computations symbolically. To name a few, CBMC [START_REF] Kroening | CBMC -C bounded model checker -(competition contribution)[END_REF] and CPAChecker [START_REF] Beyer | CPAchecker: A tool for configurable software verification[END_REF] implement bounded model checking [START_REF] Biere | Symbolic model checking without BDDs[END_REF] and CEGAR [START_REF] Clarke | Counterexample-guided abstraction refinement for symbolic model checking[END_REF]. Domain-specific tools ByMC and Cubicle prove properties of parameterized distributed algorithms with SMT [START_REF] Conchon | Cubicle: A parallel smt-based model checker for parameterized systems -tool paper[END_REF][START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF].

A simple example in Figure 1 illustrates the problems that one faces when developing a symbolic model checker for TLA + . In this example, we model two processes: Producer that inserts a subset of {"A", "B ", "Z ", "1", "8"} into the set S , and Consumer that removes from S its arbitrary subset. The system is initialized with the operator Init. A system transition is specified with the operator Next that is defined via a disjunction of operators Produce and Consume. Both Producer and Consumer maintain the state invariant empty ⇔ (S = ∅). We notice the following challenges for a symbolic approach:

1. The specification does not have types. This is not a problem for TLC, since it constructs states on the fly and hence dynamically computes types. In the symbolic case, one can use type synthesis [START_REF] Merz | Automatic verification of TLA + proof obligations with SMT solvers[END_REF] or the untyped SMT encoding [START_REF] Merz | Harnessing SMT solvers for TLA+ proofs[END_REF]. 2. Direct translation of Next to SMT would produce a monolithic formula, e.g., it would not analyze Produce and Consume as independent actions. This is in sharp contrast to translation of imperative programs, in which variable assignments allow a model checker to focus only on the local state changes.

In this paper, we focus on the second problem. Our motivation comes from the observation on how TLC computes the successors of a given state [START_REF] Lamport | Specifying systems: the TLA + language and tools for hardware and software engineers[END_REF]Ch. 14]. Instead of precomputing all potential successors -which would be anyway impossible without types -and evaluating Next on them, TLC explores subformulas of Next. The essential exploration rules are: (1) Disjunctions and conjunctions are evaluated from left to right, (2) an equality x = e assigns the value of e to x if

x is yet unbound, (3) if an unbound variable appears on the right-hand side of an assignment or in a non-assignment expression, TLC terminates with an error, and (4) operands of a disjunction assign values to the variables independently. In more detail, rule (4) means that whenever a disjunction A ∨ B is evaluated and x is assigned a value in A, this value does not propagate to B ; moreover, x must be assigned a value in B .

In our example, TLC evaluates the actions Produce and Consume independently and assigns variables as prescribed by these formulas. As TLC is explicit, for each state, it produces at most 2 2 5 successors in Produce as well as in Consume.

We introduce a technique to statically label expressions in a TLA + formula φ as assignments to the variables from a set V , while fulfilling the following:

1. For purely Boolean formulas, if one transforms φ into an equivalent formula 1≤i≤k D i in disjunctive normal form (DNF), then every disjunct D i has exactly one assignment per variable from V . 2. The assignments adhere the following partial order: if x ∈ V is assigned a value in expression e, that uses a variable y ∈ V , then the assignment to y precedes the assignment to x . 3. In general, we formalize the above idea with the notion of a branch.

As expected, the following sequence of expressions is given as assignments in our example: (1) empty = true, (2) S = S ∪ {X }, (3) S ∈ subset S , and (4) empty = (S = ∅). Using this sequence, our technique constructs two symbolic transitions that are equivalent to the actions Produce and Consume.

In general, finding assignments and slicing a formula into symbolic transitions is not as easy as in our example, because of quantifiers and if-then-else complicating matters. In this paper, we present our solution, demonstrate its soundness and report on preliminary experiments.

2 Abstract Syntax α-TLA + TLA + has rich syntax [START_REF] Lamport | Specifying systems: the TLA + language and tools for hardware and software engineers[END_REF], which cannot be defined in this paper. To focus only on the expressions that are essential for finding assignments in a formula, we define abstract syntax for TLA + formulas below. In our syntax, the essential operators such as conjunctions and disjunctions are included explicitly, while the other nonessential operators are hidden under the star expression .

We assume predefined three infinite sets:

-A set L of labels. We use notation i to refer to its elements, for i ∈ N.

-A set Vars of primed variables that are decorated with prime, e.g., x and a .

-A set Bound of bound variables, which are used by quantifiers. x ::= a variable name from the set Bound A few comments on the syntax and its relation to TLA + expressions are in order. We require every expression to carry a unique label i ∈ L. Although this is not a requirement in TLA + , it is easy to decorate every expression with a unique label. The expressions of the form :: v ∈ expr are of ultimate interest to us, as they are treated as assignment candidates. Under certain conditions, they can be used to assign to v a value from the set represented by the expression expr . Perhaps somewhat unexpectedly, expressions such as v = e and unchanged v 1 , . . . , v k are not included in our syntax. To keep the syntax minimal, we represent them with :: v ∈ expr . Indeed, these expressions can be rewritten in an equivalent form: v = e as v ∈ {e}, and unchanged v 1 , . . . , v k as v 1 ∈ {v 1 }∧• • •∧v k ∈ {v k }. Every non-essential TLA + expression e is presented in the abstract form :: (v 1 , . . . , v k ), where v 1 , . . . , v k are the names of the primed variables that appear in e. When no primed variable appears in an expression, we omit parenthesis and write :: . TLA + expressions often refer to user-defined operators, which are not present in our abstract syntax. We simply assume that all non-recursive user-defined operators have been expanded, that is, recursively replaced with their bodies. All uses of recursive operators are hidden under ; hence, recursive operator definitions are ignored when searching for assignment candidates.

It should be now straightforward to see how one could translate a TLA + expression to our abstract syntax. We write α(e) to denote the expression in α-TLA + , that represents an expression e in the complete TLA + syntax. With γ we denote the reverse translation from α-TLA + to TLA + that has the property that γ(α(e)) = e. Figure 2 shows the abstract expression α(Next) of the operator Next defined in Figure 1.

Discussions. Notice that α-TLA + is missing several fundamental constructs permitted in TLA + , such as case expressions, universal quantifiers, and negations. They are all abstracted to . The primary purpose of α-TLA + is to allow us to determine whether a given expression containing set inclusion -or equality -can be used as an assignment. If such an expression occurs under a universal quantifier, it is not clear which value should be used for an assignment. Hence, we abstract the expressions under universal quantifiers. For similar reason, we abstract the expressions under negation. The latter is consistent with TLC, which produces an error when given, for example, Next == ¬(x = 1). Finally, we abstract case, due to its semantics, which is defined in terms of the choose operator [START_REF] Lamport | Specifying systems: the TLA + language and tools for hardware and software engineers[END_REF]Ch. 6]. In practice, there are no potential assignments under case in the standard TLA + examples.

Preliminary Definitions

Every TLA + specification declares a certain finite set of variables, which may appear in the formulas contained therein. Let φ be an α-TLA + expression. We assume, for the purposes of our analysis, that φ is associated with some finite set Vars (φ), which is a subset of Vars , containing all of the variables that appear in φ (and possibly additional ones). This is the set of variables declared by the specification in which γ(φ) appears.

Since the labels are unique, we write lab( :: ψ) to refer to the expression label and expr( ) to refer to the expression that is labeled with . We refer to the set of all subexpressions of φ by Sub(φ). See [START_REF] Kukovec | Extracting symbolic transitions from TLA + specifications[END_REF] for a formal definition.

The set Sub(φ) allows us to reason about terms that appear inside an expression φ, at some unknown/irrelevant depth. We will often refer to the set of all labels appearing in φ, that is,

Labs(φ) = {lab(ψ) | ψ ∈ Sub(φ)}.
Of special interest to us are assignment candidates, i.e., expressions of the form :: v ∈ φ 1 . Given a variable v ∈ Vars (φ) and an α-TLA + expression φ, we write cand(v , φ) to mean the set of labels that belong to assignment candidates for v in subexpressions of φ. More formally, cand(v , φ) is { | ( :: v ∈ ψ) ∈ Sub(φ)}. An exhaustive definition is included in [START_REF] Kukovec | Extracting symbolic transitions from TLA + specifications[END_REF]. We use the notation cand(φ) to mean

v ∈ Vars (φ) cand(v , φ).
Finally, we assign to each label in Labs(φ) a set frozen φ ( ) ⊆ Vars (φ). Intuitively, if a variable v is in frozen φ ( ), then no expression of the form ˆ :: v ∈ ψ can be treated as an assignment inside expr( ). Formally, for every ∈ Labs(φ) the set frozen φ ( ) is defined as the minimal set satisfying all the constraints in Table 1.

The sets frozen φ naturally lead to the dependency relations v on Labs(φ), where v ∈ Vars (φ). We will use 1 v 2 to mean that 1 is an assignment candidate for v , which also belongs to the frozen set of 2 . Formally:

1 v 2 ⇐⇒ 1 ∈ cand(v , φ) ∧ v ∈ frozen φ ( 2 )
Intuitively, if 1 v 2 we want to make sure that expr( 1 ) is evaluated before expr( 2 ), if possible.

Example 1. Let us look at the following α-TLA + expression:

1 :: [∃i ∈ [ 2 :: (y )] : 3 :: x ∈ [ 4 :: ]]
:: (v 1 , . . . , v k ) {v 1 , . . . , v k } ⊆ frozen φ ( ) :: v ∈ φ1 frozen φ ( ) = frozen φ (lab(φ1))
:: s i=1 φi or :: s i=1 φi frozen φ ( ) ⊆ frozen φ (lab(φi )) for i ∈ {1, . . . , s}

:: ∃x ∈ φ1 : φ2 frozen φ ( ) ⊆ frozen φ (lab(φ1)) ⊆ frozen φ (lab(φ2)) :: if φ1 then φ2 else φ3 frozen φ ( ) ⊆ frozen φ (lab(φ1)) frozen φ (lab(φ1)) ⊆ frozen φ (lab(φi )) for i = 2, 3
Take the subexpression 3 :: x ∈ [ 4 :: ], which we name ψ . By solving the constraints for frozen ψ ( 3 ) we conclude that frozen ψ ( 3 ) = ∅. However, if we take the additional constraints for frozen φ ( 3 ) into consideration, the empty set no longer satisfies all of them, specifically, it does not satisfy the condition imposed by the existential quantifier in 1 . The additional requirement {y } ⊆ frozen φ ( 3 ) implies that frozen φ ( 3 ) = {y }. This corresponds to the intuition that expressions under a quantifier, like ψ, implicitly depend on the bound variable and the expressions used to define it, which is expr( 2 ) in our example.

Formalizing Symbolic Assignments

As TLC evaluates formulas in a left-to-right order, there is a very clear notion of an assignment; the first occurrence of an expression v ∈ S is interpreted as an assignment to v . In our work, we want to statically find expressions that can safely be used as assignments. If we were only dealing with Boolean formulas, we could transform the original TLA + formula to DNF, s i=1 D i , and treat each D i independently. However, we also need to find assignments, which may be nested under existential quantifiers. To transfer our intuition about DNF to the general case we first introduce a transformation boolForm, that captures the Boolean structure of the formula. Then, we introduce branches and assignment strategies to formalize the notion of assignments in the symbolic case. Then, Branches(φ) is the set of all branches of φ.

Example 2. Let us look the α-TLA + expression φ given by As our goal is to reason about the side-effects of variable assignments, the remainder of this section looks at how we can achieve this with the help of branches.

1 :: [[ 2 :: x ∈ ] ∧ [ 3 :: [[ 4 :: x ∈ ] ∨ [ 5 :: x ∈ ]]]] We know that boolForm(φ) = b 2 ∧ (b 4 ∨ b 5 ). The set S = { 2 , 4 , 5 }
Assignment strategies. We want to statically mark some expressions as assignments, that is, pick a set A ⊆ Labs(φ). Below, we formulate the critical properties we require from such a set, which we will later call an assignment strategy.

Most obviously, we want to consider only assignment candidates:

Definition 1. A set H ⊆ Labs(φ)
is homogeneous if all the labels in H are assignment candidates. Formally, H ⊆ cand(φ).

If we choose an arbitrary homogeneous set H , it might lack assignments on some branches or have multiple assignments to the same variable on others. Formally, we say that H has a covering index d ∈ N 0 if there is a branch Br ∈ Branches(φ) and a variable v ∈ Vars (φ) for which d = |Br ∩ H ∩ cand(v , φ)|. Now we define sets, that cover all branches with assignments: Definition 2. A homogeneous set C is a covering of φ, if it does not have 0 as a covering index. It is a minimal covering of φ, if it only has 1 as a covering index.

Consider the TLA + formula x = y ∧ y = 2x . Its corresponding α-TLA + expression 0 :: ( 1 :: x ∈ 2 :: (y ) ∧ 3 :: y ∈ 4 :: (x )) has a minimal covering { 1 , 3 }. However, there is no way to order the assignments to x and y . To detect such cases, we define acyclic sets: Definition 3. A homogeneous set A is acyclic, if there is a strict total order ≺ A on A, with the following property: For every variable v ∈ V , every branch Br ∈ Branches and every pair of labels i and j in A ∩ Br the relation i v j implies i ≺ A j .

Having defined homogeneous, minimal covering, and acyclic sets, we can formulate the notion of an assignment strategy. Definition 4. Let φ be an α-TLA + expression. A set A ⊆ L is an assignment strategy for φ, if it is an acyclic minimal covering.

Static assignment problem. Given an α-TLA + expression φ, our goal is to find an assignment strategy, or prove that none exists.

Finding Assignment Strategies with SMT

For a given α-TLA + expression φ, we construct an SMT formula θ(φ), that encodes the properties of assignment strategies. Technically, θ(φ) is defined as θ H (φ) ∧ θ C (φ) ∧ θ A (φ), and consists of:

1. A Boolean formula θ H (φ), that encodes homogeneity. 2. A Boolean formula θ C (φ), that encodes the minimal covering property. 3. A formula θ A (φ), that encodes acyclicity. This formula requires the theories of linear integer arithmetic and uninterpreted functions (QF UFLIA).

In the following, Propositions 1, 3, and 4 formally establish the relation between φ and its three SMT counterparts. Together, the propositions allows us to prove the following theorem: Theorem 1. For every α-TLA + formula φ and A ⊆ Labs(φ), it holds that M[A] θ(φ) if and only if A is an assignment strategy for φ.

Homogeneous Sets

We introduce a Boolean formula, whose models are exactly those induced by homogeneous sets. To this end, take the set of labels corresponding to expressions that are not assignment candidates, N (φ), given by N (φ) := Labs(φ) \ cand(φ). Then, we define the following:

θ H (φ) := ∈ N (φ)
¬b Proposition 1. For every α-TLA + expression φ and A ⊆ Labs(φ), it holds that M[A] θ H (φ) if and only if A is homogeneous.

:: if φ1 then φ2 else φ3 δ v (φ2) ∧ δ v (φ3)

Minimal Covering Sets

Next we construct a Boolean formula θ * C (φ), whose models are exactly those induced by covering sets. To this end, we define, for each v ∈ Vars (φ), the transformation δ v as shown in Table 3. Intuitively, δ v (φ) is satisfiable exactly when there is an assignment to v on every branch of φ. We then define

θ * C (φ) := v ∈ Vars (φ) δ v (φ)
Formally, the following proposition holds:

Proposition 2. For every α-TLA + expression φ and A ⊆ Labs(φ), it holds that M[A] θ H (φ) ∧ θ * C (φ) if and only if A is a covering set for φ. It is easy to restrict coverings to the minimal coverings. To do this, we define the set of collocated labels, denoted Colloc(φ), as

Colloc(φ) := {( 1 , 2 ) ∈ L 2 | ∃Br ∈ Branches(φ) . { 1 , 2 } ⊆ Br }
We can use this set to reason about minimal coverings: A minimal covering may contain, per variable, no more than one label from each pair of collocated assignments to that variable. We describe these labels by using the sets Colloc v (φ

) := Colloc(φ) ∩ cand(v , φ) 2 and Colloc Vars (φ) := v ∈ Vars (φ) Colloc v (φ)
Then, the following SMT formula, in addition to θ * C (φ), helps us find minimal covering sets:

θ ∃! (φ) := (i,j ) ∈ Colloc Vars (φ) i<j ¬(b i ∧ b j )
We denote by θ C (φ) the formula θ * C (φ) ∧ θ ∃! (φ). Proposition 3. For every α-TLA + expression φ and A ⊆ Labs(φ), it holds that M[A] θ H (φ) ∧ θ C (φ) if and only if A is a minimal covering set for φ.

Acyclic Assignments

The last step is reasoning about acyclicity. Recall that, for 1 , 2 ∈ L, the relation

1 v 2 holds if and only if 1 ∈ cand(v , φ) ∧ v ∈ frozen φ ( 2 )
. It is prudent to see that v is not, in general, a strict total order (possibly not even irreflexive). However, the acyclicity property states that we can find a strict total order, which agrees with all relations v , on all branches.

Take Colloc (φ) to be the filtering of Colloc(φ) by the relations v , i.e. the set

{(i , j ) ∈ Colloc(φ) ∩ cand(φ) 2 | ∃v ∈ Vars (φ) . i v j }.
The SMT formula describing acyclicity is as follows:

θ * A (φ) := (i,j ) ∈ Colloc (φ) b i ∧ b j ⇒ R(i ) < R(j )
where R is an uninterpreted L → N function, capturing assignment order. In practice, we take L = N. Unlike the previous formulas, θ * A (φ) extends beyond Boolean logic, requiring both linear integer arithmetic and uninterpreted functions. Thus, a model for θ * A (φ) is a pair (M , r ), where M models the Boolean part of the formula, i.e. assigns truth values to each b i , and r : N → N is the interpretation of R.

To simplify the analysis, we force R to be injective, when it is restricted to Labs(φ). Otherwise we could always construct an injective function from R, which respects the required inequalities. The formula we therefore consider is as follows:

θ A (φ) := θ * A (φ) ∧ 1, j ∈ Labs(φ) i < j R( i ) = R( j )
Proposition 4. For every α-TLA + expression φ and A ⊆ Labs(φ), there is a function r : N → N, for which (M[A], r ) θ H (φ) ∧ θ A (φ) if and only if A is acyclic.

Soundness of our Approach

In this section, we show the relation between assignment strategies and the original TLA + formulas. To this end, we introduce the notion of a slice. Together, branches allow us to rewrite a TLA + formula into an equivalent disjunction of slices. In TLA + , there are two kinds of variables: rigid variables that correspond to the variables declared with constant, and flexible variables whose values change during the course of an execution. Primed versions of the variables exist only for flexible variables and are used in transition formulas. Transition formulas in TLA + are first-order terms and formulas with flexible variables (unprimed and primed ones). We give the necessary definitions of TLA + semantics, whereas details can be found in [START_REF] Merz | The specification language TLA +[END_REF]. An interpretation I defines a universe |I| of values and interprets each function symbol by a function and each predicate symbol by a relation. A state s is a mapping from unprimed flexible variables to values, and a state s is a similar mapping for primed variables. A valuation ξ is a mapping from rigid variables to values. Given an interpretation I, a pair of states (s, s ), and a valuation ξ, the semantics of a TLA + transition formula E is the standard predicate logic semantics of E with respect to the extended valuation of s, s , ξ. With these definitions, M = (I, ξ, s, s ) is a model for E , if E is equivalent to true under M . Let φ be a formula and S ⊆ L. We define φ sliced by S , denoted slice(φ, S ) in Table 4. Below, we show that the branches and slices induced by them naturally decompose a TLA + formula. Let φ be an α-TLA + expression and γ (φ) its corresponding TLA + formula. Then, the following holds: Proposition 5. Let φ be an α-TLA + expression and M = (I, ξ, s, s ) a model of the TLA + formula γ (φ). There exists a branch Br of φ such that M is also a model of γ (slice(φ, Br )). Proposition 6. Let φ be an α-TLA + expression and M = (I, ξ, s, s ) a model of the TLA + formula γ (slice(φ, Br )). Then, M is also a model of γ (φ). Proposition 7. Let φ be an α-TLA + expression. For every S , T ⊆ Labs(φ), every model M of the TLA + formula γ (slice(φ, S )), is also a model of γ (slice(φ, S ∪ T )).

It is easy to see that Proposition 7 does not hold in the other direction. For instance, take the empty set as S and Labs(φ) as T . This implies the following: γ(slice(φ, S )) = false and slice(φ, S ∪ T ) = φ.

Obviously, false cannot have a model, regardless of whether γ(φ) has one or not.

Since Propositions 5 and 6 hold, it would suffice to consider the set Branches(φ), together with an assignment strategy, to generate symbolic transitions. However, it is often the case that, for two distinct branches Br 1 and Br 2 , the same assignments in A are chosen, that is, the intersections Br 1 ∩A and Br 2 ∩A are the same. We show that one can reduce the number of considered symbolic transitions, by analyzing how various branches intersect A.

An assignment strategy A naturally defines an equivalence relation ∼ A on Branches(φ), given by Br 1 ∼ A Br 2 if and only if Br 1 ∩ A = Br 2 ∩ A. We use the notation [Br ] A to refer to the equivalence class of Br by ∼ A , that is, the set {X ∈ Branches(φ) | Br ∼ A X }. Definition 5. Let φ be an α-TLA + expression, A an assignment strategy for φ and Br a branch of φ. Using X = [Br ] A and Y = Z ∈ X Z , we define the symbolic transition generated by Br and A to be slice(φ, Y ). The first assignment strategy A 1 seems to be better than A 2 because A 1 generates fewer symbolic transitions than A 2 . However, in this paper, we do not introduce any metric, by which we could compare assignment strategies. In the implementation, we use any strategy found by the SMT solver.

The equivalence relation ∼ A allows us to define a counterpart to Proposition 7: Proposition 8. Let φ be an α-TLA + expression. For any selection Br 1 , . . . , Br k from the branches of φ, the following holds: If there exists a model M of the formula γ(slice(φ, Br 1 ∪ • • • ∪ Br k )), then M must be a model of γ(slice(φ, Br )), for some branch Br ∈ Branches(φ). Additionally, if there is an assignment strategy A for φ, such that Br 1 , . . . , Br k all belong to the same equivalence class [B ] A , then M must be a model of γ(slice(φ, Br )), for some branch Br ∈ [B ] A .

The following result allows us to use symbolic transitions, not individual branches: Theorem 2. Let φ be an α-TLA + expression and A an assignment strategy for φ. There is a model M of the TLA + formula γ(φ) if and only if there exists a Br ∈ Branches(φ), such that M is a model of γ(ψ), where ψ is the symbolic transition generated by Br and A.

Preliminary Experiments and Potential Applications

Implementation and evaluation. Based on the theory presented in this paper, we have implemented a procedure to find assignment strategies and their corresponding symbolic transitions from TLA + specifications, or report that none exist. It uses Z3 as the background SMT solver.

We have chose specifications both from publicly available sources, e.g. EWD840 and Paxos from [START_REF]A collection of TLA + specifications[END_REF], and from a collection of algorithms we have encoded in TLA + ourselves. For each specification, we focus on the Next formula. We report the number of subexpressions in α(Next), that is, | Sub(α(Next))|, the number of assignments in the strategy found by our procedure, the number of symbolic transitions computed and the total runtime. The results are presented in Table 5. Note that the results for the specification in Fig. 1 are as expected; all assignment candidates must be part of the strategy and we find two symbolic transitions corresponding to Produce and Consume. We also see that the number of symbolic transitions is generally much smaller than the number of transitions an explicit-state model checker would find, as even simple specifications, like in Figure 1, would generate numerous transitions in explicit state model checking, but only two symbolic transitions.

Applications. We illustrate an application of our technique for bounded model checking [START_REF] Biere | Symbolic model checking without BDDs[END_REF] by the means of the example in Figure 3. In this example, three processes pass a unique token in one direction, with the goal of computing the largest process identifier.

Our technique extracts three symbolic transitions T 1 , T 2 , and T 3 , each T i being equivalent to P (i ) ∧ id = id for 1 ≤ i ≤ 3. As common in bounded model checking, with F i,i+1 we denote the SMT encoding of a transition by action F from an i th to an (i +1)-th state. For instance, Next 0,1 and T 3 0,1 encode the transitions from the state 0 to the state 1 by Next and T 3 . Likewise, Init 0 encodes SMT constraints by Init on the initial states. One can use the SMT encodings introduced in [START_REF] Merz | Automatic verification of TLA + proof obligations with SMT solvers[END_REF][START_REF] Merz | Harnessing SMT solvers for TLA+ proofs[END_REF]. Fig. 4: SMT formulas that are constructed when checking the executions up to length 4: using the action Next (left), and using symbolic transitions (right). The gray formulas are excluded from the SMT context during the exploration.

Figure 4 shows the SMT formulas that are constructed by a bounded model checker when exploring executions up to length 4. (For the sake of space, we omit the formulas that check property violation.) On one hand, the monolithic encoding that uses only Next has to keep all the formulas in the SMT context. On the other hand, by incrementally checking satisfiability of the SMT context, the model checker can discover that some formulas -for example, T 2 0,1 and T 3 1,2lead to unsatisfiability and prune them from the SMT context. Similar approach improves efficiency of bounded model checking C programs [START_REF] Biere | Handbook of satisfiability[END_REF][Ch. 16], hence, we expect it to be effective for the verification of TLA + specifications too.

Conclusions

We have introduced a technique to compute symbolic transitions of a TLA + specification by finding expressions that can be interpreted as assignments. Importantly, we designed the technique with soundness in mind. Detailed proofs can be found in the report [START_REF] Kukovec | Extracting symbolic transitions from TLA + specifications[END_REF]. We believe that our results can be used as a first preprocessing step when developing a symbolic model checker or a type checker for TLA + .

As in the case of TLC, one can find TLA + specifications, for which no assignment strategy exists. However, TLA + users are systematically checking their specifications with TLC, in order to find simple errors. Hence, most of the benchmarks already come in a form compatible with TLC. Thus, we expect our approach to also work in practice. Based on these ideas, we are currently developing a symbolic model checker for TLA + .

  module prodcons variable S , empty Init ∆ = S = {} ∧ empty = true Produce ∆ = ∧ empty = false ∧ ∃ X ∈ subset {"A", "B", "Z", "1", "8"} : S = S ∪ {X } Consume ∆ = ¬empty ∧ S ∈ subset S ∧ empty = (S = {}) Next ∆ = Produce ∨ Consume

Next ∆ = 1 :Fig. 2 :

 12 Fig. 2: The Next operator of producer-consumer in α-TLA +

  Boolean structure of a formula and branches. The transformation boolForm maps an α-TLA + expression to a Boolean formula over variables from {b | ∈ L}. The definition of boolForm can be found in Table2. As boolForm(φ) is a formula in Boolean logic, a model of boolForm(φ) is a mapping from {b | ∈ L} to B = {true, false}. Take S ⊆ L. The set S naturally defines a model induced by S , denoted M[S ], by the requirement that M[S ] b if and only if ∈ S . The boolForm transformation allows us to formulate the central notion of a branch: A set Br ⊆ L is called a branch of φ if the following constraints hold: (a) The set Br induces a model of boolForm(φ), i.e., M[Br ] boolForm(φ), and (b) The model M[Br ] is minimal, that is, M[S ] boolForm(φ) for every S ⊂ Br .

Example 3 .

 3 Let us look Example 2 again. The formula φ has two assignment strategies A 1 = { 2 }, and A 2 = { 4 , 5 }. If the first assignment strategy A 1 is chosen, we have that Br 1 ∩ A 1 = Br 2 ∩ A 1 = { 2 }. This implies that Br 1 and Br 2 are in the same equivalence class, or Br 1 ∼ A1 Br 2 . Therefore, we have only one symbolic transition which is exactly φ. However, if A 2 is selected, branches Br 1 and Br 2 are not equivalent because Br 1 ∩ A 2 = { 4 } and Br 2 ∩ A 2 = { 5 }. Therefore, we have two symbolic transitions: T 1 = 1 :: [[ 2 :: x ∈ ] ∧ [ 3 :: [[ 4 :: x ∈ ] ∨ 5 :: false]]] T 2 = 1 :: [[ 2 :: x ∈ ] ∧ [ 3 :: [ 4 :: false ∨ [ 5 :: x ∈ ]]]]

  module max extends Naturals variable tok , max , id Init∆ = tok = 1 ∧ id ∈ [1..3 → Nat] ∧ max = 0 P (i) ∆ = tok = i ∧ tok = 1 + i % 3 ∧ max = if id [i] > max then id [i] else max Next ∆ = (P (1) ∨ P (2) ∨ P (3)) ∧ id = id

Fig. 3 :

 3 Fig. 3: A distributed maximum computation in a ring of three processes in TLA +

Table 1 :

 1 The constraints on frozen φ α-TLA + expression φ Constraints on frozen φ

Table 2 :

 2 The definition of boolForm(φ)

	α-TLA + expression φ	boolForm(φ)
	:: false or :: (v 1 , . . . , v k ) or :: v ∈ φ1	b
	:: s i=1 φi	s i=1 boolForm(φi )
	:: s i=1 φi	s i=1 boolForm(φi )
	:: ∃x ∈ φ1 : φ2	boolForm(φ2)
	:: if φ1 then φ2 else φ3	boolForm(φ2) ∨ boolForm(φ3)

Table 3 :

 3 The definition of δ v (φ)

	α-TLA + expression φ	δ v (φ)
	:: false or :: (v 1 , . . . , v k )	false
	:: w ∈ φ1	b false ; otherwise ; w = v
	:: s i=1 φi	s i=1 δ v (φi )
	:: s i=1 φi	s i=1 δ v (φi )
	:: ∃x ∈ φ1 : φ2	δ v (φ2)

Table 4 :

 4 The definition of slice(φ, S )

	α-TLA + formula φ		slice(φ, S )
	:: false		:: false
	:: (v 1 , . . . , v 1 ) or :: v ∈ φ1	φ	; ∈ S :: false ; otherwise
	:: s i=1 φi		:: s i=1 slice(φi , S )
	:: s i=1 φi		:: s i=1 slice(φi , S )
	:: ∃x ∈ φ1 : φ2	:: ∃x ∈ φ1 : slice(φ2, S )

:: if φ1 then φ2 else φ3 :: if φ1 then slice(φ2, S ) else slice(φ3, S )

Table 5 :

 5 Experimental results

	Specification	#subexpressions	size of #symbolic time
			strategy transitions (ms)
	aba [6]	86	48	8	271
	nbacg [13]	126	82	13	205
	EWD840 [11]	47	16	4	25
	prodcons (Fig. 1)	12	4	2	19
	Paxos [17]	60	16	4	29
	nbac [25]	47	15	14	26
	bcastFolklore [7]	41	17	4	28

Acknowledgments. We are grateful to Stephan Merz for insightful discussions on semantics of TLA + . We thank anonymous reviewers for their helpful suggestions.

Supported by the Vienna Science and Technology Fund (WWTF) through project APALACHE (ICT15-103) and the Austrian Science Fund (FWF) through Doctoral College LogiCS (W1255-N23).


Jure Kukovec
email: jkukovec@forsyte.at

Igor Konnov
email: igor.konnov@inria.fr

Josef Widder
email: widder@forsyte.at

Reachability in Parameterized Systems: All Flavors of Threshold Automata

Keywords: 2012 ACM Subject Classification Software and its engineering → Software verification, Theory of computation → Logic and verification, Software and its engineering → Software fault tolerance threshold & counter automata, parameterized verification, reachability Digital Object Identifier 10.4230/LIPIcs.CONCUR.2018.19

Threshold automata, and the counter systems they define, were introduced as a framework for parameterized model checking of fault-tolerant distributed algorithms. This application domain suggested natural constraints on the automata structure, and a specific form of acceleration, called single-rule acceleration: consecutive occurrences of the same automaton rule are executed as a single transition in the counter system. These accelerated systems have bounded diameter, and can be verified in a complete manner with bounded model checking.

We go beyond the original domain, and investigate extensions of threshold automata: nonlinear guards, increments and decrements of shared variables, increments of shared variables within loops, etc., and show that the bounded diameter property holds for several extensions. Finally, we put single-rule acceleration in the scope of flat counter automata: although increments in loops may break the bounded diameter property, the corresponding counter automaton is flattable, and reachability can be verified using more permissive forms of acceleration.

Introduction

Threshold automata were introduced as a framework for modeling and verification [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF][START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF][START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF][START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF] and recently for synthesis [START_REF] Lazić | Synthesis of distributed algorithms with parameterized threshold guards[END_REF] of fault-tolerant distributed algorithms. These algorithms typically wait for a quorum of messages, e.g., in replication services, the primary replica may block until it received acknowledgments from a majority of the back-up replicas [START_REF] Lamport | The part-time parliament[END_REF][START_REF] Moraru | There is more consensus in egalitarian parliaments[END_REF][START_REF] Dwork | Consensus in the presence of partial synchrony[END_REF][START_REF] Oki | Viewstamped replication: A general primary copy[END_REF]. Moreover, these algorithms are parameterized by design, i.e., the number of processes n is a parameter, and consequently, the primary in our example contains a guard that waits for more than n/2 messages, a so-called threshold guard. As a result, the local transition relation is parameterized, and therefore these systems are out of reach of classic work in parameterized model checking [START_REF] Emerson | Reasoning about rings[END_REF][START_REF] Bloem | Decidability of Parameterized Verification[END_REF].

We recall the necessary notions of threshold automata by the example in Figure 1. It operates on parameters n, t, and f , and shared variables x and y. The vertices are called locations, and the edges are called rules, which can be guarded, and can increase a shared variable. For instance, the threshold guard in rule r 1 compares the value of variable x to a linear expression over parameters n -f . The semantics of threshold automata is defined via counter systems, where a configuration contains the values of shared variables, and a counter value κ i for each location i . The transition relation then is defined by operations on the counters and shared variables. For instance, for some c, if κ 2 ≥ c, then there is a transition defined by rule r 4 that increases κ 4 by c, decreases κ 2 by c and increases x by c.

By allowing arbitrary values of factor c, one obtains a transition relation with a specific form of acceleration (single-rule acceleration), built-in by construction. Then, the transition system is a graph with vertices being configurations, and edges being transitions. By defining paths in this graph, and distances between vertices, one can define the diameter of a transition system. If the diameter d is bounded, then every state is reachable in d steps, and bounded model checking of executions of lengths up to d is a complete verification method for reachability [START_REF] Biere | Symbolic model checking without BDDs[END_REF]. It was shown [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] that the diameter of transition systems defined by threshold automata is bounded, and in particular, it does not depend on the values of the parameters such as n, t, and f . However, several restrictions on threshold automata were used in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] to bound the diameter. While these restrictions are well-justified for the original domain of fault-tolerant algorithms, two questions remain open: (i) which of these restrictions were actually necessary to prove the results under single-rule acceleration, and (ii) which restrictions could be avoided by allowing a more permissive form of acceleration?

The purpose of this paper is to explore various extensions of threshold automata, and understand which of them maintain a bounded diameter. We study extensions of the following properties of threshold automata as defined in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF]:

Increments in loops. Canonical threshold automata defined in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] do not allow updates of shared variables within loops.

Guards. In [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF], threshold guards compare shared variables to a threshold, that is, a linear combination of parameters. Since parameter values are fixed in a run, thresholds are effectively constant. As shared variables can only increase in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF], the guards are monotonic; for instance, once the shared variable is greater than the threshold it stays greater, and the evaluation of the guards stays unchanged after that. We consider more general guards: we replace the shared variables (e.g., x) by a function over shared variables, and consider the special case of a difference (x -y), as well as piecewise monotone functions.

19:3

Reversibility.

In [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF], only increments on shared variables are considered because increments are sufficient to model sending a message. As a result, threshold guards were monotone.

In this paper, we also consider decrements, which produce schedules that have alternating periods of increasing a variable and decreasing it.

For these extensions, we show that under certain conditions these automata entail bounded diameter results as well. Thus, the diameter result of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] can be seen as a special case of the results of this paper.

Finally, we consider threshold automata in the scope of counter automata, a modeling framework for infinite-state systems [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Leroux | Flat counter automata almost everywhere![END_REF][START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]. We consider the concepts of (i) a flat counter automaton, whose control graph does not contain nested loops, and (ii) a flattable counter automaton, for which a flat counter automaton with the same reachability relation exists. For these automata, there are procedures and tools (FAST) for reachability analysis [START_REF] Leroux | Flat counter automata almost everywhere![END_REF][START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]. We will discuss that the results of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF][START_REF] Konnov | Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms[END_REF] imply that canonical threshold automata (no increments in loops) entail flattable counter automata -which explains why FAST verified some benchmarks in the experiments of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF]. Moreover, we show that we can get rid of the canonicity restriction and still prove that the resulting counter automaton is flattable. That is, while non-canonical threshold automata do not fall into the fragment that can be verified with the methods from [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF][START_REF] Konnov | Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms[END_REF], one can still analyze these automata with more permissive forms of acceleration as implemented in FAST.

An overview of our results is in Table 1, where the simpler classes are at the top; these classes are defined in Section 2.3. The bounded diameter property implies flattability, as we show in Proposition 21, which can be seen in the first three lines. For completeness, in line 3, we mention results on reversal-bounded threshold automata rbTA, which consider the structure of runs rather than threshold automata [START_REF] Kukovec | Generalizing threshold automata for reachability in parameterized systems[END_REF]. Note that flattability of a counter automaton implies that reachability for this automaton is decidable [START_REF] Leroux | Flat counter automata almost everywhere![END_REF].

System model

This section generalizes the definitions of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF]. We use the following sets: integers Z and their extension Z ∞ = Z ∪ {-∞, +∞}, non-negative integers N 0 , reals R. We denote a vector of integers by x. When the vector dimension is clear, we write 1 k to denote the unit vector that has 1 at position k and 0 everywhere else, and 0 is the vector filled with zeroes. 2, demonstrating the nonlinear guards and rules that are not considered in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF]. Transitions. Given a UTA A = (L, I, Γ, Π, R), a transition is a pair (rule, factor) where rule ∈ R and factor ∈ N 0 . Note that the single-rule acceleration is built into to the definition of a transition, by allowing factor > 1. We use the notation t.rule and t.factor to refer to the tuple elements of the same name. Additionally, for any tuple field e of t.rule we shorten t.rule.e to t.e for brevity (e.g., t.rule.from becomes t.from).

Unrestricted threshold automata

Semantics of UTA: counter systems

Given a configuration σ and a formula ϕ over the shared variables Γ and parameters Π, we will use the notation (σ. g, σ. p) |= ϕ, or just σ |= ϕ, to mean that the formula ϕ holds true when the shared variables and the parameters are substituted with their respective values from σ. g and σ. p.

We say that a rule r is unlocked in a configuration σ if (σ. g, σ. p) |= ϕ∈r.Φ ϕ. Further, a transition t = (r, a) is unlocked in a configuration σ if r remains unlocked after at least a -1 updates imposed by r. u, that is, for each k ∈ {0, 1, . . . , a -1}, it holds that (σ. g + k • r. u, σ. p) |= ϕ∈r.Φ ϕ. Definition 2. A transition t = (r, a) is applicable to a configuration σ if t is unlocked in σ and σ. κ[r.from] ≥ a. When t is applicable to σ, we call σ the result of applying t to σdenoted as t(σ) -if the requirements 1-3 are met: 1. the location counters are changed by a, that is, σ . κ = σ. κ + a • ( 1 r.to -1 r.from ), 2. the update vector is added a times to the shared variables: σ . g = σ. g + a • r. u, 3. the parameters do not change: σ . p = σ. p. Definition 2 explicitly allows successive applications of the same rule to be compressed into a single transition. This kind of acceleration was introduced in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF], and we call it single-rule acceleration.

Example 3. Consider the automaton in Figure 1. The following table shows a configuration σ 0 , and configurations σ 1 and σ 2 after applying one and two transitions, respectively, to the configuration σ 0 :

configuration counters κ shared variables g parameters p σ0 (4, 0, 0, 0, 0) (0, 0) (4, 1, 1) σ1 (2, 2, 0, 0, 0) (0, 0) (4, 1, 1) σ2 (2, 1, 0, 1, 0) (1, 0) (4, 1, 1)
First, the parameters are initialized to n = 4, t = f = 1, and the counter of location 1 equals to n (configuration σ 0 ). Then, transition (r 3 , 2) is applied to σ 0 , resulting in the counter of 2 increasing by 2 and the counter of 1 decreasing by 2 in configuration σ 1 . Finally, rule r 4 is executed once, incrementing x to obtain σ 2 .

Number of instances.

As in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF], we assume that a threshold automaton is equipped with a function N : N |Π| 0 → N 0 . Intuitively, every configuration σ captures a state of N (σ. p) instances of the threshold automaton. The authors of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] did not restrict function N , as they were concerned only with the length of the shortest sequences of transitions connecting any two configurations. In this paper, we assume that the relation {( p, N ( p)) : p ∈ N |Π| 0 } can be defined with a formula in Presburger arithmetic. In Example 3, we define N with the following formula over the parameters n, t, and f as well as the outcome of the function N :

(n > 3t → N = n -f ∧ f ≥ 0 ∧ t ≥ 0) ∧ (n ≤ 3t → N = 0).
In our example, the number N is positive only if n > 3t, and equals to zero otherwise. This allows us to prune "irrelevant" parameter values. (In distributed computing, this is achieved by writing a so-called resilience condition.)

Counter systems. Having defined the configurations and transitions, we define a counter system of a threshold automaton: Definition 4. Given a UTA A = (L, I, Γ, Π, R), we define its counter system CS(A) as a transition system (Σ, I, R), where:

Σ is the set of all possible configurations. I ⊆ Σ is the set of initial configurations; their counter values in the initial locations sum up to N ( p). Formally, a configuration σ 0 ∈ Σ belongs to I if and only if the following conditions hold: σ 0 . κ[ ] = 0 for ∈ L\I and N (σ 0 . p) = ∈I σ 0 . κ[ ], as well as, σ 0 . g = 0. R ⊆ Σ × Σ is the transition relation. A pair of configurations (σ, σ ) belongs to R if and only if there is a transition t that is applicable to σ, and σ = t(σ).

A schedule is a finite sequence of transitions. A schedule τ = t 1 , . . . , t m is applicable to a configuration σ 0 if there exists a sequence of configurations σ 1 , . . . , σ m where σ i = t i (σ i-1 ) for all 0 < i ≤ m. We define τ (σ 0 ) to be σ m . We denote the concatenation of schedules τ and τ by τ • τ and the length of a schedule τ = t 1 , . . . , t m as |τ | = m. By , we refer to the empty schedule, which has length 0 and satisfies (σ) = σ for all σ in Σ.

For a schedule τ = t 1 , . . . , t n and two indices i, j ∈ Z, we define the subschedule τ [i,j] as follows (τ [i,j) , τ (i,j] , and τ (i,j) are obtained by choosing the intervals accordingly):

τ [i,j] = t max(1,i) , . . . , t min(n,j) , when i ≤ j, , when i > j
We say that a configuration σ is reachable from a configuration σ, if there is a schedule τ with the following properties: (1) τ is applicable to σ, and ( 2)

τ (σ) = σ . C O N C U R 2 0 1 8

19:6 All Flavors of Threshold Automata

Bounded diameters. The central result of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] is that for counter systems of threshold automata one can check, whether one configuration is reachable from another. It is sufficient to inspect the schedules of length within a precomputed bound on the diameter: Definition 5. Given a UTA A and its counter system CS(A) = (Σ, I, R), a number d ∈ N 0 ∪ {∞} is the diameter of CS(A) if d is the smallest number with the following property:

For every pair of configurations σ, σ ∈ Σ, if σ is reachable from σ, then there is a schedule τ such that: (a) τ is applicable to σ, (b) τ (σ) = σ , and (c) |τ | ≤ d.

One of our contributions is in finding fragments of unrestricted threshold automata whose counter systems have a bounded diameter. In Section 4, we give examples of UTA whose counter systems have unbounded diameters. Moreover, we show that there are classes of UTA, for which the following problem -which generalizes the problem from [START_REF] Konnov | Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms[END_REF] -is undecidable:

Parameterized reachability. Given a UTA A = (L, I, Γ, Π, R), a state property B is a Boolean combination of formulas that have the form κ[ ] = 0, for some ∈ L. The parameterized reachability problem is to decide whether there are parameter values p ∈ N |Π| 0 , an initial configuration σ 0 ∈ I, with σ 0 . p = p, and a schedule τ , such that τ is applicable to σ 0 , and property B holds in the final state: τ (σ 0 ) |= B.

Fragments of unrestricted threshold automata

In order to prove the bounded diameter property, we consider various restrictions on the guards, updates, the transition relation, and other aspects of UTA. The first restriction prohibits modifications of shared variables in loops [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF]: Definition 6. A rule r lies on a cycle, if there is a sequence of rules r 0 , . . . , r k , where r = r 0 and r i .to = r j .from for 0 ≤ i ≤ k and j = i + 1 mod (k + 1). A UTA is canonical if r. u = 0 for every rule r ∈ R that lies on a cycle.

Canonical Threshold Automata (TA). This class contains

UTAs with the following properties: (1) they are canonical, (2) all guards are affine, and (3) the update vectors in all rules are non-negative. This is the class of automata considered in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF][START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF], which is known to have a bounded diameter: Theorem 7 ([25]). For every TA A, there exists a constant C, such that the diameter of the associated counter system is less than or equal to d(CS(A)) = (C + 1) • |R| + C (independently of the parameters).

Piecewise Monotone Threshold Automata (PMTA). This class contains UTAs with the following properties: (1) they are canonical, (2) all level functions in the guards are piecewise monotone 1 , and (3) the update vectors in all rules are non-negative.

Bounded Difference Threshold Automata (BDTA). This class contains UTAs with the following properties: (1) they are canonical, (2) all level functions in the guards are of the form x i or x i -x j for some x i , x j ∈ Γ, and (3) the update vectors in all rules are non-negative. Non-canonical generalizations of TA, PMTA, and BDTA. For the mentioned classes, we omit the requirement of the automaton being canonical, and denote these classes as: NCTA, NCPMTA, and NCBDTA.

Reversible of TA, PMTA, and BDTA. For the mentioned classes, we allow shared variables to be both increased and decreased, and denote these classes as: rTA, rPMTA, and rBDTA.

Reversal-bounded extensions of TA, PMTA, and BDTA. To introduce reversal-bounded automata, we need the following definition.

Definition 8. A schedule t 1 • τ • t 2 is an x-reversal if: (a)
one of the transitions t 1 or t 2 increases x and the other decreases x, that is, t 1 . u[x] • t 2 . u[x] < 0, and (b) every transition t in τ does not update x, that is, t. u[x] = 0. If for every shared variable x, the number of x-reversals in a schedule is at most N , the schedule is called N -reversible.

Similar to reversal-bounded counter machines [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], we define the classes rbTA, rbPMTA, and rbBDTA by restricting the counter systems of the respective reversible automata to N -reversible schedules (where N is fixed).

Negative results: unbounded diameters and undecidability

We give examples of NCTA and BDTA whose counter systems have unbounded diameters. Then, we show that reachability is undecidable for counter systems of BDTA and rTA.

Unbounded diameters of non-canonical threshold automata

When we permit shared variables to be updated within loops, the diameter of the counter system becomes unbounded:

Theorem 9.
There is an NCTA whose counter system has unbounded diameter.

Proof. Figure 3 shows such an NCTA, where x is the only shared variable, and n the only parameter. To prove the theorem, take the configuration σ with σ. κ = (1, 0), σ. g = (0), and σ. p = (n) for n > 0. We show that the following configuration σ can be reached from σ in no less than n + 1 transitions: σ . κ = (0, 1), σ . g = (n), and σ . p = (n). In σ, rule r 2 is locked, and rule r 1 is not, so r 1 must be used at least n times to unlock r 2 . Since the sum of the values of location counters initially is 1 and is invariant, we can only use transitions with a factor of at most 1. Thus, to reach σ from σ, we have to execute n copies of the transition (r 1 , 1) and then the transition (r 2 , 1). Hence, the diameter must be at least n + 1, and thus grows with the unbounded parameter n.

The automaton in Figure 3 encodes the simple loop "while (n <= x) x++;" One can argue that this automaton can be accelerated by compressing self-loops into one transition; which requires another form of acceleration. Figure 5 shows an example that cannot be easily fixed by this. This example can be treated with more general acceleration techniques, as demonstrated in Section 6.

Undecidability for reversible and bounded-difference automata

We show even stronger results for rTA and BDTA: reachability is undecidable and thus counter systems of such automata cannot be analyzed with any form of acceleration.

Theorem 10. Parameterized reachability for counter systems of loop-free rTA is undecidable.

Proof. We use rTA to encode two-counter machines 2CM, for which the halting problem is undecidable [START_REF] Marvin | Computation: finite and infinite machines[END_REF]. A command of a 2CM is a triple (from, cmd, to) where from and to are labels from the set {1, . . . , m} for some m, and cmd is one of the operations: inc x, dec x, inc y, dec y, zero? x, zero? y. The label m designates the halting command. For the two counters we use two shared variables x and y. For each label i we also add a shared variable at i , that we use as a Boolean flag to indicate whether the 2CM currently is at label i. There is also a shared variable init, which is used for initialization.

It remains to encode the control structure of a 2CM (which may contain loops) in a threshold automaton without loops. Our rTA has three locations 0 , 1 , 2 , where 0 is the initial one. First, we introduce a special initialization rule from 0 to 1 that is guarded with init < 1 and increments init. Second, for each command we introduce a rule from 0 to 1 . For command (i, cmd, j), the rule is guarded with at i > 0 ∧ init ≥ 1 ∧ init < 2, and e.g., 0 ≥ x ∧ 0 ≤ x, if the test for zero is needed. The update of the rule contains at i --and at j ++ (goto label j from label i), and the required increment/decrement of a counter as e.g., x++ or y--. Third, the last rule detects that the 2CM halted: it goes from 0 to 2 and is guarded with at m ≥ 1.

The number of instances is N (n) = n + 2 for the only parameter n. Thus, n steps of the 2CM are modeled by n + 1 transitions of the constructed counter system; the (n + 2)th transition may move at least one automaton to the location 2 . Hence, the counter system simulates arbitrarily many steps of the 2CM. We ask the parameterized reachability question of whether the counter system reaches a configuration σ with σ. κ[ 2 ] = 0 (for some value of n). A positive answer is given if and only if the 2CM halts; undecidability follows. Now we consider BDTA. Figure 4 shows an example of a BDTA whose counter system has unbounded diameter: Every schedule allowed by this threshold automaton is an alternating sequence of the transitions (r 1 , 1) and (r 2 , 1). Thus to increase the counter κ 2 to n, we require a schedule of length n, which is an unbounded parameter. This shows that sinlge-rule acceleration does not help us to analyze BDTA. In fact, no form of acceleration helps: Theorem 11. Parameterized reachability for counter systems of loop-free BDTA is undecidable.

The proof goes along the same lines as the proof of Theorem 10. The only complication is to encode a decrement of a shared variable by using increments and bounded differences. To this end, for each variable x, we introduce two shared variables x 1 and x 2 . The difference x 1 -x 2 simulates a counter x. Whenever x has to be decremented, we increment x 2 , and when x has to be incremented, we increment x 1 . A test x = 0 is simulated as a conjunction 0

≥ x 1 -x 2 ∧ 0 ≤ x 1 -x 2 .

Positive results: bounding the diameter

We extend the framework and the proofs of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] to prove the bounded diameter property for certain fragments of UTAs. A key observation in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] is that if shared variables are only increased, then the evaluation of every (affine) threshold guard changes at most once in a schedule. This argument obviously applies even if increments occur in loops: Proposition 12 (Monotonicity of affine guards). For an NCTA configuration σ, if a transition t is applicable to σ, then the following holds:

A sufficient condition for diameter boundedness

Proposition 12 does not apply to unrestricted threshold automata for two reasons: First, NCTA only allow shared variables to be incremented, whereas UTA allow both increments and decrements. Obviously, an affine threshold guard such as n ≤ x can change its evaluation arbitrary many times, if increments and decrements of x are alternated (as parameter n is constant in a schedule). Second, even if we restrict updates of shared variables to non-negative vectors, guards such as 0 ≤ x -y can change their evaluations arbitrarily often in a single schedule (cf. Theorem 11). Proposition 12 implies that for every (affine) guard ϕ, when a schedule τ is applied to a configuration σ, schedule τ can be split into two intervals:

τ [1,k) and τ [k,|τ |] with the following property: τ [1,i) (σ) |= ϕ iff σ |= ϕ for 1 ≤ i ≤ k, and τ [1,j] (σ) |= ϕ iff τ (σ) |= ϕ for k ≤ j ≤ |τ |.
In other words, the evaluation of ϕ may only change in the transition from τ [1,k-1] (σ) to τ [1,k] (σ). We extend this idea to non-linear guards by requiring the guards to preserve their evaluations in a bounded number of intervals. In face of Theorem 11, we thus impose two restrictions on UTA: (1) we allow only non-negative updates of shared variables, and (2) we allow level functions to change evaluation of the guards a bounded number of times.

Consider a guard ϕ, a configuration σ, and a schedule τ applicable to σ. We say that τ is steady with respect to (ϕ, σ), if it has the following property:

τ [1,i] (σ) |= ϕ if and only if σ |= ϕ for 1 ≤ i ≤ |τ |.
Definition 13 (Bounded steadiness). We say that a guard ϕ of a UTA A is bounded-steady w.r.t A, if there exists a number N ≥ 0, called the flip bound of ϕ, with the following property:

For every configuration σ of the counter system of A and every schedule τ = t 1 , . . . , t n applicable to σ, there is a sequence of indices 0

= i 0 ≤ i 1 ≤ • • • ≤ i N ≤ i N +1 = n + 1 such that τ (ij ,ij+1) is steady with respect to ϕ and τ [1,ij ] (σ) for 0 ≤ j ≤ N .
Bounded-steadiness is central in proving the bounded diameter property:

Theorem 14 (Bounded diameter criterion). Every canonical UTA A with non-negative updates of shared variables satisfies the following:

If every guard is bounded-steady w.r.t. A, then the diameter of the counter system CS(A) is bounded by a constant.

In the context of TA, constructions are introduced in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] to remove cycles and reorder transitions (to apply acceleration), in order to shorten subschedules in which evaluations of guards do not change, i.e., steady subschedules. The results of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] can be summarized in the following lemma.

C O N C U R 2 0 1 8 19:10 All Flavors of Threshold Automata

Lemma 15. There exists an total order of rules ≺ such that for every schedule τ , there exists a unique schedule, short(τ ), with the following properties: 1. If transition (r, a) appears in short(τ ), then τ contains a transition (r, a ) for some a . 2. If transition (r, a) appears before (r , a ) in short(τ ), then r ≺ r .

3.

If for a configuration σ, an applicable schedule τ is steady with respect to all guards and σ, then short(τ ) is applicable to σ and τ (σ) = short(τ )(σ).

One can prove the above lemma independently of the shape of the guards. For the proof one only uses that in a steady schedule the evaluation of guards does not change. As a result, one can directly apply the proofs from [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] to generalize Lemma 15 to UTA. This allows us to replace a steady schedule τ by short(τ ), which reaches the same state and whose length is bounded by Lemma 15 [START_REF] Aminof | Parameterized model checking of synchronous distributed algorithms by abstraction[END_REF], because threshold automata have a fixed number of rules and ≺ is a total order. What remains to be proven for Theorem 14 is that every schedule of a threshold automaton with bounded-steady guards can be decomposed into a bounded number of steady subschedules.

Proof of Theorem 14. Let ϕ 1 , . . . , ϕ m be the bounded-steady guards. Let σ be a configuration and τ = t 1 , . . . , t n a schedule applicable to it. Since each ϕ j is bounded-steady it has a flip bound N j , for which there exist i j 1 , . . . , i j Nj with the property that τ (i j k ,i j k+1 ) is steady with respect to ϕ j and τ [1,i j k ] (σ) for 0 ≤ k ≤ N j . We denote by S i j the set of critical indices {i j 1 , . . . , i j Nj }. We denote by S the set m j=1 S j , and by i 1 , . . . , i l its elements. Additionally, denote i 0 = 0 and i l+1 = n + 1. The set S partitions τ into finer subschedules than each S j , that is, for every 0 ≤ k ≤ l and for every 1 ≤ j ≤ m there is an index i j p ∈ S j such that the schedule τ (i k ,i k+1 ) is a subschedule of the steady schedule τ (i j p ,i j p+1 ) . Because a subschedule of a steady schedule is also steady by definition (w.r.t. its initial configuration and the same guard), we can conclude that the schedules τ (i k ,i k+1 ) are steady with respect to all guards ϕ j and τ [1,i k ] (σ).

We can therefore apply Lemma 15 to each τ (i k ,i k+1 ) and replace it with a shortened schedule. By property (2) of Lemma 15 and because ≺ is a total order, the length of the shortened schedules is at most |R|. After replacing every τ (i k ,i k+1 ) with short(τ (i k ,i k+1 ) ), we obtain a schedule τ , which is applicable to σ, has the property that τ (σ) = τ (σ) and

|τ | ≤ (|S|+1)•|R|+|S|. By the definition of S, it holds that |S| ≤ m j=1 |S j | ≤ m j=1 N j .

Two fragments with bounded-steady guards

Theorem 14 gives us a sufficient condition for a function to be used in a guard so that the resulting counter system has a bounded diameter. The condition applies to threshold automata with non-negative updates to shared variables. Thus, we can characterize boundedsteady guards by the shape of their level functions. Proposition 16. Every canonical UTA A with non-negative updates of shared variables has the following property: If a threshold guard ϕ has the shape thd( p) F (y) for a shared variable y ∈ Γ, a comparison ∈ {<, ≤, >, ≥}, and a piecewise-monotone function F : Z → R, then the guard ϕ is bounded-steady w.r.t. A.

Example 17. Consider piecewise-monotone functions

f 1 (x), f 2 (x) and reals a n , . . . a 0 , b ∈ R with b > 0. Then, a n • x n + • • • + a 1 • x + a 0 , b x ,
ln x, and min{f 1 (x), f 2 (x)} are piecewisemonotone functions of x ∈ Z. Each of them can be used as F (x) in Proposition 16, and thus they produce bounded-steady guards.

As a corollary of Proposition 16 and Theorem 14, the threshold automata with piecewisemonotone functions in the guards have the bounded diameter property: Corollary 18. For every PMTA, the diameter of its counter system is bounded.

Note that the affine threshold guards of [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] have the shape required in Proposition 16, and thus are just a special case.

We generalize Proposition 16 to guards over multiple shared variables. Recall that an mdimensional integer box is a product of m intervals, that is,

B = Z m ∩ [a 1 , b 1 ] × • • • × [a m , b m ] for some boundaries a 1 , b 1 , . . . , a m , b m ∈ Z ∞ .
Proposition 19. Consider a UTA with non-negative updates of shared variables. A nonlinear guard thd( p) lvl( x), for ∈ {<, ≤, >, ≥}, is bounded-steady, if: For every level C ∈ R, the function domain

Z |Γ| of the level function can be partitioned into a finite set of disjoint |Γ|-dimensional boxes B 1 , . . . , B k that satisfy { x ∈ B i | C lvl( x)} is equal to either B i or ∅ for 1 ≤ i ≤ k.
As a result, the following two-variable functions give us bounded-steady guards:

x + y, x • y, min(f 1 (x), f 2 (y)) or max(f 1 (x), f 2 (y)) for piecewise-monotone f 1 and f 2 5

Relation to flattable counter automata

Counter automata model infinite-state systems and have acceleration procedures and tools for reachability analysis [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Leroux | Flat counter automata almost everywhere![END_REF][START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]. Threshold automata give rise to accelerated counter systems. In this section, we establish a link between these two frameworks. In particular, from a threshold automaton A, we construct two kinds of counter automata: CA 0 (A) is a counter automaton that executes a single UTA rule without any built-in acceleration, and CA 1 (A) is a counter automaton that executes one UTA rule several times in one step. The automaton CA 1 (A) corresponds to our counter system CS(A) in Section 2.2. In our analysis, single-rule acceleration plays a central role in finding diameter bounds, whereas the procedures for counter automata employ more general forms of acceleration. In fact, CA 0 (A) and CA 1 (A) have the same reachability relation, and any of them can in principle be used as the input to the techniques for counter automata. We recall the definitions of counter automata from [START_REF] Leroux | Flat counter automata almost everywhere![END_REF], operating on m counters.

Definition 20. An m-dimensional counter automaton CA is defined as a tuple (Q, T, src, tgt, {G t } t∈T ) with the following properties:

Q and T are finite, non-empty sets of CA-locations and CA-transitions respectively, src : T → Q and tgt : T → Q are the source and target mappings respectively, and {G t } t∈T is a finite family of binary relations on N m called flow guards.

The semantics of the counter automaton CA is defined as a transition system (C CA , → CA ) with the following properties: 1. The set C CA = Q × N m 0 captures CA-configurations, and 2. the relation → CA ⊆ C CA × C CA captures CA-steps. CA makes a step from a configuration (q, x) ∈ C CA to a configuration (q , x ) ∈ C CA via a transition t ∈ T -formally written as (q, x) → CA (q , x ) -if the following holds: q = src(t) and q = tgt(t) and ( x, x ) ∈ G t C O N C U R 2 0 1 8

19:12

All Flavors of Threshold Automata

q 0 n -f ≤ x, 3 = 3 + 1, 1 = 1 -1 y = y + 1, 2 = 2 + 1, 3 = 3 -1 2 = 2 + 1, 1 = 1 -1 x = x + 1, 4 = 4 + 1, 2 = 2 -1 t ≥ y, 5 = 5 + 1, 4 = 4 -1
Figure 6 A counter automaton for the threshold automaton in Figure 1.

A sequence (q 1 , x 1 ), . . . , (q k , x k ) of CA-configurations is called a CA-path, if (q i , x i ) → CA (q i+1 , x i+1 ) for 1 ≤ i < k. Then, the reachability relation

→ * CA ⊆ N |m| 0 × N |m| 0
contains all the pairs of vectors that are connected with a path for some control locations, that is, x → * CA x if and only if there is a CA-path (q 1 , x 1 ), . . . , (q k , x k ) with x = x 1 and x = x k .

A counter automaton without acceleration. Fix an unrestricted threshold automaton A = (L, I, Γ, Π, R), and let P be the set of variables L∪Γ∪Π. To represent the configurations of the UTA counter system, we use vectors x = (x 1 , . . . , x |P | ) ∈ N |P | 0 , where each element x i stores the value of a variable from the set P (there is a bijection). For a vector x ∈ N |P | 0 and a set U ⊆ P , with x| U , we denote the projection of x on the variables from U .

A |P |-dimensional counter automaton CA 0 (A) = (Q, T, src, tgt, {G t } t∈T ) is constructed as follows:

The automaton has only one CA-location, that is, Q = {q 0 } for some q 0 , The CA-transitions are identical to the UTA rules, that is, T = R, Every transition t ∈ T originates from the location q 0 and ends in q 0 ; formally, src(t) = tgt(t) = q 0 , For every rule r ∈ R, the flow relation

G r ⊆ N |P | 0 × N |P |
0 is the intersection of two relations Guard r and Update r that are defined as:

( x, x ) ∈ Guard r if and only if ( x| Γ , x| Π ) |= ϕ∈r.Φ ϕ ( x, x ) ∈ Update r if and only if x | Π = x| Π , (1)
x

| Γ = x| Γ + r. u, and x | L = x| L + 1 r.to -1 r.from (2)
Given the threshold automaton in Figure 1, we construct the respective counter automaton in Figure 6. Apart from the shared variables and parameters, the counter automaton explicitly maintains a counter for each location of UTA, whereas in threshold automata these counters are implicit.

A counter automaton with single-rule acceleration. Given a UTA A, we define its counter automaton with single-rule acceleration CA 1 (A). This automaton is structurally the same as CA 0 (A), except that the flow relation G r for r ∈ R accounts for a non-negative acceleration factor a:

( x, x ) ∈ G r if and only if ∃a ≥ 0. ∀k : 0 ≤ k < a. ( x + k • r. u, x ) ∈ Guard r , x | Π = x| Π , x | Γ = x| Γ + a • r. u, and x | L = x| L + a • ( 1 r.to -1 r.from )
Discussions. If we ignore the location q 0 , the counter automaton CA 1 (A) has the same transition relation as the counter system of A; as defined in Section 2.2 or in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF], that is, with built-in single-rule acceleration. General acceleration procedures for reachability analysis were developed for counter automata [START_REF] Leroux | Flat counter automata almost everywhere![END_REF][START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]. These techniques terminate on flat and flattable counter automata. A counter automaton is flat, if its control graph -built of locations and transitions -does not contain nested loops [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF]. A counter automaton A is flattable, if there is a flat counter automaton F with the same reachability relation, that is,

→ * F = → * A .
The counter automata CA 0 (A) and CA 1 (A) are obviously not flat, as can be seen from Figure 6, the question is whether they are flattable.

As can be seen from the definition of CA 1 (A), single-rule acceleration has a special form: it merges successive occurrences of a rule of CA 0 (A) into one transition, provided that the counter values are sufficiently large. The motivation behind this acceleration is to perform transitions of many processes in a distributed system in parallel [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF], in contrast to compressing sequential steps.

The bounded diameter property for a threshold automaton A implies flattability of the counter automaton CA 0 (A). It is sufficient to unroll CA 0 (A) up to the diameter bound and add self-loops to model single-rule acceleration: Proposition 21. For every unrestricted threshold automaton A, if the diameter of the counter system CS(A) is bounded, then the counter automaton CA 0 (A) is flattable.

Flattability for non-canonical threshold automata

It is easy to see that the counter systems of non-canonical threshold automata do not have bounded diameter, when applying single-rule acceleration. Interestingly, we show that the respective counter automata for NCTA are flattable. Hence, they can be thus analyzed with general acceleration tools such as FAST [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF].

Additional definitions. To prove flattability, we adapt a few definitions from [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF]. Let G = r∈R r.Φ. Then, Φ R = {g ∈ G | g is an upper guard} and Φ F = {g ∈ G | g is a lower guard}. A context is a pair (Ω R , Ω F ), where Ω R ⊆ Φ R and Ω F ⊆ Φ F . The set Ω R keeps track of unlocked guards from Φ R , and the set Ω F keeps track of locked guards from Φ F . We usually denote a context with Ω, and refer to its first and second component by writing Ω R and Ω F respectively. For contexts Ω 1 and Ω 2 , we say that Ω 1 Ω 2 if and only

if Ω R 1 ∪ Ω F 1 ⊆ Ω R 2 ∪ Ω F 2 .
Finally, for a context Ω, we define a formula form(Ω) that summarizes the constraints of the guards that are locked/unlocked in the context: Overview of the proof. We start with an NCTA. The relation is a partial order on the contexts. We construct a flat counter automaton as a composition of flat counter automata, one per context, that are then connected according to the partial order . Figure 7 sketches the construction. In more detail, for each context Ω of A we construct the slice. We show that when one removes the threshold guards from the slice, its counter automaton becomes structurally a BPP-net [START_REF] Esparza | Petri nets, commutative context-free grammars, and basic parallel processes[END_REF][START_REF] Fribourg | A decompositional approach for computing least fixedpoints of datalog programs with z-counters[END_REF], which are known to be flattable [START_REF] Leroux | Flat counter automata almost everywhere![END_REF]. Thus, there is a flattened counter automaton F (Ω) for Ω. However, as F (Ω) does not have threshold guards, it allows transitions to leave the context Ω earlier than in the original counter system. Thus, we add additional constraints to F (Ω) to keep the transitions in the context, and form a "flat slice". Then, we combine flat slices for each context according to the partial order between the contexts, and obtain a flat counter automaton whose reachability relation is the same as of CA 0 (A). Proposition 23. For every non-canonical threshold automaton A and context Ω, there is a flat counter automaton Flat(A| Ω ) that has the same reachability relation when restricted to the CA-configurations that match the context, that is, → * Flat(A| Ω ) ∩ form(Ω) 2 equals to → * CA 0 (A) ∩ form(Ω) 2 .

ψ∈Ψ + ψ ∧ ψ∈Ψ -¬ψ for Ψ + = Ω R ∪ (Φ F \ Ω F ) and Ψ -= (Φ R \ Ω R ) ∪ Ω F . We
Assembling the flat counter automata for the slices. Fix a non-canonical threshold automaton A = (L, I, Γ, Π, R). Proposition 23 allows us to flatten a single slice. To flatten CA 0 (A), we flatten slices and connect them with context changing transitions. As a first step, we enumerate all contexts Ω 1 , . . . , Ω K , where K = |Φ R × Φ F |. For each context i ∈ {1, . . . , K}, we apply Proposition 23, to construct a flat counter automaton Flat(i) = (Q i , T i , src i , tgt i , {G i t } t∈Ti ). We assume that the sets Q 1 , . . . , Q K and T 1 , . . . , T K are all disjoint. We use Flat(1), . . . , Flat(K) to construct two sets of counter automata:

1. An automaton FlatSlice(i) produces paths of CA 0 (A) in the context Ω i . Formally, FlatSlice(i) = (Q i , T i , src i , tgt i , {G i t ∩ form(Ω) 2 } t∈Ti ). 2. An automaton Branch(i, j), for 1 ≤ i, j ≤ K such that Ω i Ω j and i = j, produces the context-changing transitions from FlatSlice(i) to FlatSlice(j). Formally, Branch(i, j) = (Q i ∪ Q j , T i,j , src i,j , tgt i,j , {G i,j t } t∈Ti,j ),

where the components of Branch(i, j) are defined as follows for t ∈ T i : There is a transition for each ith slice transition and jth slice state: T i,j = T i × Q j , The mappings are src i,j ((t, q)) = src i (t) and tgt i,j ((t, q)) = q for q ∈ Q j , and We restrict the guards to the two contexts: G i,j t = G i t ∩ ( form(Ω i ) × form(Ω j ) ).

A flat version of CA 0 (A) is the union of all flat slices and branches:

Flattened(A) = 1≤i≤K
FlatSlice(i)∪ (i,j)∈E Branch(i, j) for E = {(i, j) | Ω i Ω j , i = j} [START_REF] Bar | A tight lower bound for randomized synchronous consensus[END_REF]

r1 : n -f ≤ x r 3 : true r 2 :Figure 1 A

 321 Figure 1 A threshold automaton.

Configurations.

  For a UTA A = (L, I, Γ, Π, R), a triple of vectors ( κ, g, p) ∈ N |L| 0 × Z |Γ| × N |Π| 0 is called a configuration. The vectors have the following meaning: vector κ ∈ N |L| 0 stores the values of the location counters, vector g ∈ Z |Γ| stores the values of the shared variables, and vector N |Π| 0 stores the parameters.

1 2 r 2 :Figure 3

 1223 Figure 3 A simple NCTA.

1 2 r 2 : 1 Figure 4 A

 12214 Figure 4 A BDTA with unbounded diameter.

r 5 :Figure 5

 55 Figure 5 A non-canonical automaton with unbounded diameter.

Definition 22 .

 22 write form(Ω) to denote the set of vectors that satisfy form(Ω), that is, x ∈ form(Ω) if and only if ( x| Γ , x| Π ) |= form(Ω) holds true. For a NCTA A = (L, I, Γ, Π, R) and a context Ω, we define the slice of A with context Ω as a threshold automaton A| Ω = (L, I, Γ, Π, R| Ω ), where a rule r ∈ R belongs to R| Ω if and only if form(Ω) → ϕ∈r.Φ ϕ.

2 ,Figure 7

 27 Figure[START_REF] Bloem | Decidability of Parameterized Verification[END_REF] An example of the flattened threshold automaton from Figure1. The edges connecting the gray blocks connect all the states inside the blocks.

Table 1

 1 Summary of results. "p.m. f (x)" means a piecewise monotone function of x.

	Level	Reversals	Canonical	Bounded diameter?	Flattable?	Decidable reachability?	Class name
	x	0		[25, Thm. 8]			TA
	p.m. f (x)	0		Cor. 18			PMTA
	x	≤ k		[27, Thm. 4]			rbTA
	x	0		Thm. 9 Thm. 24		NCTA
	x -y	0				Thm. 11 BDTA
	x	∞				Thm. 10 rTA

N C U R 2 0 1 8 19:4 All Flavors of Threshold Automata

  Guards.A nonlinear guard of a UTA is a formula: thd( p) lvl( x), where p = [p 1 , . . . , p |Π| ],x = [x 1 , . . . , x |Γ| ], lvl : Z |Γ| → R is the level function, thd : Z |Π| → Ris the threshold function, and is one of {<, ≤, >, ≥}. When is either < or ≤, the guard is called a lower guard, otherwise it is an upper guard. For x ∈ Γ and a 0 , a 1 , . . . , a |Π| ∈ Z, a guard of the following form is called affine: a 0 + |Π| i=1 a i p i x. (Affine guards have only one shared variable.) Rules. A rule is a tuple (from, to, Φ, u) where to, from ∈ L are two local states, Φ is a set of nonlinear guards and u ∈ Z |Γ| is an update vector.

	x++	2 x--, z--n ≤ x 2 + ln y , y ++	true, z++	3 y--	e t > 2 z 3 -x y z		y++, z++,
	1	t + 1 ≤ min{x 2 + y 2 + z 2 , x -z}, y++	4	x--
	Figure 2 An unrestricted threshold automaton.
	Example 1. Consider the automaton in Figure

An unrestricted threshold automaton (UTA) is a tuple (L, I, Γ, Π, R) where L is a finite set of local states (locations), I ⊆ L is a set of initial local states, Γ is a finite set of shared variables, Π is a finite set of parameter variables, and R is a finite set of rules, which are defined below.

C O

The domain of a piecewise monotone function can be decomposed into finitely many intervals where the function is monotone.

Acknowledgements

We thank the anonymous reviewers for spotting a few technical omissions in the preliminary version of this paper.

Funding Supported by the Austrian Science Fund (FWF) via the National Research Network RiSE (S11403, S11405), project PRAVDA (P27722), and Doctoral College LogiCS (W1255-N23); and by the Vienna Science and Technology Fund (WWTF) via project APALACHE (ICT15-103).

We define the union A ∪ B as usual: The states, transitions, and flows of A ∪ B are the unions of the A's and B's states, transitions, and flows respectively. The source and target mappings are identical to the A's and B's mappings on their domains.

Theorem 24. For every non-canonical threshold automaton A, its flattened version has the same reachability relation: →

Conclusions

Verification of infinite-state systems and parameterized concurrent systems is a lively research area, e.g., see some recent results [START_REF] Ganjei | Counting dynamically synchronizing processes[END_REF][START_REF] Durand-Gasselin | Model checking parameterized asynchronous shared-memory systems[END_REF][START_REF] Parosh | Parameterized verification through view abstraction[END_REF][START_REF] Delzanno | A unified view of parameterized verification of abstract models of broadcast communication[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF][START_REF] Drăgoi | A logic-based framework for verifying consensus algorithms[END_REF][START_REF] Maric | Cutoff bounds for consensus algorithms[END_REF][START_REF] Bouajjani | On reducing linearizability to state reachability[END_REF][START_REF] Aminof | Parameterized model checking of synchronous distributed algorithms by abstraction[END_REF]. There are many different modeling frameworks, and it is not easy to understand relations between them. However, this understanding is of paramount importance for reusing existing tools. In this paper, on the one hand, we give reachability results for new classes of systems, and on the other hand, establish the relation of the model in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF][START_REF] Konnov | Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms[END_REF] to counter automata [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Leroux | Flat counter automata almost everywhere![END_REF]. We clarify the relation between the single rule acceleration introduced in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] to acceleration in (flattable) counter automata [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF][START_REF] Leroux | Flat counter automata almost everywhere![END_REF]. The single-rule acceleration in [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF] is very simple compared to the general acceleration techniques [START_REF] Leroux | Flat counter automata almost everywhere![END_REF][START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]. Still, it was demonstrated to be effective in parameterized verification of fault-tolerant distributed algorithms [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF][START_REF] Konnov | Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms[END_REF]. The benefits of our extended framework are two-fold. On one hand, we can use our results to optimize threshold automata. Figure 8 shows an unrestricted threshold automaton that uses minimum and maximum. This UTA can be expressed as an equivalent threshold automaton by introducing more rules and guards (see Figure 8), which makes it harder to reason about. On the other hand, our framework permits some new guards, which have no corresponding encoding in threshold automata. For instance, a threshold x < n/ log n in [START_REF] Bar | A tight lower bound for randomized synchronous consensus[END_REF] gives us such an example (though they are using the synchronous model of computation). Some open questions still remain. Regarding application to distributed algorithms, we observe that in the pseudo code of several distributed consensus algorithms, processes pick the "most often received value" from a set of received values [START_REF] Biely | Tolerating corrupted communication[END_REF][START_REF] Charron-Bost | The heard-of model: computing in distributed systems with benign faults[END_REF]. A shared variable encoding -such as the one in [START_REF] Konnov | Accuracy of message counting abstraction in fault-tolerant distributed algorithms[END_REF] -maintains the number of messages with value 0 in a shared variable x 0 , and the number of messages with value 1 in a shared variable x 1 . The pseudo code statement about the "most often received value" needs a bounded difference guard "x 1 -x 0 > 0", which leads to undecidability as we show. This calls for further insights on modeling of such algorithms.

While we focused on reachability in this paper, as future work, we plan to lift the results of this paper to safety and liveness, following the ideas of [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF].