Decidable models of integermanipulating programs with recursive parallelism (technical report)Matthew Hague and Anthony Widjaja LinRoyal Holloway, University of London, UK and YaleNUS College, Singapore 
Abstract: We study safety verification for multithreaded programs with recursive parallelism (i.e. unbounded thread creation and recursion) as well as unbounded integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is stateextended groundtree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since the model is Turingcomplete, we propose a decidable underapproximation. First, using a restriction similar to contextbounding, we underapproximate the global control by a weak global control (i.e. DAGs possibly with selfloops), thereby limiting the number of synchronisations between different threads. Second, we bound the number of reversals between nondecrementing and nonincrementing modes of the counters. Under this restriction, we show that reachability becomes NPcomplete. In fact, it is polytime reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our decidable approximation strictly generalises known decidable models including (i) weaklysynchronised groundtree rewrite systems, and (ii) synchronisation/reversalbounded concurrent pushdown systems systems with counters. Finally, we show that, when equipped with reversalbounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability.
Verification of multithreaded programs is wellknown to be a challenging problem. One approach that has proven effective in addressing the problem is to bound the number of context switches [38, 36]. [Recall that a context switch occurs when the CPU switches from executing one thread to executing a different thread.] When the number of context switches is fixed, one may adopt pushdown systems as a model of a single thread and show that reachability for the concurrent extension of the abstraction (i.e. multipushdown systems) is NPcomplete [38]. This result has paved the way for an efficient use of highly optimised SMT solvers in verifying concurrent programs (e.g. see [24, 1, 19]). Note that without bounding the number of context switches the model is undecidable [37].
In the past decade the work of Qadeer and Rehof [38] has spawned a lot of research in underapproximation techniques for verifying multithreaded programs, e.g., see [24, 1, 19, 40, 5, 28, 35, 31, 22, 42, 4, 2, 6, 20, 33, 27, 42, 14] among many others. Other than unbounded recursions, some of these results simultaneously address other sources of infinity, e.g., unbounded thread creation [31, 22, 5], unbounded integer variables [24], and unbounded FIFO queues [1, 2].
In this paper we generalise existing underapproximation techniques [23, 31] so as to handle both shared unbounded integer variables and recursive parallelism (unbounded thread creation and unbounded recursions). The paper also provides a cleaner proof of the result in [24]: an NP upper bound for synchronisation/reversalbounded reachability analysis of concurrent pushdown systems with counters. We describe the details below.
We adopt stateextended groundtree rewrite systems (sGTRS) [31] as a model for multithreaded programs with recursive parallelism (e.g. programming constructs including fork/join, parbegin/parend, and Parallel.For). Groundtree rewrite systems (GTRS) are known (see [21]) to strictly subsume other wellknown sequential and concurrent models like pushdown systems [11], PAprocesses [18], and PADprocesses [34], which are known to be suitable for analysing concurrent programs. [One may think of GTRS as an extension of PA and PAD processes with return values to parent threads [21].] We then equip sGTRS with unbounded integer counters that can be incremented, decremented, and compared against an integer constant.
Since our model is Turingpowerful, we provide an underapproximation of the model for which safety verification becomes decidable. First, we underapproximate the global control by a weak global control [26, 31] (i.e. DAGs possibly with selfloops), thereby limiting the number of synchronisations between different threads. To this end, we may simply unfold the underlying controlstate graph of the sGTRS (see Section 3) in the standard way, while preserving selfloops. This type of underapproximation is similar to loop acceleration in the symbolic acceleration framework of [8]. Second, we bound the number of reversals between nondecrementing and nonincrementing modes of the counters [25]. Under these two restrictions, reachability is shown to be NPcomplete; in fact, it is polytime reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our result strictly generalises the decidability (in fact, NPcompleteness) of reachability for (i) weaklysynchronised groundtree rewrite systems [31, 41], and (ii) synchronisation/reversalbounded concurrent pushdown systems with counters [24].
Finally, we show one negative result that delineates the boundary of decidability. If we relax the weak control underapproximation by the notion of senescence (with age restrictions associated with nodes in the trees) [22], then the resulting model becomes undecidable.
Recursivelyparallel program analysis was analysed in detail by Bouajjani and Emmi [10]. However, in contrast to our systems, their model does not allow processes to communicate during execution. Instead, processes hold handles to other processes which allow them to wait on the completion of others, and obtain the return value. They show that when handles can be passed to child processes (during creation) then the state reachability problem is undecidable. When handles may only be returned from a child to its parent, state reachability is decidable, with the complexity depending on which of a number of restrictions are imposed.
The work of Bouajjani and Emmi is closely related to branching vector addition systems [43] which can model a stack of counter values which can be incremented and decremented (if they remain nonnegative), but not tested. While it is currently unknown whether reachability of a configuration is decidable, controlstate reachability and boundedness are both 2ExpTimecomplete [17].
Another variant of vector addition systems with recursion are pushdown vector addition systems, where a single (sequential) stack and several global counters are permitted. As before, these counters can be incremented and decremented, but not compared with a value. Reachability of a configuration, and controlstate reachability in these models remain open problems, but termination (all paths are finite) and boundedness are known to be decidable [30]. For reachability of a configuration, an underapproximation algorithm is proposed by Atig and Ganty where the stack behaviour is approximated by a finite index contextfree language [7].
Lang and Löding study boundedness problems over sequential pushdown systems [29]. In this model, the pushdown system is equipped with a counter that can be incremented, reset, or recorded. Their model differs from ours first in the restriction to sequential systems, and second because the counter cannot effect execution or be decremented: it is a recording of resource usage. These kind of cost functions have also been considered over static trees [13, 9], however, to our knowledge, they have not been studied over tree rewrite systems.
We write ℕ to denote the set of natural numbers and ℤ the set of integers.
Trees
A ranked alphabet is a finite set of characters Σ together with a rank function ρ : Σ ↦ ℕ. A tree domain D ⊂ ℕ^{∗} is a nonempty finite subset of ℕ^{∗} that is both prefixclosed and youngersiblingclosed. That is, if η i ∈ D, then we also have η ∈ D and, for all 1 ≤ j ≤ i, η j ∈ D (respectively). A tree over a ranked alphabet Σ is a pair t = (D, λ) where D is a tree domain and λ : D ↦ Σ such that for all η ∈ D, if λ(η) = a and ρ(a) = n then η has exactly n children (i.e. η n ∈ D and η (n + 1) ∉ D). Let T_{Σ} denote the set of trees over Σ.
Context Trees
A context tree over the alphabet Σ with a set of context variables x_{1}, …, x_{n} is a tree C = (D, λ) over Σ ⊎ {x_{1}, …, x_{n}} such that for each 1 ≤ i ≤ n we have ρ(x_{i}) = 0 and there exists a unique context node η_{i} such that λ(η_{i}) = x_{i}. By unique, we mean η_{i} ≠ η_{j} for all i ≠ j. We will denote such a tree C[x_{1}, …, x_{n}]. Given trees t_{i} = (D_{i}, λ_{i}) for each 1 ≤ i ≤ n, we denote by C[t_{1}, …, t_{n}] the tree t′ obtained by filling each variable x_{i} with t_{i}. That is, t′ = (D′, λ′) where
D′ = D ⋃ η_{1} · D_{1} ⋃ ⋯ ⋃ η_{n} · D_{n} and λ′  ⎛ ⎝  η  ⎞ ⎠  = 

