{'fraction_non_alphanumeric': 0.052859801271022785, 'fraction_numerical': 0.00981355991713774, 'mean_word_length': 3.8151310228233304, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 21, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Revisiting Parameter Synthesis for One-Counter Automata

We study the (parameter) synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some omega-regular property. Lechner showed that (the complement of) the problem can be encoded in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment, called AERPADPLUS, is unfortunately undecidable. Nevertheless, by a careful re-encoding of the problem into a decidable restriction of AERPADPLUS, (ii) we prove that the synthesis problem is decidable in general and in N2EXP for several fixed omega-regular properties. Finally, (iii) we give a polynomial-space algorithm for the special case of the problem where parameters can only be used in tests, and not updates, of the counter.

On the left, the CFG with vertex labels corresponding to source code line numbers; on the right, the CFG extended by tracking the value of i non-determinism. Hence, the question becomes: "is it the case that all paths from the initial vertex avoid the one labelled with 10?" In this particular example, the abstraction is too coarse and thus we obtain a false negative. In such cases, the abstraction of the program should be refined [9]. A natural refinement of the CFG in this context is obtained by tracking the value of i (cf. program graphs in [2]). The result is an OCA with parameters such that: For x ∈ {0, 1} it has no run that reaches the state labelled with 10. This is an instance of a safety (parameter) synthesis problem for which the answer is positive.
In this work, we focus on the parameter synthesis problems for given OCA with parameters and do not consider the problem of obtaining such an OCA from a program (cf. [11]).
Counter automata [30] are a classical model that extend finite-state automata with integervalued counters. These have been shown to be useful in modelling complex systems, such as programs with lists and XML query evaluation algorithms [5,8]. Despite their usefulness as a modelling formalism, it is known that two counters suffice for counter automata to become Turing powerful. In particular, this means that most interesting questions about them are undecidable [30]. To circumvent this, several restrictions of the model have been studied in the literature, e.g. reversal-bounded counter automata [19] and automata with a single counter. In this work we focus on an extension of the latter: OCA with parametric updates and parametric tests.
An existential version of the synthesis problems for OCA with parameters was considered by Göller et al. [13] and Bollig et al. [4]. They ask whether there exist a valuation of the parameters and a run of the automaton which satisfies a given ω-regular property. This is in contrast to the present problem where we quantify runs universally. (This is required for the conservative-approximation use case described in the example above.) We note that, of those two works, only [13] considers OCA with parameters allowed in both counter updates and counter tests while [4] studies OCA with parametric tests only. In this paper, unless explicitly stated otherwise, we focus on OCA with parametric tests and updates like in [13]. Further note that the model we study has an asymmetric set of tests that can be applied to the counter: lower-bound tests, and equality tests (both parametric and non-parametric). The primary reason for this is that adding upper-bound tests results in a model for which even the decidability of the (arguably simpler) existential reachability synthesis problem is a long-standing open problem [7]. Namely, the resulting model corresponds to Ibarra's simple programs [18].
In both [13] and [4], the synthesis problems for OCA with parameters were stated as open. Later, Lechner [22] gave an encoding for the complement of the synthesis problems into a one-alternation fragment of Presburger arithmetic with divisibility (PAD). Her encoding relies on work by Haase et al. [17], which shows how to compute a linear-arithmetic representation of the reachability relation of OCA (see [25] for an implementation). In the same work, Haase et al. show that the same can be achieved for OCA with parameters using the divisibility predicate. In [22], Lechner goes on to consider the complexity of (validity of sentences in) from [6] works correctly. For completeness, and to clarify earlier mistakes in the literature, we recall Lechner's analysis of the algorithm and conclude, just as she did, that the complexity of BIL is in co2NEXP [22] (Theorem 4). After some preliminaries regarding OCA with parameters in Section 3, we re-establish decidability of various synthesis problems in Section 4 (Theorem 10 and Corollary 17, see Table 1 for a summary). To do so, we follow Lechner's original idea from [22] to encode them into ∀∃ R PAD + sentences. However, to ensure we obtain a BIL sentence, several parts of her encoding have to be adapted. Finally, in Section 5 we make small modifications to the work of Bollig et al. [4] to give more efficient algorithms that are applicable when only tests have parameters (Theorem 18 and Corollary 19).

Presburger Arithmetic with divisibility
Presburger arithmetic (PA) is the first-order theory over ⟨Z, 0, 1, +, <⟩ where + and < are the standard addition and ordering of integers. Presburger arithmetic with divisibility (PAD) is the extension of PA obtained when we add the binary divisibility predicate |, where for all a, b ∈ Z we have a | b ⇐⇒ ∃c ∈ Z : b = ac. Let X be a finite set of first-order variables. A linear polynomial over x = (x 1 , . . . , x n ) ∈ X n is given by the syntax rule: p(x) ::= 1≤i≤n a i x i + b, where the a i , b and the first-order variables from x range over Z.
In general, quantifier-free PAD formulas have the grammar: φ : where P can be the order predicate < or the divisibility predicate |, and f, g are linear polynomials. We define the standard Boolean abbreviation φ 1 ∨ φ 2 ⇐⇒ ¬(¬φ 1 ∧ ¬φ 2 ). Moreover we introduce the abbreviations f ( The size |φ| of a PAD formula φ is defined by structural induction over |φ|: For a linear polynomial p(x) we define |p(x)| as the number of symbols required to write it if the coefficients are given in binary. Then, we define

Allowing one restricted alternation
We define the language ∀∃ R PAD of all PAD sentences allowing a universal quantification over some variables, followed by an existential quantification over variables that may not appear on the left-hand side of divisibility constraints. Formally, ∀∃ R PAD is the set of all PAD sentences of the form: ∀x 1 . . . ∀x n ∃y 1 . . . ∃y m φ(x, y) where φ is a quantifier-free PAD formula and all its divisibility constraints are of the form f (x) | g(x, y).
Positive-divisibility fragment. We denote by ∀∃ R PAD + the subset of ∀∃ R PAD sentences φ where the negation operator can only be applied to the order predicate < and the only other Boolean operators allowed are conjunction and disjunction. In other words, ∀∃ R PAD + is a restricted negation normal form in which divisibility predicates cannot be negated. Lechner showed in [22] that all ∀∃ R PAD sentences can be translated into ∀∃ R PAD + sentences.

Undecidability of both one-alternation fragments
We will now prove that the language ∀∃ R PAD + is undecidable, that is, to determine whether a given sentence from ∀∃ R PAD + is true is an undecidable problem.
From Proposition 1 it follows that arguing ∀∃ R PAD is undecidable suffices to prove the theorem. The latter was proven in [6]. More precisely, they show the complementary language is undecidable. Their argument consists in defining the least-common-multiple predicate, the squaring predicate, and subsequently integer multiplication. Undecidability thus follows from the MRDP theorem [29] which states that satisfiability for such equations (i.e. Hilbert's 10th problem) is undecidable. Hence, Theorem 2 is a direct consequence of the following result.

The Bozga-Iosif-Lechner fragment
The Bozga-Iosif-Lechner (BIL) fragment is the set of all ∀∃ R PAD + sentences of the form: where I, J i ⊆ N are all finite index sets, the f j and g j are linear polynomials and the φ i (x) are quantifier-free PA formulas over the variables x. Note that, compared to ∀∃ R PAD + , BIL sentences only constraint non-negative values of x. (This technicality is necessary due to our second constraint below.) For readability, henceforth, we omit (x < 0) and just assume the x take non-negative integer values, i.e. from N. Additionally, it introduces the following three important constraints: 1. The y variables may only appear on the right-hand side of divisibility constraints.

All divisibility constraints
The y variables are only allowed to take non-negative values.
It should be clear that the first constraint is necessary to avoid undecidability. Indeed, if the y variables were allowed in the PA formulas φ i (x) then we could circumvent the restrictions of where they appear in divisibilities by using equality constraints. The second constraint is similar in spirit. Note that if a = 0 then a | b holds if and only if b = 0 so if the left-hand side of divisibility constraints is allowed to be 0 then we can encode PA formulas on x and y as before. Also, the latter (which was missing in [6,22]) will streamline the application of the generalized Chinese remainder theorem in the algorithm described in the sequel. While the third constraint is not required for decidability, it is convenient to include it for Section 4, where we encode instances of the synthesis problem into the BIL fragment.
In the rest of this section, we recall the decidability proof by Bozga and Iosif [6] and refine Lechner's analysis [22] to obtain the following complexity bound.
The idea of the proof is as follows: We start from a BIL sentence. First, we use the generalized Chinese remainder theorem (CRT, for short) to replace all of the existentially quantified variables in it with a single universally quantified variable. We thus obtain a sentence in ∀PAD (i.e. the Π 0 -fragment of PAD) and argue that the desired result follows from the bounds on the bitsize of satisfying assignments for existential PAD formulas [24].
▶ Theorem 5 (Generalized Chinese remainder theorem [21]). (ai,mi). From a BIL sentence, we apply the CRT to the rightmost existentially quantified variable and get a sentence with one less existentially quantified variable and with gcd-expressions. Observe that the second restriction we highlighted for the BIL fragment (the conjunction with f j (x) > 0) is necessary for the correct application of the CRT. We will later argue that we can remove the gcd expressions to obtain a sentence in ∀PAD.
▶ Example 6. Consider the sentence: Let α j denote the coefficient of y 2 in g j (x, y) and r j (x, y 1 ) def = −(g j (x, y) − α j y 2 ). We can rewrite the above sentence as ∀x∃y 1 i∈I ψ i (x, Applying the CRT, ψ i (x, y 1 ) can equivalently be written as follows: Note that we have dropped the y 2 ≥ 0 constraint without loss of generality since the CRT states that the set of solutions forms an arithmetic progression containing infinitely many positive (and negative) integers. This means the constraint will be trivially satisfied for any valuation of x and y 1 which satisfies ψ i (x, y 1 ) ∧ φ i (x) ∧ y 1 ≥ 0 for some i ∈ I. Observe that y 1 only appears in polynomials on the right-hand side of divisibilities.
The process sketched in the example can be applied in general to BIL sentences sequentially starting from the rightmost quantified y i . At each step, the size of the formula is at most squared. In what follows, it will be convenient to deal with a single polyadic gcd instead of nested binary ones. Thus, using associativity of gcd and pushing coefficients inwards -i.e. using the equivalence a · gcd(x, y) ≡ gcd(ax, ay) for a ∈ N -we finally obtain a sentence: where |L i |, |K j |, and the coefficients may all be doubly-exponential in the number m of removed variables, due to iterated squaring.
Eliminating the gcd operator. In this next step, our goal is to obtain an ∀PAD sentence from Equation (1). Recall that ∀PAD "natively" allows for negated divisibility constraints.
(That is, without having to encode them using Lechner's trick.) Hence, to remove expressions in terms of gcd from Equation (1), we can use the following identity: This substitution results in a constant blowup of the size of the sentence. To prove Theorem 4, the following small-model results for purely existential PAD formulas and BIL will be useful.
Proof. Using Lemma 7, we translate the BIL sentence to ∀x 1 . . . ∀x n ∀dψ(x, d), where the latter is an ∀PAD sentence. Then, using Theorem 8, we get that the ∃PAD formula ¬ψ(x, d) admits a solution if and only if it has one with bitsize bounded by |ψ| poly(n+1) . Now, from Lemma 7 we have that |ψ| is bounded by |φ| 2 m . Hence, we get that the bitsize of a solution is bounded by: |φ| 2 m poly(n+1) . ◀ We are now ready to prove the theorem.
Proof of Theorem 4. As in the proof of Corollary 9, we translate the BIL sentence to ∀x 1 . . . ∀x n ∀dψ(x, d). Note that our algorithm thus far runs in time: O |φ| 2 m . By Corollary 9, if ¬ψ(x, d) has a solution then it has one encodable in binary using a doubly exponential amount of bits with respect to the size of the input BIL sentence. The naive guess-and-check decision procedure applied to ¬ψ(x, d) gives us a co2NEXP algorithm for BIL sentences. Indeed, after computing ψ(x, d) and guessing a valuation, checking it satisfies ¬ψ takes polynomial time in the bitsize of the valuation and |ψ|, hence doubly exponential time in |φ|. ◀

Succinct One-Counter Automata with Parameters
We now define OCA with parameters and recall some basic properties. The concepts and observations we introduce here are largely taken from [17] and the exposition in [23].
A succinct parametric one-counter automaton (SOCAP) is a tuple A = (Q, T, δ, X), where Q is a finite set of states, X is a finite set of parameters, T ⊆ Q × Q is a finite set of transitions and δ : T → Op is a function that associates an operation to every transition.
We denote by "= 0" or "= x" an equality test between the value of the counter and zero or the value of x respectively; by "≥ x", a lower-bound test between the values of the counter and x. A valuation V : X → N assigns to every parameter a natural number. We assume CU are encoded in binary, hence the S in SOCAP. We omit "parametric" if X = ∅ and often write q op −→ q ′ to denote δ(q, q ′ ) = op. A configuration is a pair (q, c) where q ∈ Q and c ∈ N is the counter value. Given a valuation V : X → N and a configuration (q 0 , c 0 ), a V -run from (q 0 , c 0 ) is a sequence ρ = (q 0 , c 0 )(q 1 , c 1 ) . . . such that for all i ≥ 0 the following hold: is "= 0", "= x", and "≥ x", respectively; and c i+1 is obtained from c i based on the counter operations. That is, We extend the weight function to finite paths in the natural way. Namely, we set weight(q 0 . . . q n ) Synthesis problems. The synthesis problem asks, given a SOCAP A, a state q and an ω-regular property p, whether there exists a valuation V such that all infinite V -runs from (q, 0) satisfy p. We focus on the following classes of ω-regular properties. Given a set of target states F ⊆ Q and an infinite run ρ = (q 0 , c 0 )(q 1 , c 1 ) . . . we say ρ satisfies: the linear temporal logic (LTL) formula φ over a set of atomic propositions P -and with respect to a labelling function f : 1 We will decompose the synthesis problems into reachability sub-problems. It will thus be useful to recall the following connection between reachability (witnesses) and graph flows.
That is, the total incoming flow equals the total outgoing flow for all but the source and the target vertices. We then define the value of a flow f as:

Path flows. Consider a path
We denote by f π its Parikh image, i.e. f π maps each edge e to the number of times e occurs in π. A flow f is called a path flow if there exists a path π such that f = f π . Finally, we observe that an

Encoding Synthesis Problems into the BIL Fragment
In this section, we prove that all our synthesis problems are decidable. More precisely, we establish the following complexity upper bounds.
▶ Theorem 10. The reachability, Büchi, coBüchi, and safety synthesis problems for succinct one-counter automata with parameters are all decidable in 2NEXP.
The idea is as follows: we focus on the coBüchi synthesis problem and reduce its complement to the truth value of a BIL sentence. To do so, we follow Lechner's encoding of the complement of the Büchi synthesis problem into ∀∃ R PAD + [22]. The encoding heavily relies on an encoding for (existential) reachability from [17]. We take extra care to obtain a BIL sentence instead of an ∀∃ R PAD + one as Lechner originally does. It can be shown that the other synthesis problems reduce to the coBüchi one in polynomial time. The corresponding bounds thus follow from the one for coBüchi synthesis. The proof of the following lemma is given in the long version of the paper.
▶ Lemma 11. The reachability, safety and the Büchi synthesis problems can be reduced to the coBüchi synthesis problem in polynomial time.
Now the cornerstone of our reduction from the complement of the coBüchi synthesis problem to the truth value of a BIL sentence is an encoding of reachability certificates into ∀∃ R PAD formulas which are "almost" in BIL. In the following subsections we will focus on a SOCAP A = (Q, T, δ, X) with X = {x 1 , . . . , x n } and often write x for (x 1 , . . . , x n ). We will prove that the existence of a V -run from (q, c) to (q ′ , c ′ ) can be reduced to the satisfiability problem for such a formula.
▶ Proposition 12. Given states q, q ′ , one can construct in deterministic exponential time in |A| a PAD formula: φ are quantifier-free PA formulas, and additionally: reach | is at most exponential with respect to |A|; and the number of y variables is polynomial with respect to |A|.
Below, we make use of this proposition to prove Theorem 10. Then, we prove some auxiliary results in Section 4.1 and, in Section 4.2, we present a sketch of our proof of Proposition 12.
We will argue that ∀x∃a∃bφ reach (x, a, b) can be transformed into an equivalent BIL sentence. Note that for this to be the case it suffices to remove the ψ i (y, a, b) subformulas. Intuitively, since these are quantifier-free PA formulas, their set of satisfying valuations is semi-linear (see, for instance, [16]). Our intention is to remove the ψ i (y, a, b) and replace the occurrences of y, a, b in the rest of φ (q,q ′ ) reach (x, a, b) with linear polynomials "generating" their set of solutions. This is formalized below.
Affine change of variables. Let A ∈ Z m×n be an integer matrix of size m × n of rank r, and b ∈ Z m . Let C ∈ Z p×n be an integer matrix of size p × n such that ( A C ) has rank s, and d ∈ Z p . We write µ for the maximum absolute value of an (s − 1) ▶ Theorem 13 (From [36]). Given integer matrices A ∈ Z m×n and C ∈ Z p×n , integer vectors b ∈ Z m and d ∈ Z p , and µ defined as above, there exists a finite set I, a collection of n×(n−r) matrices E (i) , and n × 1 vectors u (i) , indexed by i ∈ I, all with integer entries bounded by We are now ready to prove Theorem 10.
Proof of Theorem 10. We will first prove that the complement of the coBüchi synthesis problem can be encoded into a BIL sentence. Recall that the complement of the coBüchi synthesis problem asks: given a SOCAP A with parameters X, for all valuations does there exist an infinite run from a given configuration (q, 0), that visits the target set F infinitely many times. Without loss of generality, we assume that the automaton has no parametric tests as they can be simulated using parametric updates and zero tests.
The idea is to check if there exists a reachable "pumpable cycle" containing one of the target states. Formally, given the starting configuration (q, 0), we want to check if we can reach a configuration (q f , k), where q f ∈ F and k ≥ 0 and then we want to reach q f again via a pumpable cycle. This means that starting from (q f , k) we reach the configuration (q f , k) again or we reach a configuration (q f , k ′ ) with k ′ ≥ k without using zero-test transitions. Note that reachability while avoiding zero tests is the same as reachability in the subautomaton obtained after deleting all the zero-test transitions. We write φ reach−nt for the φ reach formula constructed for that sub-automaton as per Proposition 12. The above constraints can be encoded as a formula φ k, k) . Finally, the formula φ Büchi (x) will look as follows: where, by Proposition 12, the φ i (x) are quantifier-free PA formulas over x constructed by grouping all the quantifier-free PA formulas over x. Similarly, we can construct ψ i (y, k, k ′ ) by grouping all the quantifier free formulas over y, k and k ′ . Now, we use the affine change of variables to remove the formulas ψ i (y, k, k ′ ). Technically, the free variables from the subformulas ψ i will be replaced in all other subformulas by linear polynomials on newly introduced variables z. Hence, the final formula φ Büchi (x) becomes: Note that, after using the affine change of variables, the number of z variables is bounded by the number of old existentially quantified variables (y, k, k ′ ). However, we have introduced exponentially many new disjuncts. 2 By construction, for a valuation V there is an infinite V -run in A from (q, 0) that visits the target states infinitely often iff φ Büchi (V (x)) is true. Hence, ∀x(x < 0 ∨ φ Büchi (x)) precisely encodes the complement of the coBüchi synthesis problem. Also, note that it is a BIL sentence since the subformulas (and in particular the divisibility constraints) come from our usage of Proposition 12. Now, the number of z variables, say m, is bounded by the number of y variables before the affine change of variables which is polynomial with respect to |A| from Proposition 12. Also, the bitsize of the constants in φ Büchi is polynomial in |A| though the size of the formula is exponential in |A|. Now, using Lemma 7, we construct an ∀PAD sentence ∀x∀dψ(x, d) from ∀x(x < 0 ∨ φ Büchi (x)). By Corollary 9, ¬ψ admits a solution of bitsize bounded by: exp(ln(|φ Büchi |)2 m poly(n + 1)) = exp(|A| · 2 poly(|A|) poly(n + 1)), which is doubly exponential in the size of |A|. As in the proof of Theorem 4, a guess-and-check algorithm for ¬ψ gives us the desired 2NEXP complexity result for the coBüchi synthesis problem. By Lemma 11, the other synthesis problems have the same complexity. ◀ In the sequel we sketch our proof of Proposition 12.

Reachability certificates
We presently recall the notion of reachability certificates from [17]. Fix a SOCAP A and a valuation V . A flow f in G A is a reachability certificate for two configurations (q, c), that induces a path π such that f = f π and one of the following holds: (type 1) f has no positive-weight cycles, (type 2) f has no negative-weight cycles, or (type 3) f has a positive-weight cycle that can be taken from (q, c) and a negative-weight cycle that can be taken to (q ′ , c ′ ).
In the sequel, we will encode the conditions from the following result into a PAD formula so as to accommodate parameters. Intuitively, the proposition states that there is a run from (q, c) to (q ′ , c ′ ) if and only if there is one of a special form: a decreasing prefix (type 1), a positive cycle leading to a plateau followed by a negative cycle (type 3), and an increasing suffix (type 2). Each one of the three sub-runs could in fact be an empty run.
Encoding the certificates. Now, we recall the encoding for the reachability certificates proposed by Lechner [22,23]. Then, we highlight the changes necessary to obtain the required type of formula. We begin with type-1 and type-3 certificates.
) that induces a path π with f π a type-t reachability certificate.
The formulas Φ (q,q ′ ) t from the result above look as follows: where |I| and the size of each disjunct are exponential. 3 Further, all the φ i and ψ i are quantifier-free PA formulas and the m j (x) are all either x, −x, or n ∈ N >0 .
We observe that the constraint (m j (x) > 0 ↔ z j > 0) regarding when the variables can be 0, can be pushed into a further disjunction over which subset of X is set to 0. In one case the corresponding m j (x)'s and z j 's are replaced by 0, in the remaining case we add to φ i and ψ i the constraints z j > 0 and m j (x) > 0 respectively. We thus obtain formulas Ψ (q,q ′ ) t (x, a, b) with the following properties.
▶ Lemma 16. Suppose A has no zero tests and let t ∈ {1, 2, 3}. Given states q, q ′ , one can construct in deterministic exponential time a PAD formula Ψ y, a, b) are quantifier-free PA formulas, and additionally: that induces a path π such that f π is a type-t reachability certificate, the bitsize of constants in Ψ (q,q ′ ) t is of polynomial size in |A|, |Ψ (q,q ′ ) t | is at most exponential with respect to |A|, and the number of y variables is polynomial with respect to |A|.

Putting everything together
In this section, we combine the results from the previous subsection to construct φ reach for Proposition 12. The construction, in full detail, and a formal proof that φ reach enjoys the claimed properties are given in the long version of this paper. First, using Proposition 14 and the lemmas above, we define a formula φ To do so, we use formulas for the sub-automaton obtained by removing from A all zero-test transitions. Then, the formula φ (q,q ′ ) reach (x, a, b) expressing general reachability can be defined by taking a disjunction over all orderings on the zero tests. In other words, for each enumeration of zero-test transitions we take the conjunction of the intermediate φ reach−nt formulas as well as φ reach−nt formulas from the initial configuration and to the final one.
Recall that for any LTL formula φ we can construct a universal coBüchi automaton of exponential size in |φ| [2,20]. (A universal coBüchi automaton accepts a word w if all of its infinite runs on w visit F only finitely often. Technically, one can construct such an automaton for φ by constructing a Büchi automaton for ¬φ and "syntactically complementing" its acceptance condition.) By considering the product of this universal coBüchi automaton and the given SOCAP, the LTL synthesis problem reduces to coBüchi synthesis.
▶ Corollary 17. The LTL synthesis problem for succinct one-counter automata with parameters is decidable in 3NEXP.

One-Counter Automata with Parametric Tests
In this section, we introduce a subclass of SOCAP where only the tests are parametric. The updates are non-parametric and assumed to be given in unary. Formally, OCA with parametric tests (OCAPT) allow for constant updates of the form {+a : a ∈ {−1, 0, 1}} and zero and parametric tests. However, PU = ∅. We consider the synthesis problems for OCAPT. Our main result in this section are better complexity upper bounds than for general SOCAP. Lemma 11 states that all the synthesis problems reduce to the coBüchi synthesis problem for SOCAP. Importantly, in the construction used to prove Lemma 11, we do not introduce parametric updates. Hence, the reduction also holds for OCAPT. This allows us to focus on the coBüchi synthesis problemthe upper bounds for the other synthesis problems follow. To prove the theorem, we follow an idea from [4] to encode parameter valuations of OCAPT into words accepted by an alternating two-way automaton. Below, we give the proof of the theorem assuming some auxiliary results that will be established in the following subsections.
Proof. In Proposition 21, we reduce the coBüchi synthesis problem to the non-emptiness problem for alternating two-way automata. Hence, we get the PSPACE upper bound. Since the Büchi and the safety synthesis problems reduce to the coBüchi one (using Lemma 11) in polynomial time, these are also in PSPACE.
Next, we improve the complexity upper bound for the reachability synthesis problem from PSPACE to NP NP . In Lemma 22 we will prove that if there is a valuation V of the parameters such that all infinite V -runs reach F then we can assume that V assigns to each x ∈ X a value at most exponential. Hence, we can guess their binary encoding and store it using a polynomial number of bits. Once we have guessed V and replaced all the x i by V (x i ), we obtain a non-parametric one counter automata A ′ with X = ∅ and we ask whether all infinite runs reach F . We will see in Proposition 23 that this problem is in coNP. The claimed complexity upper bound for the reachability synthesis problem follows. ◀ Using a similar idea to Corollary 17, we reduce the LTL synthesis problem to the coBüchi one and we obtain the following.
▶ Corollary 19. The LTL synthesis problem for OCAPT is in EXPSPACE.

Alternating two-way automata
Given a finite set Y , we denote by B + (Y ) the set of positive Boolean formulas over Y , including true and false. A subset Y ′ ⊆ Y satisfies β ∈ B + (Y ), written Y ′ |= β, if β is evaluated to true when substituting true for every element in Y ′ , and false for every element in Y \ Y ′ . In particular, we have ∅ |= true.
We can now define an alternating two-way automaton (A2A, for short) as a tuple T = (S, Σ, s in , ∆, S f ), where S is a finite set of states, Σ is a finite alphabet, s in ∈ S is the initial state, S f ⊆ S is the set of accepting states, and ∆ ⊆ S × (Σ ∪ {first?}) × B + (S × {+1, 0, −1}) is the finite transition relation. The +1 intuitively means that the head moves to the right; −1, that the head moves to the left; 0, that it stays at the current position. Furthermore, transitions are labelled by Boolean formulas over successors which determine whether the current run branches off in a non-deterministic or a universal fashion.
A run is accepting if all of its infinite branches contain infinitely many labels from S f × N. The language of T is L(T ) def = {w ∈ Σ ω | ∃ an accepting run of T on w from 0}. The non-emptiness problem for A2As asks, given an A2A T and n ∈ N, whether L(T ) ̸ = ∅.

▶ Proposition 20 (From [33]). Language emptiness for A2As is in PSPACE.
In what follows, from a given OCAPT A we will build an A2A T such that T accepts precisely those words which correspond to a valuation V of X under which all infinite runs satisfy the coBüchi condition. Hence, the corresponding synthesis problem for A reduces to checking non-emptiness of T .

Transformation to alternating two-way automata
Following [4], we encode a valuation V : X → N as an infinite parameter word w = a 0 a 1 a 2 . . . over the alphabet Σ = X ∪ {□} such that a 0 = □ and, for every x ∈ X, there is exactly one position i ∈ N such that a i = x. We write w(i) to denote its prefix a 0 a 1 . . . a i up to the letter a i . By |w(i)| □ , we denote the number of occurrences of □ in a 1 . . . a i . (Note that we ignore a 0 .) Then, a parameter word w determines a valuation V w : x → |w(i)| □ where a i = x. We denote the set of all parameter words over X by W X .
From a given OCAPT A = (Q, T, δ, X), a starting configuration (q 0 , 0) and a set of target states F , we will now construct an A2A T = (S, Σ, s in , ∆, S f ) that accepts words w ∈ W X such that, under the valuation V = V w , all infinite runs from (q 0 , 0) visit F only finitely many times. The construction is based on the A2A built in [4], although we make more extensive use of the alternating semantics of the automaton. To capture the coBüchi condition, we simulate a safety copy with the target states as "non-accepting sink" (states having a self-loop and no other outgoing transitions) inside T . Simulated accepting runs of A can "choose" to enter said safety copy once they are sure to never visit F again. Hence, for every state q in A, we have two copies of the state in T : q ′ ∈ S representing q normally and q ′′ ∈ S representing q from the safety copy. Now the idea is to encode runs of A as branches of run trees of T on parameter words w by letting sub-trees t whose root is labelled with (q ′ , i) or (q ′′ , i) correspond to the configuration (q, |w(i)| □ ) of A. If t is accepting, it will serve as a witness that all infinite runs of A from (q, |w(i)| □ ) satisfy the coBüchi condition.
We present the overview of the construction below with some intuitions. A detailed proof of Proposition 21 is given in the long version of the paper.
The constructed A2A T for the given A is such that for every q ∈ Q, there are two copies q ′ , q ′′ ∈ S as mentioned earlier. We also introduce new states in T as required. The A2A includes a sub-A2A that verifies that the input word is a valid parameter word. For every x i , a branch checks that it appears precisely once in the parameter word. From a run sub-tree whose root is labelled with (q ′ , i) or (q ′′ , i), the A2A verifies that all runs of A from (q, |w(i)| □ ) visit F only finitely many times. To do this, for all transitions δ of the form q op − → r in A, we create a sub-A2A T δ sub using copies of sub-A2As. For each such transition, one of two cases should hold: either the transition cannot be simulated (because of a zero test or a decrement from zero), or the transition can indeed be simulated. For the former, we add a violation branch to check that it is indeed the case; for the latter, a validation branch checks the transition can be simulated and a simulation branch reaches the next vertex with the updated counter value. Now if the root vertex is of the form (q ′ , i) then the simulation branch could reach a vertex labelled with r ′ or with r ′′ -with the idea being that T can choose to move to the safety copy or to stay in the "normal" copy of A. If the root vertex is of the form (q ′′ , i), the simulation branch can only reach the vertex labelled with r ′′ with the updated counter value. We obtain the global A2A T by connecting sub-A2As. To ensure that all runs of A are simulated, we have the global transition relation ∆ be a conjunction of that of the sub-A2As which start at the same state q ∈ {p ′ , p ′′ } for some p ∈ Q. For instance, let δ 1 = (q, op 1 , q 1 ) and δ 2 = (q, op 2 , q 2 ) be transitions of A. The constructed sub-A2As T δ1 sub , T δ2 sub will contain transitions (q, □, β 1 ) ∈ ∆ 1 , (q, □, β 2 ) ∈ ∆ 2 respectively. In T , we instead have (q, □, β 1 ∧ β 2 ) ∈ ∆. Finally, the accepting states are chosen as follows: For every q ∈ Q \ F , we set q ′′ as accepting in T . The idea is that if a run in A satisfies the coBüchi condition then, after some point, it stops visiting target states. In T , the simulated run can choose to move to the safety copy at that point and loop inside it forever thus becoming an accepting branch. On the other hand, if a run does not satisfy the condition, its simulated version cannot stay within the safety copy. (Rather, it will reach the non-accepting sink states.) Also, the violation and the validation branches ensure that the operations along the runs have been simulated properly inside T . It follows that T accepts precisely those words whose run-tree contains a simulation branch where states from F have been visited only finitely many times.

An upper bound for reachability synthesis of OCAPT
Following [4], we now sketch a guess-and-check procedure using the fact that Proposition 21 implies a sufficient bound on valuations satisfying the reachability synthesis problem. Recall that, the reachability synthesis problem asks whether all infinite runs reach a target state.

▶ Lemma 22 (Adapted from [4, Lemma 3.5]). If there is a valuation V such that all infinite
It remains to give an algorithm to verify that in the resulting non-parametric OCA (after substituting parameters with their values), all infinite runs from (q 0 , 0) reach F .

▶ Proposition 23.
Checking whether all infinite runs from (q 0 , 0) reach a target state in a non-parametric one-counter automata is coNP-complete.
Before proving the claim above, we first recall a useful lemma from [22].
We define a pumpable cycle as being a zero-test-free cycle such that for all runs ρ = (q 0 , c 0 ) . . . (q n , c n ) lifted from π we have c n ≥ c 0 , i.e., the effect of the cycle is non-negative.
▶ Lemma 24 (From [22]). Let A be a SOCA with an infinite run that does not reach F . Then, there is an infinite run of A which does not reach F such that it induces a path π 0 · π ω 1 , where π 1 either starts from a zero test or it is a simple pumpable cycle.

Sketch of proof of Proposition 23.
We want to check whether all infinite runs starting from (q 0 , 0) reach F . Lemma 24 shows two conditions, one of which must hold if there is an infinite run that does not reach F . Note that both conditions are in fact reachability properties: a path to a cycle that starts from a zero test or to a simple pumpable cycle.
For the first condition, making the reachability-query instances concrete requires configuration a (q, 0) and a state q ′ such that δ(q, q ′ ) is a zero test. Both can be guessed and stored in polynomial time and space. For the other condition, we can assume that π 0 does not have any simple pumpable cycle. It follows that every cycle in π 0 has a zero test or has a negative effect. Let W max be the sum of all the positive updates in A. Note that the counter value cannot exceed W max along any run lifted from π 0 starting from (q 0 , 0). Further, since π 1 is a simple cycle the same holds for 2W max for runs lifted from π 0 π 1 . Hence, we can guess and store in polynomial time and space the two configurations (q, c) and (q, c ′ ) required to make the reachability-query instances concrete.
Since the reachability problem for non-parametric SOCAP is in NP [17], we can guess which condition will hold and guess the polynomial-time verifiable certificates. This implies the problem is in coNP.
For the lower bound, one can easily give a reduction from the complement of the SubsetSum problem, which is NP-complete [12]. The idea is similar to reductions used in the literature to prove NP-hardness for reachability in SOCAP. In the long version of the paper, the reduction is given in full detail. ◀

Conclusion
We have clarified the decidability status of synthesis problems for OCA with parameters and shown that, for several fixed ω-regular properties, they are in 2NEXP. If the parameters only appear on tests, then we further showed that those synthesis problems are in PSPACE. Whether our new upper bounds are tight remains an open problem: neither our coNPhardness result for the reachability synthesis problem nor the PSPACE and NP NP hardness results known [34,22,23] for other synthesis problems (see Table 1) match them. We believe the BIL fragment will find uses beyond the synthesis problems for OCA with parameters: e.g. it might imply decidability of the software-verification problems that motivated the study of ∀∃ R PAD + in [6], or larger classes of quadratic string equations than the ones solvable by reduction to ∃PAD [26]. While we have shown BIL is decidable in 2NEXP, the best known lower bound is the trivial coNP-hardness that follows from encoding the complement of the SubsetSum problem. (Note that BIL does not syntactically include the Π 1 -fragment of PA so it does not inherit hardness from the results in [15].) Additionally, it would be interesting to reduce validity of BIL sentences to a synthesis problem. Following [17], one can easily establish a reduction to this effect for sentences of the form:  φ(x, y).
We observe Φ can always be brought into negation normal form so that negations are applied only to predicates [31]. Hence, it suffices to argue that we can remove negated divisibility predicates while staying within ∀∃ R PAD. The claim follows from the identity below since the newly introduced variables x ′ , x ′′ are both existentially quantified and only appear on the right-hand side of divisibility constraints. For all a, b ∈ Z we have the following.
In other words, if a = 0 and b ̸ = 0 then ¬(a | b). Further, if a ̸ = 0, there are integers q, r ∈ Z such that b = qa + r and 0 < r < |a| if and only if ¬(a | b). ◀

B Undecidability of ∃∀ R PAD
For completeness, we give a proof of Proposition 3 below.
Proof of Proposition 3. We will show the language ∃∀ R PAD of all sentences of the form ¬φ such that φ ∈ ∀∃ R PAD is undecidable. We begin by recalling the definition of the lcm(·, ·, ·) predicate. A common multiple of a, b ∈ Z is an integer m ∈ Z such that a | m and b | m. Their least common multiple m is minimal, that is m | m ′ for all common multiples m ′ . This leads to the following definition of lcm(a, b, m) for all a, b, m ∈ Z.
Observe that the universally-quantified m ′ appears only on the right-hand side of the divisibility constraints. We thus have that ∃∀ R PAD can be assumed to include a leastcommon-multiple predicate. 4 For convenience, we will write lcm(a, b) = m instead of lcm (a, b, m). Now, once we have defined the lcm(·, ·, ·) predicate, we can define the perfect square relation using the identity: x > 0 ∧ x 2 = y ⇐⇒ lcm(x, x + 1) = y + x and multiplication via: Observe that we are now able to state Diophantine equations. Undecidability thus follows from the MRDP theorem [29] which states that satisfiability for such equations (i.e. Hilbert's 10th problem) is undecidable. ◀

C Example where decidability algorithm for ∀∃ R PAD fails
Here we provide some insight where the attempt of Bozga and Iosif [6] fails to show that ∀∃ R PAD + is decidable. First note that every ∀∃ R PAD + sentence φ is of the form where , y), where ψ i are Presburger formulas with free variables x and y. In their proposed algorithm the first step claims that by substituting and renaming the existentially quantified variables, we can reduce φ to the following DNF-BIL form: Intuitively their algorithm proposes that we can remove all the existentially quantified variables occurring outside of the divisibility predicates. Now, we take an example: we start with a ∀∃ R PAD + formula and follow their proposed steps and show that it is not true.
turning inequalities to equalities removing x 1 removing x 2 Now the equation (2y + z 1 − z 2 + z 3 = 0) cannot be reduced anymore as we cannot remove any of the z variables and hence in the end we get existentially quantified variables outside divisibility. ■

D Reduction from all the Synthesis Problems to the coBüchi one
Proof of Lemma 11. Here we give the polynomial time reduction from the reachability, safety and Büchi synthesis problems to the coBüchi synthesis problem. Consider a SOCAP A = (Q, T, δ, X), an initial configuration (q 0 , c 0 ) and the set of target states F . We construct an automaton B = (Q ′ , T ′ , δ ′ , X) which is disjoint union of two copies We denote the states of A 1 as Q 1 and states of A 2 as Q 2 and the set of target states in B as F ′ . We take the initial configuration as (q in 1 , c 0 ) in B where, q in 1 ∈ Q 1 is the copy of q 0 in A 1 . We "force" a move from the first copy to the second one via the target states (only) and there is no way to come back to the first copy once we move to the second one. Formally, for every transition (u, v) ∈ T such that u / ∈ F , we have ( For the transitions (s, t) ∈ T such that s ∈ F , we have (s 1 , t 2 ), (s 2 , t 2 ) ∈ T ′ where s i , t i ∈ Q i . For all states q ∈ Q 1 and q ′ ∈ Q 2 , q ∈ F ′ and q ′ / ∈ F ′ .
Note that, for all valuations, there is an infinite run in A that visits a target state if and only if in B the corresponding run moves to A 2 (and never comes back to the first copy) if and only if it visits target states only finitely many times. Hence, the answer to the safety synthesis problem in A is false if and only if the answer to the Büchi synthesis is false in B. For the reduction from reachability synthesis to Büchi, we can take the exact same construction of B reversing the target and the non-target states in B.
The construction of the automaton B for the reduction from Büchi synthesis to coBüchi is a bit different from the previous one. Here also, we construct B as a disjoint union of two copies of A, but we remove the states in F from the copy A 2 . Also, for every (u, v) ∈ T , we have ( does not exist.) We set F ′ def = Q 2 . Now, for all valuations there is an infinite run ρ in A that visits F only finitely many times if and only if there is an infinite run in B that follows ρ within A 1 until it last visits a state from F and then moves to A 2 so that it visits states from F ′ infinitely often. Hence, the answer to the Büchi synthesis problem in A is negative if and only if it is negative for the coBüchi problem in B. ◀ where Φ is given by: In words: for each enumeration of zero-test transitions we take the conjunction of the intermediate φ reach−nt formulas as well as φ reach−nt formulas from the initial configuration and to the final one. Note that φ reach has the required form as every Ψ subformula is in the required form too. Indeed, the existentially quantified variables in each Ψ only appear in (the right-hand side of) divisibility constraints and every divisibility constraint f (x) | g(x, z) appears conjoined with f (x) > 0. Also, we have only introduced an exponential number of disjunctions (over the enumeration of subsets of zero-test transitions), 2|T | + 4 new variables (since m ≤ |T |) and have not changed the bitsize length of constants after the construction of the Ψ subformulas. Thus, the bitsize of constants and the number of variables in φ reach remain polynomial and |φ reach | is at most exponential in |A|. ◀

F Detailed construction of A2A from OCAPT
Here we give the detailed constructions of all the sub-A2A for each operation of the OCAPT. The general idea of the construction is given in the Figure 3. In this section, while describing A2A constructions from transitions of the form (q i , op, q j ), we will represent the simulation branches as s i ⇝ s j for readability, where s i (similarly, s j ) represents q ′ i or q ′′ i corresponding to the normal or the safety copy as described earlier. Now we move forward to the detailed constructions for each operations.  Verifying the input word The sub-A2A T inp sub depicted in Figure 4a checks whether the given input is a valid parameter word. The states of the form ✓ xi represents that x i has been found along the path. We let S f consist of states ✓ xi , one per x i ∈ X.
▶ Lemma 25. It holds that L(T inp sub ) = W X .
Proof. The A2A T inp sub consists of one deterministic one-way automata, per x ∈ X, whose language clearly corresponds to the set of words where x occurs exactly once. In T inp sub , from the initial state and on the first letter □, a transition with a conjunction formula leads to all sub-automata for each x. The result follows. ◀ Increments For every transition δ = (q i , +1, q j ) we construct T inc sub (see Figure 4b). A run of this sub-A2A starts from s i and some position c on the input word. Recall that c uniquely determines the current counter value in the simulated run of A (although, it should be noted c itself is not the counter value). Then, the run of T inc sub moves to the next occurrence of □ to the right of the current position and then goes to s j accordingly.
Decrements For transitions δ = (q i , −1, q j ) we construct T dec sub (see Figure 5a). In contrast to the increment sub-A2A, it also includes a violation branch in case the decrement would result in a negative counter value: On this branch, T dec sub attempts to read first? to determine if the position of the head corresponds to the first letter of the word.  Proof. Note that any accepting run γ of the sub-A2A must include at least one of the two finite branches from the claim. We further argue that each branch enforces the corresponding constraints if they appear in γ. Since these are mutually exclusive, it follows that γ includes exactly one of the branches.
If γ includes (s i , k) ⇝ (s j , l) then |w(k)| □ − 1 = |w(l)| □ . The latter implies k > l >= 0 since otherwise the position of the head cannot be moved to the left. On the other hand, if γ includes (s i , n) ⇝ (final, n) then γ can only be accepting if n = 0. Hence, γ includes (s i , 0) ⇝ (final, 0). ◀

Zero tests
For every transition δ = (q i , = 0, q j ) we construct T zero sub (see Figure 5b) similarly to how we did for decrements. For the validation branch, it reads first? to confirm the position of the head is at the beginning of the word. For the violation branch, it moves the head to the left to confirm that the head is not at the beginning. ▶ Lemma 27. Let k ∈ N and w ∈ W X with □ the (k + 1)-th letter of w. A run tree γ of T zero sub on w from k is accepting if and only if either (s i , 0) ⇝ (s j , 0) is a part of γ and k = 0, or (s i , k) ⇝ (s ̸ =0 i , k − 1) is a part of γ and |w(k)| □ > 0.
Proof. We proceed as in the proof of Lemma 26.
If γ includes a branch with the state s =0 i then γ is accepting if and only if it reaches s j . It can only reach s j with the first? transition, i.e. when k = 0. Otherwise, it has to include a branch with s ̸ =0 i and reading any letter it reaches true. This is only possible if k > 0. Since the (k + 1)-th letter of w is □, the latter means |w(k)| □ > 0. ◀ Parametric equality tests For every transition δ = (q i , = k, q j ) we construct T eq sub (see Figure 6a). For the validation branch, it moves the head right, skipping over other variable symbols X \ {x}, while looking for k. For the violation branch it skips over other variable symbols while looking for the next □.
(a) T eq sub for parametric equality tests T lb sub for parametric lower-bound tests Proof. Fix a word w ∈ W X with □ as (k + 1)-th letter. Consider any run tree γ of T eq sub on w. After reading the first □, suppose γ has a branch leading to the state s j . It must therefore also have a branch containing present(x). Since, from there, it can only move to the state true if it reads x before reading another □ symbol to the right, we have V (x) = |w(k)| □ .
If γ has a branch containing absent(x i ), then it is accepting if and only if it reaches true after reading another □ before ever reading x. Hence, V (x i ) ̸ = |w(k)| □ . ◀ Parametric lower-bound tests For every transition δ = (q i , ≥ x, q j ) we construct T lb sub (see Figure 6b). For the validation branch, we check for equality to x or we check whether > x. We also create the corresponding violation branches.
▶ Lemma 29. Let k ∈ N and w ∈ W X with □ the (k + 1)-th letter of w. A run tree γ of T lb sub on w from k is accepting if and only if either (s i , k) ⇝ (s j , k) is part of γ and |w(k)| □ ≥ V w (x), or (s i , k) ⇝ (f ront(x), k + 1) is a part of γ and |w(k)| □ < V w (x).
Proof of Lemma 29. Fix a word w ∈ W X with □ as (k + 1)-th letter and consider any run tree γ of T lb sub on w. After reading the first □, let us suppose it adds a branch checking = x in T eq sub . Then, γ is accepting if and only if it additionally contains a branch to (s j , k) and |w(k)| □ = V w (x). If it has the other sub-tree, i.e. it contains back(x), γ is accepting if and only if it reaches the state true which is possible only if there is a □ to the left of the current position and it reads an x to the left of that. It follows that it is accepting if and only if |w(k)| □ > V w (x) and (s i , k) ⇝ (s j , k) is part of γ.
If γ instead contains the branch with f ront(x i ), it is accepting only if it can read x from search(x) after having read a □ from f ront(x) to the right of the current position of the input. Hence, |w(k)| □ < V w (x i ). ◀ Using the previous lemmas, it is straightforward to prove Proposition 21. The detailed proof of correctness is given below.

Proof of Proposition 21.
Here we present a detailed proof of Proposition 21. We have to show that, L(T ) = {w ∈ W X | all infinite V w -runs of A visit F finitely many times from (q 0 , 0)}. We prove this in two parts: ⊇: Consider a word w = a 0 a 1 a 2 · · · ∈ W X , such that with valuation V w all infinite V w -runs of A visit F only finitely many times starting from (q 0 , 0). We have to show, that w is accepted by T , i.e., there exists an accepting run tree γ of w on T . We will now grow an accepting run tree γ valid . Since w is a valid parameter word, we can add to γ valid a sub-tree with root labelled by (s in , 0) and a branch extending to (q ′ 0 , 0) (see Lemma 25). Consider now a valid infinite run ρ of A that visits F only finitely many times. Hence, ρ can be divided into ρ = ρ f · ρ inf such that ρ f is a finite prefix and ρ inf is the infinite suffix that never visits F . Let π be the path of the form (q 0 , op 1 , q 1 )(q 1 , op 2 , q 2 ) . . . induced by ρ. We extend the division of π into π = π 1 · (q j−1 , op j , q j ) · π 2 such that, π 1 · (q j−1 , op j , q j ) is induced by ρ f and π 2 is induced by ρ inf . The idea is that, the run ρ jumps to a "safety component" from the state q j after which it does not visit F at all as ρ satisfies the coBüchi condition. Now, we further extend γ valid by appending to it, from the (q ′ 0 , 0)-labelled vertex, a subtree γ π1 simulating the prefix π 1 as follows: for every transition of the form (q i , op i+1 , q i+1 ) where op i is an increment or decrement, the corresponding T inc sub and T dec sub simulate the path from q ′ i to q ′ i+1 correctly. Also, as every transition in π is valid in π 1 (i.e. does not result in negative counter values), using the first part of Lemmas 27, 28, and 29, we can take the validation sub-trees of T zero sub , T eq sub , and T lb sub , and append them to our run tree. For every simulation branch, we stay at the normal copy and we move from q ′ i to q ′ i+1 . Now, for the transition (q j−1 , op j , q j ), we do the same for the violation and validation branches but in the simulation branch, we move to the safety copy and move to q ′′ j . Intuitively, this safety copy simulates the safety component of ρ as mentioned above. Now, with this we append another sub-tree γ π2 , which we create exactly in the similar way as γ π1 but the simulation branch stays in the safety copy, i.e., it moves from states of the form q ′′ i to q ′′ i+1 . It is easy to see that, γ π2 simulates the suffix ρ inf correctly. Note that, since π 2 does not visit F at all, the simulation branch never reaches the non-accepting sink states in the safety copy and it infinitely loops within the accepting states in the safety copy, making it accepting.
As ρ was chosen arbitrarily, we have that γ ρ , for all infinite runs ρ, are accepting. To conclude, we need to deal with run trees arising from maximal finite runs-the runs that cannot be continued with any valid operation and hence, finite: We construct a sub-tree γ maxf appending simulation and validation sub-trees for as long as possible. By definition of maximal finite runs, every such run reaches a point where all possible transitions are disabled. There, we append a violation sub-tree which, using the second part of the mentioned lemmas, is accepting. Hence, γ valid is accepting.
⊆: Consider a word w ∈ L(T ). We have to show that with valuation V w , every infinite run of A visits F only finitely often from (q 0 , 0). We will prove the contrapositive of this  Figure 7 Reduction from non-SubsetSum to (universal) reachability for SOCA traversed infinitely many times. Using this fact, the run lifted from π[0, r] · π[r, s] ω is our desired safe run. ◀

Proof of second part of Proposition 23.
Here we give the full reduction from the complement of the SubsetSum problem to the problem of checking if all infinite runs reach a target state in a non-parametric SOCAP. Given a set S = {a 1 , a 2 , . . . a n } ⊆ N and a target sum t ∈ N, the Subset Sum problem asks whether there exists S ′ ⊆ S such that ai∈S ′ a i = t. Given an instance of the Subset Sum problem with S and t, we create a SOCA A with initial configuration (q 0 , 0) and a single target state q f as depicted in Figure 7. Note that, for every 1 ≤ i ≤ n there are two ways of reaching q i from q i−1 : directly, with constant update +0; or via q ′ i with total effect +a i . Hence, for every subset S ′ ⊆ S, there exists a path from q 0 to q n with counter value ai∈S ′ a i . Clearly, if there exists S ′ such that ai∈S ′ a i = t Subset Sum then there exists an infinite run leading to q s -not reaching the target state. On the other hand, if there is no such S ′ then all infinite runs reach q f . Hence, the universal reachability in A is positive if and only if the answer to the SubsetSum problem is negative. ◀