Tree Automata
A bottomup nondeterministic tree automaton (NTA) over a ranked alphabet Σ is a tuple T = (Q, Δ, F) where Q is a finite set of states, F ⊆ Q is a set of final (accepting) states, and Δ is a finite set of rules of the form (q_{1}, …, q_{n}) –[a]→ q where q_{1}, …, q_{n}, q ∈ Q, a ∈ Σ and ρ(a) = n. A run of T on a tree t = (D, λ) is a mapping π : D ↦ Q such that for all η ∈ D labelled λ(η) = a with ρ(a) = n we have (π(η 1), …, π(η n)) –[a]→ π(η). It is accepting if π(ε) ∈ F. The language defined by a tree automaton T over alphabet Σ is a set L(T) ⊆ T_{Σ} of trees over which there exists an accepting run of T.
Parikh images
Given an alphabet Σ = {γ_{1},…,γ_{n}} and a word w ∈ Σ^{*}, we write P(w) to denote a mapping ρ: Σ → ℕ, where ρ(a) is defined to be the number of occurrences of a in w. Given a language L ⊆ Σ^{*}, we write P(L) to denote the set {P(w)  w ∈ L}. We say that P(L) is the Parikh image of L.
Presburger Arithmetic
Presburger formulas are firstorder formulas over integers with addition. Here, we use existential Presburger formulas ϕ(x,y) := ∃ x ϕ, where (i) x and y are sets of variables, and (ii) ϕ is a boolean combination of expressions ∑_{i=1}^{m} a_{i}z_{i} ∼ b for variables z_{1},…,z_{m} ∈ x ∪ y, constants a_{1},…,a_{m},b∈ ℤ, and ∼ ∈ {≤,≥,<,>,=} with constants represented in binary. A solution to ϕ is a valuation b: y ↦ ℤ to y such that ϕ(x,b) is true. The formula ϕ is satisfiable if it has a solution. Satisfiability of existential Presburger formulas is known to be NPcomplete [39].
In this section, we will define our formal models, which are based on groundtree rewrite systems. Groundtree rewrite systems (GTRSs) [15] permit subtree rewriting where rules are given as a pair of groundtrees. In the sequel, we use the extension proposed by Löding [32] where NTA (instead of ground trees) appear in the rewrite rules. Hence, a single rule may correspond to an infinite number of concrete rules (i.e. containing concrete trees).
Ground Tree Rewrite Systems with State and Reversal Bounded Counters.
To capture synchronisations between different subthreads, we follow [31, 26, 41] and extend GTRS with state (a.k.a. global control). The resulting model is denoted by sGTRS (stateextended GTRS). To capture integer variables, we further extend the model with unbounded integer counters, which can be incremented, decremented, and compared against an integer constant. Since Minsky’s machines can easily be encoded in such a model, we apply a standard underapproximation technique: reversalbounded analysis of the counters [23, 25]. This means that one only analyses executions of the machines whose number of reversals between nondecrementing and nonincrementing modes of the counters is bounded by a given constant r ∈ ℕ (represented in unary). The resulting model will be denoted by rbGTRS. We will now define this model in more detail.
An atomic counter constraint on counter variables C = {c_{1},…,c_{k}} is an expression of the form c_{i} ∼ v, where v ∈ ℤ and ∼ ∈ {<,≤,=,≥,>}. A counter constraint θ on C is a boolean combination of atomic counter constraints on C. Given a valuation ν : C ↦ ℤ to the counter variables, we can determine whether θ[ν] is true or false by replacing a variable c by ν(c) and evaluating the resulting boolean expressions in the obvious way. Let Cons_{C} denote the set of all counter constraints on C. Intuitively, these formulas will act as guards to determine whether certain transitions can be fired. Given two counter valuations ν and µ we define ν + µ as the pointwise addition of the valuations. That is, (ν + µ)(c) = ν(c) + µ(c).
Given a sequence of counter values, a reversal occurs when a counter switches from being incremented to being decremented or viceversa. For example, if the values of a counter c along a run are 1,1,1,2,3,4,4,4,3,2,2,3, then the number of reversals of c is 2 (reversals occur in between the overlined positions). A sequence of valuations is reversalbounded whenever the number of reversals is the sequence is bounded.
We define sGTRS with reversalbounded counters.
In the sequel, we will omit mention of the number r in the tuple G if it is clear from the context.
A configuration of an sGTRS with counters is a tuple α = (p, t, ν) where p is a controlstate, t a tree, and ν a valuation of the counters. We have a transition (p_{1}, t_{1}, ν_{1}) –[γ]→ (p_{2}, t_{2}, ν_{2}) whenever there is a rule (p_{1}, T_{1}, θ) –[γ]→ (p_{2}, T_{2}, µ) ∈ R such that: (i) (dynamics of counters) θ[ν_{1}] is true and ν_{2} = ν_{1} + µ, and (ii) (dynamics of trees) t_{1} = C[t′_{1}] for some context C and tree t′_{1} ∈ L(T_{1}) and t_{2} = C[t′_{2}] for some tree t′_{2} ∈ L(T_{2}). A run π over γ_{1}…γ_{n−1} is a sequence
⎛ ⎝  p_{1}, t_{1}, ν_{1}  ⎞ ⎠  –[γ_{1}]→ ⋯ –[γ_{n−1}]→  ⎛ ⎝  p_{n}, t_{n}, ν_{n}  ⎞ ⎠ 
such that for all 1 ≤ i < n we have (p_{i}, t_{i}, ν_{i}) –[γ_{i}]→ (p_{i+1}, t_{i+1}, ν_{i+1}) is a transition of G and for each c ∈ C the sequence ν_{1}, …, ν_{n} is rreversalbounded for c. We say that γ_{1}…γ_{n−1} is the output string of π. We write (p, t, ν) –[γ_{1}…γ_{n}]→ (p′, t′, ν′) (or simply (p, t, ν) →^{*} (p′, t′, ν′)) whenever there is a run from (p, t, ν) to (p′, t′, ν′) over γ_{1}…γ_{n}. Let ε denote the empty output symbol.
Whenever we wish to discuss sGTRSs without counters, we simply omit the counter components. That is, we have configurations of the form (p, t) and transitions of the form (p_{1}, T_{1}) –[γ]→ (p_{2}, T_{2}). The standard notion of GTRS (i.e. not stateextended) [32] is simply sGTRS without counters with only one state.
We next define the problems of (global) reachability. To this end, we use a tree automaton T (resp. an existential Presburger formula ϕ) to represent the tree (resp. counter) component of a configuration. More precisely, a symbolic configset of an rbGTRS G = (P, Σ, Γ, R, C, r) is a tuple (p, T, ϕ), where p ∈ P, T is an NTA over Σ, and ϕ(x) is an existential Presburger formula with free variables x = {x_{c}}_{c ∈ C} (i.e. one free variable for each counter). Each symbolic configset (c, T, ϕ) represents a set of configurations of G defined as follows: [[(p, T, ϕ) ]] := { (p, t, ν) : t ∈ L(T), ϕ(ν) is true }. Global Reachability
Input: an rbGTRS G and two symbolic configsets (p_{1}, T_{1}, ϕ_{1}) (p_{2}, T_{2}, ϕ_{2})
Problem: Decide whether
(p_{1}, t_{1}, ν_{1}) →^{*}
(p_{2}, t_{2}, ν_{2}), for some
(p_{1}, t_{1}, ν_{1}) ∈
[[(p_{1}, T_{1}, ϕ_{1}) ]] and
(p_{2}, t_{2}, ν_{2}) ∈
[[(p_{2}, T_{2}, ϕ_{2}) ]]
The problem of controlstate reachability can be defined by restricting
(i) the tree automata T_{1} and T_{2} to accept, respectively, a singleton
tree and the set of all trees, and (ii) the solutions to the formulas
ϕ_{1} and ϕ_{2} are, respectively, {ν_{0}} (where
ν_{0} is the valuation assigning 0 to all counters) and the set of all
counter valuations.
Weakly Synchronised Ground Tree Rewrite Systems
The controlstate and global reachability problems for sGTRS are known to be undecidable [12, 21]. The problems become NPcomplete for weaklysynchronised sGTRS [31, 41], where the underlying controlstate graph (where there is an edge between p_{1} and p_{2} whenever there is a transition (p_{1}, T_{1}) –[γ]→ (p_{2}, T_{2})) may only have cycles of length 1 (i.e. selfloops), i.e., a DAG (directed acyclic graph) possibly with selfloops. Underapproximation by a weak control is akin to loop acceleration in the symbolic acceleration framework of [8]. We extend the definition to rbGTRSs. The original definition can be easily obtained by omitting the counter components.
We define the underlying control graph of an rbGTRS G = (P, Σ, Γ, R, C) as a tuple (P, Δ) where Δ = {(p_{1}, p_{2})  (p_{1}, T_{1}, θ) –[γ]→ (p_{1}, T_{2}, µ) ∈ R} .
In this section we will prove the main result of the paper:
To prove this theorem, we fix notation for the input to the problem: an rbGTRS G = (P, Σ, Γ, R, C, r) and two symbolic configsets (p_{1}, T_{1}, ϕ_{1}), (p_{2}, T_{2}, ϕ_{2}) of G. Let C = {c_{i}}_{i=1}^{k}. The gist of the proof is as follows. From G, we construct a new sGTRS G′ (without counters) by encoding the dynamics of the counters in the output symbols of G′. Of course, G′ has no way of comparing the values of counters with constants. [In this sense, G′ only overapproximates the behavior of G.] To deal with this problem, we use the result of [31] to compute an existential Presburger formula ψ capturing the Parikh images of the set of all output strings of G′ from (p_{1}, T_{1}, ϕ_{1}) to (p_{2}, T_{2}, ϕ_{2}). The final formula is ψ ∧ ψ′, where ψ is a constraint asserting that the desired counter comparisons are performed throughout runs of G′. We sketch the details of the construction below.
The first notion that is crucial in our proof is that of mode of a counter [23, 25], which is an abstraction of the values of a counter in a run of an rbGTRS containing three pieces of information: (i) the region of the counter value (i.e. how it compares to constants occurring in counter constraints), (ii) the number of reversals that has been performed by each counter (between 0 and r), and (iii) whether a counter is currently nondecrementing (↑) or nonincrementing (↓). A mode vector is simply a ktuple of modes, one mode for each of the k counters. We now formalise these notions.
Let d_{1} < … < d_{m} be the integer constants appearing in the counter constraints in G. This sequence of constants gives rise to the set REG of regions defined as REG := { A_{0},…,A_{m}, B_{1},…,B_{m}}, where B_{i} := {d_{i}} (where 1 ≤ i ≤ m), A_{i} := { n ∈ ℤ: d_{i} < n < d_{i+1} } (where 1 ≤ i < m), A_{0} := { n ∈ ℤ: n < d_{1} }, and A_{m} := { n ∈ ℤ: n > d_{m} }. A mode is simply a tuple in REG × [0,r] × {↑,↓}. A mode vector is simply a tuple in Modes := REG^{k} × [0,r]^{k} × {↑,↓}^{k}.
We might be tempted to build G′ by first removing the counters from G and then embedding Modes into the controlstates G′. This, however, causes two problems. First, the number of controlstates becomes exponential in k. Second, the resulting system is no longer weakly synchronised even though G originally was weakly synchronised. To circumvent this problem, we adapt a technique from [23]. Every run π of G from (p_{1}, T_{1}, ϕ_{1}) to (p_{2}, T_{2}, ϕ_{2}) can be associated with a sequence σ of mode vectors recording the information (i)–(iii) for each counter. The crucial observation is that there are at most N_{max} := 2mk(r+1) different mode vectors in σ. This is because a counter can only go through at most 2m regions without incurring a reversal. For this reason, we may use the controlstates of G′ to store the number of mode vectors that G has gone through, while the actual mode vector guessed by G′ will be made “visible” in the output strings of G′. That way, we can use an additional existential Presburger formula ψ′ (see below) to enforce that the run of G′ faithfully simulates runs of G. In addition, the shape of the controlstates (DAG with selfloops) of G′ is preserved. [The product graph of two DAGs with selfloops is also a DAG with selfloops.] We detail the construction below.
Define the weaklysynchronised sGTRS G′ = (P′, Σ, Γ′, R′) as follows. Let P′ := P × [0,N_{max}]. The output alphabet Γ′ is defined as Γ × R × [0,N_{max}] × {0,1}, where the boolean flag is used to denote whether the transition taken changes the mode. We define R′ as follows. For each rule τ = (p, T, θ) –[γ]→ (p′, T′, µ) in R, we add the rule ((p,i), T) –[(γ,τ,i,0)]→ ((p′,i), T′) for each i ∈ [0,N_{max}], and ((p,i), T) –[(γ,τ,i,1)]→ ((p′,i+1), T′) for each i ∈ [0,N_{max}). Since G is weaklysynchronised and the mode counter never decreases, it follows that G′ is weaklysynchronised too. Note also that this construction can be performed in polynomialtime.
As we mentioned, ψ is an existential Presburger formula encoding the Parikh image P(L) of the set L of all output strings of G′ from ((p_{1},0), T_{1}) to (S, T_{2}), where S = {p_{2}} × [0,N_{max}]. More precisely, the set z of free variables of ψ include z_{a} for each a ∈ Γ′. Furthermore, for each valuation µ ∈ z ↦ ℤ, it is the case that ψ(µ) is true iff µ ∈ P(L). Such a formula is known to be polynomialtime computable since G′ is a weaklysynchronised sGTRS [31].
Recall that ψ′ should assert that the desired counter comparisons are performed throughout runs of G′. To this end, the formula ψ′ will have extra variables for guessing the existence of a sequence of N_{max} distinct mode vectors through runs of G′. More precisely, the formula ψ′ is the conjunction
ϕ_{1}(x) ∧ ϕ_{2}(y) ∧ Dom(m_{0},…,m_{Nmax}) ∧ Init(m_{0}) ∧ 
GoodSeq(m_{0},…,m_{Nmax}) ∧ Respect(z,m_{0},…,m_{Nmax}) ∧ EndVal(x,y,z). 
The set x consists of variables x_{i} (1 ≤ i ≤ k) which contain the initial value of the ith counter. Similarly, the set y consists of variables y_{i} (1 ≤ i ≤ k) which contain the final value of the ith counter. Each m_{i} denotes a set of variables for the ith mode vector defined as follows:
We detail each subformula below.
The subformula Dom asserts that each variable in m_{i} (for each i) has the right domain (i.e. range of integer values). More precisely, for each j ∈ [1,k], we add the conjuncts: (i) 0 ≤ reg_{j}^{i} ≤ 2m, (ii) 0 ≤ rev_{j}^{i} ≤ r, and (iii) 0 ≤ arr_{j}^{i} ≤ 1. For the first constraint, we use an even number of the form 2i to represent the region A_{i}, and an odd number 2i−1 to represent the region B_{i}. The last constraint simply encodes nondecrementing (↑) as 1, and nonincrementing (↓) as 0.
The subformula Init asserts that m_{0} is an initial mode vector. More precisely, for each j ∈ [1,k], we add the conjuncts rev_{j}^{0} = 0.
The subformula GoodSeq asserts that m_{0},…,m_{Nmax} forms a valid sequence of mode vectors. More precisely, for each i ∈ [0,N_{max}) and each j ∈ [1,k], we add the conjuncts: (i) arr_{j}^{i} ≠ arr_{j}^{i+1} ⇒ rev_{j}^{i+1} = rev_{j}^{i}+1, (ii) arr_{j}^{i} = arr_{j}^{i+1} ⇒ rev_{j}^{i+1} = rev_{j}^{i}, (iii) reg_{j}^{i} < reg_{j}^{i+1} ⇒ arr_{j}^{i+1} = 1, and (iv) reg_{j}^{i} > reg_{j}^{i+1} ⇒ arr_{j}^{i+1} = 0. For example, the first constraint asserts that a change in the direction (nonincrementing or nondecrementing) of the counter incurs one reversal. The other constraints are similar.
The subformula Respect asserts that the Parikh image z of the run of G′ respects the sequence m_{0},…,m_{Nmax} of mode vectors. In effect, this subformula ensures that G′ faithfully simulates G. Firstly, we need to assert that the jth counter values at the start and at the end of the ith mode of G′ (which are encoded in z) are in the right regions reg_{j}^{i}. To state this more precisely, for each rule τ = (p, T, θ) –[γ]→ (p′, T′, µ) in R, we let µ_{j}(τ) denote the value µ(c_{j}). For each i ∈ [0,N_{max}] and j ∈ [1,k], we denote by the notation StartCounter_{j}^{i} the term x_{j} + ∑_{s=0}^{i−1}∑_{(γ,τ,s,l)} µ_{j}(τ) × z_{(γ,τ,s,l)}, where γ, τ, and l, range over, respectively, Γ, R, and {0,1}. Similarly, we denote by EndCounter_{j}^{i} the term StartCounter_{j}^{i} + ∑_{(γ,τ,i,0)} µ_{j}(τ) × z_{(γ,τ,i,0)}. We add the conjuncts: (i) reg_{j}^{i} = 2h ⇒ EndCounter_{j}^{i} ∈ A_{h}, for each h ∈ [0,m], and (ii) reg_{j}^{i} = 2h+1 ⇒ EndCounter_{j}^{i} ∈ B_{h}, for each h ∈ [0,m). [Note that formulas of the form g ∈ A, for a Presburger term g and a set S ∈ {A_{0},…,A_{m},B_{1},…,B_{m}}, can be easily replaced by quantifierfree Presburger formulas, e.g., g ∈ A_{0} stands for g < d_{1}.] To ensure that the initial condition is correct, for each j ∈ [1,k], we add the following conjuncts: (1) StartCounter_{j}^{0} ∈ A_{h} ⇒ reg_{j}^{0} = 2h, and (2) StartCounter_{j}^{0} ∈ B_{h} ⇒ reg_{j}^{0} = 2h+1. Secondly, we need to state that the transitions executed in each mode are valid (i.e. satisfy the counter constraints). More precisely, for each γ ∈ Γ, τ ∈ R, i ∈ [0,N_{max}], and l ∈ {0,1}, if θ is the counter constraint in τ, we add the conjunct z_{(γ,τ,i,l)} > 0 ⇒ θ(StartCounter_{1}^{i},…,StartCounter_{k}^{i}). Next we assert that, when the jth counter is nonincrementing (resp. nondecrementing), only nonnegative (resp. nonpositive) counter increments are permitted. More precisely, for each i ∈ [0,N_{max}], j ∈ [1,k], l ∈ {0,1}, and τ ∈ R, if µ_{j}(τ) > 0, then add the conjunct arr_{j}^{i} = 0 ⇒ z_{(γ,τ,i,l)} = 0; if µ_{j}(τ) < 0, then add the conjunct arr_{j}^{i} = 1 ⇒ z_{(γ,τ,i,l)} = 0.
Finally, the subformula EndVal simply asserts that, starting from the initial counter value x and following the transitions z, the end counter values are y. To this end, we can simply add the conjunct y_{j} = EndCounter_{j}^{Nmax} for each j ∈ [1,k].
This concludes the formula construction. It is immediate that G′ faithfully simulates G iff ψ ∧ ψ′ is true. In addition, the formula construction runs in polynomialtime. Since satisfiability over existential Presburger formulas is NPcomplete [39], the NP upper bound for Theorem 1 follows. NPhardness already holds for the restricted model where the tree component is a stack [23].
A natural question arising from the result on weakly synchronised rbGTRS is whether the “weakly synchronised” restriction can be relaxed while maintaining decidability. It is known that allowing arbitrary underlying controlstate graphs leads to undecidability of reachability even without reversal bounded counters. In this section we explore the notion of senescence [22], which is more general than the weakly synchronised restriction, but still permits a decidable reachability problem (without counters). After giving the formal definition of senescent GTRS, we show the following result.
Senescence allows the underlying controlstate graph to have arbitrary cycles (instead of only selfloops). For sGTRS, controlstate reachability is decidable under an “age restriction” that is imposed on the nodes that can be rewritten. That is, when the controlstate changes, the nodes in the tree age by one timestep. Once a node reaches an a priori fixed age r, it becomes fixed (i.e. cannot be rewritten by further transitions in the run).
Before the formal definition, two example transitions of a senescent rbGTRS are shown in Figure 3. A configuration is written as its controlstate and counter values ((p, ν) or (p′, ν′)) with the tree appearing below. In the tree, the label of each node appears in the centre of the node. The ages of each node is depicted as a subscript on the right. Dotted lines are used to indicate the part of the tree rewritten by a rule. In Figure 1 the transition changes the controlstate, causing the age of the nodes that are not rewritten to increase by 1. The rewritten nodes are given the age 0 as they are new, fresh, nodes. The situation when the controlstate does not change is shown in Figure 2. In this case, the nodes that are not rewritten maintain the same age. The senescence restriction disallows runs where nodes older than a fixed age are rewritten.
More formally, given a run
⎛ ⎝  p_{1}, t_{1}, ν_{1}  ⎞ ⎠  –[γ_{1}]→ ⋯ –[γ_{n−1}]→  ⎛ ⎝  p_{n}, t_{n}, ν_{n}  ⎞ ⎠ 
of an rbGTRS, let C_{1}, …, C_{n−1} be the sequence of tree contexts used in the transitions from which the run was constructed. That is, for all 1 ≤ i < n, we have t_{i} = C_{i}[t_{i}^{out}] and t_{i+1} = C_{i}[t_{i+1}^{in}] where (p_{i}, T_{i}, θ_{i}) –[γ_{i}]→ (p_{i+1}, T′_{i}, µ_{i}) was the rewrite rule used in the transition and t_{i}^{out} ∈ L(T_{i}), t_{i+1}^{in} ∈ L(T′_{i}) were the trees that were used in the tree update.
For a given position (p_{i}, t_{i}, ν_{i}) in the run and a given node η in the domain of t_{i}, the birthdate of the node is the largest 1 ≤ j ≤ i such that η is in the domain of C_{j}[t_{j}^{in}] and η is in the domain of C_{j}[x] only if its label is x. The age of a node is the cardinality of the set {i′  j ≤ i′ < i ∧ p_{i′} ≠ p_{i′+1}}. That is, the age is the number of times the controlstate changed between the jth and the ith configurations in the run.
A lifespanrestricted run with a lifespan of r is a run such that each transition (p_{i}, C_{i}[t_{i}^{out}], ν_{i}) –[γ_{i}]→ (p_{i+1}, C_{i}[t_{i+1}^{in}], ν_{i+1}) has the property that all nodes η in t_{i}^{out} have an age of at most r. That is, more precisely, that all nodes η in the domain of C_{i}[t_{i}^{out}] but only in the domain of C_{i}[x] if the label is x have an age of at most r.
Note that the senescence restriction is weaker than the weaklysynchronised restriction in that the number of times the finite control could change state is unbounded. In fact, a node could be affected by an unbounded number of controlstate changes so long as it is always rewritten without becoming fixed (i.e. reaches age r).
We show controlstate reachability for senescent rbGTRSs is undecidable in the appendix, and give the intuition here. In the following, we refer to nodes whose age is within the age bound as live. We refer to nodes that are not live as fixed. Note, each time a node is rewritten, its age is reset to zero. Thus, we can keep leaves of the tree live by allowing them to rewrite to themselves. That is, for all symbols a we wish to keep live and all controlstates p, we have a transition (p, a, θ) –[γ]→ (p, a, µ) where θ is a formula that is always satisfied, and µ assigns 0 to all counters (i.e. the rule does not depend on, nor change the counter values). In addition, by omitting the above rules for certain controlstates, we can prevent a node from keeping itself fresh in certain situations.
We follow the proof that reachability for reset Petri nets is undecidable [3]. We simulate a twocounter machine. Testing whether such a machine can reach a given controlstate while having counters with value zero is undecidable.
Let the two counters be c_{1} and c_{2}. In the tree, we track the value of a counter c ∈ {c_{1}, c_{2}} by the number of live leaves labelled with the counter name c. E.g. the tree •(c_{1}, •(c_{2}, ∗)) represents the situation where both counters have value 1, assuming these leaves are live. We will always use internal nodes labelled •. The node ∗ is for adding new leaves when required. To increment a counter we add a new leaf labelled c. To decrement a counter, we rewrite a leaf labelled c to a null label. Thus, we can easily increment and decrement counters. Zero tests, however, are more subtle. To help with this, we track, using reversalbounded counters, the number of increments made to each counter, and in separate reversalbounded counters, the number of decrements. That is, we have reversal bounded counters {c_{1}^{+},c_{1}^{−},c_{2}^{+},c_{2}^{−}}. When we simulate an increment of c_{1} we add a leaf and increment c_{1}^{+}. When we simulate a decrement of c_{2} we rewrite a leaf to a null character and increment c_{1}^{−}. Similarly for c_{2}. We simulate zero tests as follows.
To simulate a zero test on a counter c we perform the following checks. First, we “reset” the counter to zero by forcing enough controlstate changes to fix the nodes corresponding to the counter. That is, we move to a controlstate p where all leaf labels may rewrite to themselves, except those labelled c. After the move to p all leaves will have age 1. Leaves not labelled c can refresh their age to 0 by rewriting themselves. Leaves labelled c will stay aged 1. Then, we move to the target controlstate of the transition we are simulating. Thus, after these moves, all leaves labelled c will reach age 2, while all other nodes will only reach age 1. Thus, if our lifespan is 2, nodes labelled c will no longer be live. That is, the simulated value of c in the tree has been forced to 0.
After this reset operation, the counter value is definitely zero. However, we did not enforce that the counter value was zero before the transition. Recall, we track the number of increments and decrements to c in the reversal bounded counters. If the counter was not zero before the test, there will be a discrepancy with the reversal bounded counters: more increments will be recorded than decrements. E.g. for counter c_{1} we will have c_{1}^{+} > c_{1}^{−}. This cannot be corrected by the simulation. Thus, at the end of the run, we check whether the number of increments is equal to the number of decrements. If not, we know the run made a spurious transition. That is, it performed a zero test transition when the counter was not zero. If no spurious transitions were made, we know the twocounter machine has a corresponding run. This completes the gist of the simulation of a twocounter machine.
We proposed sGTRS with counters as a model of recursively parallel programs with unbounded recursion, thread creation, and integer variables. To obtain decidability, we gave an underapproximation in the form of weak sGTRS with reversalbounded counters. We showed that the reachability problem for this model is NPcomplete; in fact, polynomialtime reducible to satisfiability of linear integer arithmetic, for which highly optimised SMT solvers are available (e.g. Z3 [16]). Additionally, we explored the possibility of relaxing the weaklysynchronised constraint to that of senescence, and showed that the resulting model has an undecidable controlstate reachability problem.
One possible avenue of future work is to investigate what happens when local integer values are permitted. That is, reversalbounded counters can be stored on the nodes of the tree. We may also study techniques that allow nodes to contain multiple labels, permitting the modelling of multiple local variables without an immediate exponential blow up.
We thank anonymous reviewers for their helpful feedback. This work was supported by the Engineering and Physical Sciences Research Council [EP/K009907/1] and YaleNUS College Startup Grant.
We show that the controlstate reachability problem is undecidable via a reduction from the reachability problem for twocounter machines.
A twocounter machine is a tuple M = (S, Δ) where P is a finite set of controlstates, Δ is a finite set of rules of the form p_{1} –[op, ]→ p_{2} where p_{1}, p_{2} ∈ S, and op ∈ {inc_{1}, inc_{2}, dec_{1}, dec_{2}, zero_{1}, zero_{2}}. A configuration of M is a tuple (p, v_{0}, v_{1}) ∈ S × ℕ × ℕ. We have a transition (p_{1}, v_{0}^{1}, v_{1}^{1}) —→ (p_{2}, v_{0}^{2}, v_{1}^{2}) if we have a rule p_{1} –[op, ]→ p_{2} and
Let ν_{0} be the valuation assigning 0 to all counters. For given twocounter machine M and controlstates s_{0} and s_{f} we define a senescent rbGTRS G_{M} such that there is a run
⎛ ⎝  s_{0}, T_{0}, ν_{0}  ⎞ ⎠  –[ε]→ ⋯ –[ε]→  ⎛ ⎝  s_{f}, T, ν  ⎞ ⎠ 
for some T and ν iff there is a run
⎛ ⎝  p_{0}, 0, 0  ⎞ ⎠  —→ ⋯ —→  ⎛ ⎝  p_{f}, 0, 0  ⎞ ⎠ 
of M. Since this latter problem is wellknown to be undecidable, we obtain undecidability of controlstate reachability for senescent rbGTRS.
In the following definition we use the following 1reversalbounded counters: c_{0}^{+}, c_{1}^{+}, c_{0}^{−} and c_{1}^{−}. We use R_{fresh} to keep leaf nodes within the lifespan, R_{inc}, R_{dec}, and R_{zero} to simulate the counter operations, and R_{fin} to check c_{i}^{+} = c_{i}^{−} for both i at the end of the run. Furthermore, let

Recall ν_{0} maps all counters to zero.
Given a node η and trees t_{1}, …, t_{n}, we will often write η(t_{1}, …, t_{n}) to denote the tree with root node η and lefttoright child subtrees t_{1}, …, t_{n}. When η is labelled a, we may also write a(t_{1}, …, t_{n}) to denote the same tree. We will often simply write a to denote the tree with a single node labelled a.
For a tree t, let T_{t} be an NTA accepting only t. For example, T_{a(b)} is the automaton accepting only the tree a(b), and T_{a} accepts only the tree containing a single node labelled a. Note, we do not use natural numbers as tree labels, hence T_{1}, T_{2}, … may range over all NTAs.
G_{M}=  ⎛ ⎝  P, Σ, Γ, R, C  ⎞ ⎠ 


⎛ ⎝  p_{0}, 0, 0  ⎞ ⎠  —→ ⋯ —→  ⎛ ⎝  p_{f}, 0, 0  ⎞ ⎠ 
⎛ ⎝  s_{0}, T_{0}, ν_{0}  ⎞ ⎠  –[ε]→ ⋯ –[ε]→  ⎛ ⎝  s_{f}, T, ν  ⎞ ⎠ 
Proof. Let s_{1} = s_{0} and s_{n} = s_{f} and suppose we have a run
⎛ ⎝  s_{1}, 0, 0  ⎞ ⎠  —→ ⋯ —→  ⎛ ⎝  s_{n}, 0, 0  ⎞ ⎠  . 
We build the required run of G_{M} by induction such that for configuration (s_{j}, v_{0}^{j}, v_{1}^{j}) along the run of M, we have a run to a configuration (s_{j}, T_{j}, ν_{j}) of G_{M} such that
In the base case the result holds trivially for the configuration (s_{1}, ∗, ν_{0}). Now take a transition (s_{j}, op, s_{j+1}) from the run of M. By induction we have a run to (s_{j}, T_{j}, ν_{j}) as above. We show how to extend this run to (s_{j+1}, T_{j+1}, ν_{j+1}). There are several cases depending on op. In each case we show how to reach a tree satisfying the induction hypothesis, except the age of the leaf nodes. After the case analysis we show how to satisfy the age requirement also.
Finally, to obtain the age restriction on all leaf nodes, we apply (s_{j+1}, T_{η}, ⊤) –[ε]→ (s_{j+1}, T_{η}, ν_{0}) to each leaf labelled by some η ∈ {∗, 0, 1}.
Thus, by induction, we can reach a configuration (s_{f}, T, ν) such that, for each i we have ν(c_{i}^{+}) = ν(c_{i}^{−}). Thus, we can apply a sequence of rules from R_{fin} to reach (f, T, ν). In particular, we apply (s_{f}, T_{∗}, ⊤) –[ε]→ (p_{=}, T_{∗}, ν_{0}) and then simultaneously reduce each reversalbounded counter to zero using (p_{=}, T_{∗}, ⊤) –[ε]→ (p_{=}, T_{∗}, µ_{i}^{=}) repeatedly for each i, and then finally apply
⎛ ⎝  p_{=}, T_{∗}, c_{0}^{+} = 0 ∧ c_{0}^{−} = 0 ∧ c_{1}^{+} = 0 ∧ c_{1}^{−} = 0  ⎞ ⎠  –[ε]→  ⎛ ⎝  f, T_{∗}, ν_{0}  ⎞ ⎠ 
to complete this direction of the proof.
We prove the opposite direction via two inductions. First, take some run of G_{M}, which necessarily has the form
⎛ ⎝  p_{1}, T_{1}, ν_{1}  ⎞ ⎠  –[ε]→ ⋯ –[ε]→  ⎛ ⎝  p_{n}, T_{n}, ν_{n}  ⎞ ⎠  –[ε]→  ⎛ ⎝  p_{=}, T_{n}, ν_{n}  ⎞ ⎠  –[ε]→ ⋯ –[ε]→  ⎛ ⎝  p_{=}, 0, 0  ⎞ ⎠  –[ε]→  ⎛ ⎝  f, 0, 0  ⎞ ⎠ 
where the last sequence of transitions (from p_{n}) are all from R_{fin}, p_{1} = s_{0}, T_{1} = ∗, ν_{1} = ν_{0}, and p_{n} = s_{f}. Let #_{i}(T) be the number of leaves labelled i in T. We first prove by induction over the run that for all 1 ≤ j ≤ n and i ∈ {0,1} we have #_{i}(T_{j}) = ν_{j}(c_{i}^{+}) − ν_{j}(c_{i}^{−}). This is a straightforward induction that can be seen by observing
Given #_{i}(T_{j}) = ν_{j}(c_{i}^{+}) − ν_{j}(c_{i}^{−}) for all j and i, we construct, also by induction, a sequence
⎛ ⎝  s_{1}, v_{0}^{1}, v_{1}^{1}  ⎞ ⎠  , …,  ⎛ ⎝  s_{n}, v_{0}^{n}, v_{1}^{n}  ⎞ ⎠ 
of M such that for all j and i we have #_{i}(T_{j}) = v_{0}^{j} and p_{j} ∈ {s_{j}, (s_{j}, 0), (s_{j}, 1)} and, either
In the base case we set (s_{1}, v_{0}^{1}, v_{0}^{1}) = (s_{0}, 0, 0). Next, take a transition
⎛ ⎝  p_{j}, T_{j}, ν_{j}  ⎞ ⎠  –[ε]→  ⎛ ⎝  p_{j+1}, T_{j+1}, ν_{j+1}  ⎞ ⎠ 
of G_{M}. There are several cases depending on which rule τ was applied.
Thus, we have a sequence (s_{1}, v_{0}^{1}, v_{1}^{1}), …, (s_{n}, v_{0}^{n}, v_{1}^{n}) from which we can immediately extract a run of M from (s_{1}, v_{0}^{1}, v_{1}^{1}) = (s_{0}, 0, 0) to (s_{n}, v_{0}^{n}, v_{1}^{n}) = (s_{f}, v_{0}^{n}, v_{1}^{n}). That v_{0}^{n} = v_{1}^{n} = 0 follows since the final transitions from s_{n} have the effect of asserting ν_{n}(c_{i}^{+}) − ν_{n}(c_{i}^{−}) = 0 from which we conclude #_{i}(T_{n}) = 0 and since v_{i}^{n} = #_{i}(T_{n}) we complete the proof as required.
Thus, via Property 1 (Simulation of M) we can reduce the reachability problem for twocounter machines to the controlstate reachability problem for senescent rbGTRS. Thus, we show the controlstate reachability problem is undecidable and complete the proof of Theorem 2.
This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.