Decidable models of integer-manipulating
programs with recursive parallelism
Matthew Hague and Anthony Widjaja Lin
1

Royal Holloway, University of London, UK
2
Yale-NUS College, Singapore

Abstract. We study safety verification for multithreaded programs withrecursive 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 ground-tree rewrite systems equipped with shared unbounded
integer counters that can be incremented, decremented, and comparedagainst an integer constant. Since the model is Turing-complete, we propose a decidable underapproximation. First, using a restriction similar
to context-bounding, we underapproximate the global control by a weak
global control (i.e. DAGs possibly with self-loops), thereby limiting thenumber of synchronisations between diﬀerent threads. Second, we boundthe number of reversals between non-decrementing and non-incrementing
modes of the counters. Under this restriction, we show that reachability
becomes NP-complete. In fact, it is poly-time 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) weakly-synchronised ground-tree
rewrite systems, and (ii) synchronisation/reversal-bounded concurrent
pushdown systems systems with counters. Finally, we show that, whenequipped with reversal-bounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability.

1

Introduction

Verification of multithreaded programs is well-known to be a challenging problem. One approach that has proven eﬀective in addressing the problem is tobound the number of context switches [36, 38]. [Recall that a context switch occurs when the CPU switches from executing one thread to executing a diﬀerent
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. multi-pushdown systems) is NP-complete[38]. This result has paved the way for an eﬃcient use of highly optimised SMT
solvers in verifying concurrent programs (e.g. see [1, 18, 24]). Note that withoutbounding 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 [1, 2, 4, 5, 7, 14, 18, 20, 22, 24, 27, 28, 31, 33, 35, 40, 42] among many others.

2Matthew Hague and Anthony Widjaja Lin

Other than unbounded recursions, some of these results simultaneously address
other sources of infinity, e.g., unbounded thread creation [5, 22, 31], unbounded
integer variables [24], and unbounded FIFO queues [1, 2].
Contributions. 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 forsynchronisation/reversal-bounded reachability analysis of concurrent pushdown
systems with counters. We describe the details below.
We adopt state-extended ground-tree rewrite systems (sGTRS) [31] as amodel for multithreaded programs with recursive parallelism (e.g. programming constructs including fork/join, parbegin/parend, and Parallel.For).
Ground-tree rewrite systems (GTRS) are known (see [21]) to strictly subsume
other well-known sequential and concurrent models like pushdown systems [11],PA-processes [19], and PAD-processes [34], which are known to be suitable foranalysing concurrent programs. [One may think of GTRS as an extension of PA
and PAD processes with return values to parent threads [21].] We then equipsGTRS with unbounded integer counters that can be incremented, decremented,
and compared against an integer constant.
Since our model is Turing-powerful, we provide an underapproximation of themodel for which safety verification becomes decidable. First, we underapproximate the global control by a weak global control [26, 31] (i.e. DAGs possiblywith self-loops), thereby limiting the number of synchronisations between diﬀerent threads. To this end, we may simply unfold the underlying control-state graphof the sGTRS (see Section 3) in the standard way, while preserving self-loops.
This type of underapproximation is similar to loop acceleration in the symbolic
acceleration framework of [8]. Second, we bound the number of reversals between
non-decrementing and non-incrementing modes of the counters [25]. Under these
two restrictions, reachability is shown to be NP-complete; in fact, it is poly-time
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, NP-completeness) of reachability for (i) weakly-synchronised
ground-tree rewrite systems [31, 41], and (ii) synchronisation/reversal-bounded
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 ofsenescence (with age restrictions associated with nodes in the trees) [22], thenthe resulting model becomes undecidable.
Related Work. Recursively-parallel 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 completionof others, and obtain the return value. They show that when handles can bepassed to child processes (during creation) then the state reachability problem
is undecidable. When handles may only be returned from a child to its parent,Integer-manipulating programs with recursive parallelism

3state reachability is decidable, with the complexity depending on which of anumber 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 non-negative), but not tested. While
it is currently unknown whether reachability of a configuration is decidable,
control-state reachability and boundedness are both 2ExpTime-complete [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 control-statereachability in these models remain open problems, but termination (all paths
are finite) and boundedness are known to be decidable [30]. For reachabilityof a configuration, an under-approximation algorithm is proposed by Atig and
Ganty where the stack behaviour is approximated by a finite index context-freelanguage [6].
Lang and Löding study boundedness problems over sequential pushdown
systems [29]. In this model, the pushdown system is equipped with a counterthat can be incremented, reset, or recorded. Their model diﬀers from ours firstin the restriction to sequential systems, and second because the counter cannot
eﬀect execution or be decremented: it is a recording of resource usage. These kindof cost functions have also been considered over static trees [9, 13], however, to
our knowledge, they have not been studied over tree rewrite systems.

2

Preliminaries

We write N to denote the set of natural numbers and Z the set of integers.
Trees A ranked alphabet is a finite set of characters Σ together with a rankfunction ρ : Σ 7→ N. A tree domain D ⊂ N∗ is a non-empty finite subset of N∗
that is both prefix-closed and younger-sibling-closed. That is, if ηi ∈ D, then we
also have η ∈ D and, for all 1 ≤ j ≤ i, ηj ∈ D (respectively). A tree over aranked alphabet Σ is a pair t = (D, λ) where D is a tree domain and λ : D 7→ Σsuch that for all η ∈ D, if λ(η) = a and ρ(a) = n then η has exactly n children/ D). Let TΣ denote the set of trees over Σ.
(i.e. ηn ∈ D and η(n + 1) ∈Context Trees A context tree over the alphabet Σ with a set of context
variables x1 , . . . , xn is a tree C = (D, λ) over Σ ⊎ {x1 , . . . , xn } such that for each1 ≤ i ≤ n we have ρ(xi ) = 0 and there exists a unique context node ηi suchthat λ(ηi ) = xi . By unique, we mean ηi ̸= ηj for all i ̸= j. We will denote sucha tree C[x1 , . . . , xn ]. Given trees ti = (Di , λi ) for each 1 ≤ i ≤ n, we denoteby C[t1 , . . . , tn ] the tree t′ obtained by filling each variable xi with ti . That is,
t′ = (D′ , λ′ ) where{′

D = D ∪ η1 · D1 ∪ · · · ∪ ηn · Dn′

and λ (η) =λ(η)λi (η ′ )if η ∈ D ∧ ∀i.η ̸= ηiif η = ηi η ′ .

4Matthew Hague and Anthony Widjaja Lin

Tree Automata A bottom-up non-deterministic tree automaton (NTA) overa 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 theaform (q1 , . . . , qn ) −→ q where q1 , . . . , qn , q ∈ Q, a ∈ Σ and ρ(a) = n. A run of T
on a tree t = (D, λ) is a mapping π : D 7→ Q such that for all η ∈ D labelledaλ(η) = a with ρ(a) = n we have (π(η1), . . . , π(ηn)) −→ π(η). 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 ∈ Σ ∗ , wewrite P(w) to denote a mapping ρ : Σ → N, where ρ(a) is defined to be thenumber 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 first-order formulas overintegers with addition. Here, we use existential Presburger formulas φ(x, y) :=∃xφ, where (i) x andy are sets of variables, and (ii) φ is a boolean combina∑mtion of expressions
i=1 ai zi ∼ b for variables z1 , . . . , zm ∈ x ∪ y, constants
a1 , . . . , am , b ∈ Z, and ∼ ∈ {≤, ≥, <, >, =} with constants represented in binary.
A solution to φ is a valuation b : y 7→ Z 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 NP-complete [39].

3Formal Models

In this section, we will define our formal models, which are based on groundtree rewrite systems. Ground-tree rewrite systems (GTRSs) [15] permit subtree
rewriting where rules are given as a pair of ground-trees. In the sequel, we use theextension proposed by Löding [32] where NTA (instead of ground trees) appear
in the rewrite rules. Hence, a single rule may correspond to an infinite numberof concrete rules (i.e. containing concrete trees).
Ground Tree Rewrite Systems with State and Reversal-BoundedCounters. To capture synchronisations between diﬀerent subthreads, we follow [26, 31, 41] and extend GTRS with state (a.k.a. global control). The resulting
model is denoted by sGTRS (state-extended GTRS). To capture integer variables, we further extend the model with unbounded integer counters, which canbe 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: reversal-bounded 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 ∈ N (represented in unary). The
resulting model will be denoted by rbGTRS. We will now define this model inmore detail.
An atomic counter constraint on counter variables C = {c1 , . . . , ck } is anexpression of the form ci ∼ v, where v ∈ Z and ∼∈ {<, ≤, =, ≥, >}. A counter

Integer-manipulating programs with recursive parallelism

5

constraint θ on C is a boolean combination of atomic counter constraints on
C. Given a valuation ν : C 7→ Z 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 ConsC denote the setof all counter constraints on C. Intuitively, these formulas will act as guards todetermine 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 switchesfrom being incremented to being decremented or vice-versa. For example, if thevalues of a counter c along a run are 1, 1, 1, 2, 3, 4, 4, 4, 3, 2, 2, 3, then the numberof reversals of c is 2 (reversals occur in between the overlined positions). A
sequence of valuations is reversal-bounded whenever the number of reversals is
the sequence is bounded.
Definition 1 (r-Reversal-Bounded). For a counter c from a set of counters
C, a sequence ν1 , . . . , νn of counter valuations over C is r-reversal-bounded forc whenever we can partition ν1 , . . . , νn into (r + 1) sequences A1 , . . . , Ar+1 (withν0 , . . . , νn = A1 , . . . , Ar+1 ) such that for all 1 ≤ i ≤ r there is some ∼∈ {≤, ≥}such that for all νj , νj+1 appearing together in Ai , we have νj (c) ∼c νj+1 (c).
We define sGTRS with reversal-bounded counters (rbGTRS).
Definition 2 (sGTRSs with r-Reversal-Bounded Counters). We definestate-extended ground tree rewrite system with r-reversal-bounded counters(rbGTRS) as a tuple G = (P, Σ, Γ, R, C, r) where P is a finite set of controlstates, Σ is a finite ranked alphabet, Γ is a finite alphabet of output symbols (i.e.
transition labels), C is a finite set of counters, R is a finite set of rules of theγform (p1 , T1 , θ) −→ (p2 , T2 , µ) where p1 , p2 ∈ P, γ ∈ Γ , θ ∈ ConsC , µ ∈ C 7→ Z,
and T1 , T2 are NTAs over Σ.
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 isa control-state, t a tree, and ν a valuation of the counters. We have a transitionγγ(p1 , t1 , ν1 ) −→ (p2 , t2 , ν2 ) whenever there is a rule (p1 , T1 , θ) −→ (p2 , T2 , µ) ∈ R
such that: (i) (dynamics of counters) θ[ν1 ] is true and ν2 = ν1 + µ, and (ii)(dynamics of trees) t1 = C[t′1 ] for some context C and tree t′1 ∈ L(T1 ) and
t2 = C[t′2 ] for some tree t′2 ∈ L(T2 ). A run π over γ1 . . . γn−1 is a sequence
γ1

γn−1

(p1 , t1 , ν1 ) −→ · · · −−−→ (pn , tn , νn )γisuch that for all 1 ≤ i < n we have (pi , ti , νi ) −→ (pi+1 , ti+1 , νi+1 ) is a transition of G and for each c ∈ C the sequence ν1 , . . . , νn is r-reversal-bounded forγ1 ...γnc. We say that γ1 . . . γn−1 is the output string of π. We write (p, t, ν) −−−−→
′ ′
′
∗
′ ′
′
(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.

6

Matthew Hague and Anthony Widjaja Lin

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 (p1 , T1 ) −→ (p2 , T2 ). The standard notion of GTRS (i.e.
not state-extended) [32] is simply sGTRS without counters with only one state.
We next define the problems of (global) reachability. To this end, we use atree automaton T (resp. an existential Presburger formula φ) to represent thetree (resp. counter) component of a configuration. More precisely, a symbolic
config-set 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 freevariables x̄ = {xc }c∈C (i.e. one free variable for each counter). Each symbolic
config-set (c, T , φ) represents a set of configurations of G defined as follows:[[(p, T , φ)]] := {(p, t, ν) : t ∈ L(T ), φ(ν) is true}.
Global Reachability
Instance: an rbGTRS G and two symbolic config-sets (p1 , T1 , φ1 ) (p2 , T2 , φ2 )Question: Decide whether (p1 , t1 , ν1 ) →∗ (p2 , t2 , ν2 ), for some (p1 , t1 , ν1 ) ∈[[(p1 , T1 , φ1 )]] and (p2 , t2 , ν2 ) ∈ [[(p2 , T2 , φ2 )]]The problem of control-state reachability can be defined by restricting (i) thetree automata T1 and T2 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.

Remark 3. When we measure the complexity of reachability for rbGTRS, thenumber r of reversals is represented in unary, while the numbers in counter
constraints and valuations are represented in binary. This is consistent withthe standard representation of numbers in previous work on reversal-bounded
counter machines (e.g. see [23, 24]). The unary representation for r can be justified by the fact that bugs can often be discovered within a small number ofreversals.
Weakly-Synchronised Ground Tree Rewrite Systems The control-stateand global reachability problems for sGTRS are known to be undecidable [12, 21].
The problems become NP-complete for weakly-synchronised sGTRS [31, 41],
where the underlying control-state graph (where there is an edge between p1γ
and p2 whenever there is a transition (p1 , T1 ) −→ (p2 , T2 )) may only have cycles of length 1 (i.e. self-loops), i.e., a DAG (directed acyclic graph) possiblywith self-loops. 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 countercomponents.
We define the underlying {control graph of an rbGTRS G = (P,}Σ, Γ, R, C)
as a tuple (P, ∆) where ∆ = (p1 , p2 )γ

(p1 , T1 , θ) −→ (p1 , T2 , µ) ∈ R.

Integer-manipulating programs with recursive parallelism

7

Definition 4 (Weakly-Synchronised rbGTRS). An rbGTRS is said to be
weakly-synchronised if its underlying control graph (P, ∆) is a DAG possiblywith self-loops.

4

Decidability

In this section we will prove the main result of the paper:
Theorem 5. Global reachability for weakly synchronised rbGTRS is NP-complete. In fact, it is poly-time reducible to satisfiability over existential Presburger
formulas.
To prove this theorem, we fix notation for the input to the problem: an rbGTRS
G = (P, Σ, Γ, R, C, r) and two symbolic config-sets (p1 , T1 , φ1 ), (p2 , T2 , φ2 ) of
G. Let C = {ci }ki=1 . 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 ofcounters with constants. [In this sense, G′ only overapproximates the behaviorof 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 (p1 , T1 , φ1 ) to (p2 , T2 , φ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.
Modes of the counters. The first notion that is crucial in our proof is that of modeof a counter [23, 25], which is an abstraction of the values of a counter in a run ofan rbGTRS containing three pieces of information: (i) the region of the countervalue (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 non-decrementing (↑) or nonincrementing (↓). A mode vector is simply a k-tuple of modes, one mode for eachof the k counters. We now formalise these notions.
Let d1 < . . . < dm 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 := {A0 , . . . , Am , B1 , . . . , Bm }, where Bi := {di } (where 1 ≤ i ≤ m),
Ai := {n ∈ Z : di < n < di+1 } (where 1 ≤ i < m), A0 := {n ∈ Z : n < d1 }, andAm := {n ∈ Z : n > dm }. A mode is simply a tuple in REG × [0, r] × {↑, ↓}. A
mode vector is simply a tuple in Modes := REGk × [0, r]k × {↑, ↓}k .
Building the sGTRS G′ . We might be tempted to build G′ by first removing
the counters from G and then embedding Modes into the control-states G′ .
This, however, causes two problems. First, the number of control-states becomes
exponential in k. Second, the resulting system is no longer weakly synchronisedeven though G originally was weakly synchronised. To circumvent this problem,
we adapt a technique from [23]. Every run π of G from (p1 , T1 , φ1 ) to (p2 , T2 , φ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 mostNmax := 2mk(r + 1) diﬀerent mode vectors in σ. This is because a counter can

8Matthew Hague and Anthony Widjaja Lin

only go through at most 2m regions without incurring a reversal. For this reason, we may use the control-states of G′ to store the number of mode vectorsthat G has gone through, while the actual mode vector guessed by G′ will bemade “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 control-states (DAG with
self-loops) of G′ is preserved. [The product graph of two DAGs with self-loops
is also a DAG with self-loops.] We detail the construction below.
Define the weakly-synchronised sGTRS G′ = (P ′ , Σ, Γ ′ , R′ ) as follows. Let′
P := P × [0, Nmax ]. The output alphabet Γ ′ is defined as Γ × R × [0, Nmax ] ×{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 , θ) −→(γ,τ,i,0)(p′ , T ′ , µ) in R, we add the rule ((p, i), T ) −−−−−→ ((p′ , i), T ′ ) for each i ∈(γ,τ,i,1)[0, Nmax ], and ((p, i), T ) −−−−−→ ((p′ , i + 1), T ′ ) for each i ∈ [0, Nmax ). Since G
is weakly-synchronised and the mode counter never decreases, it follows that G′
is weakly-synchronised too. Note also that this construction can be performedin polynomial-time.
Constructing the formula ψ∧ψ ′ . 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 ((p1 , 0), T1 ) to (S, T2 ), where S = {p2 } × [0, Nmax ]. More precisely, the set z
of free variables of ψ include za for each a ∈ Γ ′ . Furthermore, for each valuationµ ∈ z 7→ Z, it is the case that ψ(µ) is true iﬀ µ ∈ P(L). Such a formula is known
to be polynomial-time computable since G′ is a weakly-synchronised 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 Nmax distinct mode vectors
through runs of G′ . More precisely, the formula ψ ′ is the conjunction
φ1 (x) ∧ φ2 (y) ∧ Dom(m0 , . . . , mNmax ) ∧ Init(m0 )∧GoodSeq(m0 , . . . , mNmax ) ∧ Respect(z, m0 , . . . , mNmax ) ∧ EndVal(x, y, z).
The set x consists of variables xi (1 ≤ i ≤ k) which contain the initial value ofthe ith counter. Similarly, the set y consists of variables yi (1 ≤ i ≤ k) whichcontain the final value of the ith counter. Each mi denotes a set of variables forthe ith mode vector defined as follows:– regji (for each j ∈ [1, k]) — to encode which of the 2m + 1 possible regions
the jth counter is in.
– revji (for each j ∈ [1, k]) — to encode how many reversals have been used
up by the jth counter.
– arrji (for each j ∈ [1, k]) — to encode whether the jth counter is nonincrementing or non-decrementing.
We detail each subformula below.
The subformula Dom asserts that each variable in mi (for each i) has the rightdomain (i.e. range of integer values). More precisely, for each j ∈ [1, k], we add

Integer-manipulating programs with recursive parallelism

9

the conjuncts: (i) 0 ≤ regji ≤ 2m, (ii) 0 ≤ revji ≤ r, and (iii) 0 ≤ arrji ≤ 1. For
the first constraint, we use an even number of the form 2i to represent the region
Ai , and an odd number 2i − 1 to represent the region Bi . The last constraint
simply encodes non-decrementing (↑) as 1, and non-incrementing (↓) as 0.
The subformula Init asserts that m0 is an initial mode vector. More precisely, for each j ∈ [1, k], we add the conjuncts revj0 = 0.
The subformula GoodSeq asserts that m0 , . . . , mNmax forms a valid sequenceof mode vectors. More precisely, for each i ∈ [0, Nmax ) and each j ∈ [1, k],
we add the conjuncts: (i) arrji ̸= arrji+1 ⇒ revji+1 = revji + 1, (ii) arrji =arrji+1 ⇒ revji+1 = revji , (iii) regji < regji+1 ⇒ arrji+1 = 1, and (iv) regji >regji+1 ⇒ arrji+1 = 0. For example, the first constraint asserts that a change inthe direction (non-incrementing or non-decrementing) 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 m0 , . . . , mNmax of mode vectors. In eﬀect, this subformula
ensures that G′ faithfully simulates G. Firstly, we need to assert that the jthcounter values at the start and at the end of the ith mode of G′ (which are
encoded in z) are in the right regions regji . To state this more precisely, for eachγrule τ = (p, T , θ) −→ (p′ , T ′ , µ) in R, we let µj (τ ) denote the value µ(cj ). For eachi ∈ [0, Nmax ] and j ∈ [1, k], we denote by the notation StartCounterij the term∑i−1 ∑
xj + s=0 (γ,τ,s,l) µj (τ )×z(γ,τ,s,l) , where γ, τ , and l, range over, respectively, Γ ,R, and {0, 1}. Similarly, we denote by EndCounterij the term StartCounterij +∑ii(γ,τ,i,0) µj (τ )×z(γ,τ,i,0) . We add the conjuncts: (i) regj = 2h ⇒ EndCounterj ∈Ah , for each h ∈ [0, m], and (ii) regji = 2h + 1 ⇒ EndCounterij ∈ Bh , for eachh ∈ [0, m). [Note that formulas of the form g ∈ A, for a Presburger term g
and a set S ∈ {A0 , . . . , Am , B1 , . . . , Bm }, can be easily replaced by quantifierfree Presburger formulas, e.g., g ∈ A0 stands for g < d1 .] To ensure that theinitial condition is correct, for each j ∈ [1, k], we add the following conjuncts:(1) StartCounter0j ∈ Ah ⇒ regj0 = 2h, and (2) StartCounter0j ∈ Bh ⇒ regj0 =2h + 1. Secondly, we need to state that the transitions executed in each modeare valid (i.e. satisfy the counter constraints). More precisely, for each γ ∈ Γ ,τ ∈ R, i ∈ [0, Nmax ], and l ∈ {0, 1}, if θ is the counter constraint in τ , we add
the conjunct z(γ,τ,i,l) > 0 ⇒ θ(StartCounteri1 , . . . , StartCounterik ). Next we
assert that, when the jth counter is non-incrementing (resp. non-decrementing),
only non-negative (resp. non-positive) counter increments are permitted. Moreprecisely, for each i ∈ [0, Nmax ], j ∈ [1, k], l ∈ {0, 1}, and τ ∈ R, if µj (τ ) > 0,then add the conjunct arrji = 0 ⇒ z(γ,τ,i,l) = 0; if µj (τ ) < 0, then add the
conjunct arrji = 1 ⇒ z(γ,τ,i,l) = 0.
Finally, the subformula EndVal simply asserts that, starting from the initialcounter value x and following the transitions z, the end counter values are y.
max
To this end, we can simply add the conjunct yj = EndCounterN
for eachjj ∈ [1, k].
This concludes the formula construction. It is immediate that G′ faithfully
simulates G iﬀ ψ ∧ ψ ′ is true. In addition, the formula construction runs in10Matthew Hague and Anthony Widjaja Lin

polynomial-time. Since satisfiability over existential Presburger formulas is NPcomplete [39], the NP upper bound for Theorem 5 follows. NP-hardness alreadyholds for the restricted model where the tree component is a stack [23].

5Senescent Ground-Tree Rewrite Systems

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 control-state graphs
leads to undecidability of reachability even without reversal bounded counters.
In this section we explore the notion of senescence [22], which is more generalthan 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.
Theorem 6 (Control-State Reachability of Senescent rbGTRS). The
control-state reachability problem for senescent rbGTRS is undecidable.
5.1

Model Definition

Senescence allows the underlying control-state graph to have arbitrary cycles(instead of only self-loops). For sGTRS, control-state reachability is decidable
under an “age restriction” that is imposed on the nodes that can be rewritten. That is, when the control-state 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).
p′

p
a
b

1

a

2

c

1

d

0

b

p
a

3

a

2

b

0

b

0

c

0

1

p
a

2

c

1

d

0

b

2

a

1

b

0

0

c

0

(a) A transition changing the control-state. (b) A transition that does not change thecontrol-state.

Fig. 1: Transitions of a senescent GTRS.
Before the formal definition, two example transitions of a senescent rbGTRS
are shown in Figure 1. A configuration is written as its control-state and countervalues ((p, ν) or (p′ , ν ′ )) with the tree appearing below. In the tree, the label ofeach 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 1a the transition changes the control-state, 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 1b. In this case, the nodes that are notrewritten maintain the same age. The senescence restriction disallows runs where
nodes older than a fixed age are rewritten.

Integer-manipulating programs with recursive parallelism

11

More formally, given a run
γ1

γn−1

(p1 , t1 , ν1 ) −→ · · · −−−→ (pn , tn , νn )of an rbGTRS, let C1 , . . . , Cn−1 be the sequence of tree contexts used in thetransitions from which the run [was ]constructed. That is, for all 1 ≤ i < n, we
γiin
have ti = Ci [tout→ (pi+1 , Ti′ , µi ) was thei ] and ti+1 = Ci ti+1 where (pi , Ti , θi ) −outinrewrite rule used in the transition and ti ∈ L(Ti ), ti+1 ∈ L(Ti′ ) were the treesthat were used in the tree update.
For a given position (pi , ti , νi ) in the run and a given node η in the domainof ti , the birthdate[ ] of the node is the largest 1 ≤ j ≤ i such that η is in thedomain of Cj tin
and η is in the domain of Cj [x] only if its label is x. The age
jof a node is the cardinality of the set {i′ | j ≤ i′ < i ∧ pi′ ̸= pi′ +1 }. That is, theage is the number of times the control-state changed between the jth and theith configurations in the run.
A lifespan-restrictedrun [with ]a lifespan) of r is a run such that each transition
γi (
in
out
(pi , Ci [tout
],
ν
)
−
→
p
,
C
t
,
ν
i
i+1
i i+1
i+1 has the property that all nodes η in ti
ihave an age of at most r. That is, more precisely, that all nodes η in the domain
of Ci [touti ] but only in the domain of Ci [x] if the label is x have an age of at mostr.
Definition 7 (Senescent rbGTRS). A senescent rbGTRS with lifespan r is
an rbGTRS G = (P, Σ, R, C) where runs are lifespan-restricted with a lifespanof r.
Note that the senescence restriction is weaker than the weakly-synchronised
restriction in that the number of times the finite control could change stateis unbounded. In fact, a node could be aﬀected by an unbounded number ofcontrol-state changes so long as it is always rewritten without becoming fixed(i.e. reaches age r).
5.2

Undecidability

We show control-state reachability for senescent rbGTRSs is undecidable in thefull version, 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, forall symbols a we wish to keep live and all control-states 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 control-states, we can preventa node from keeping itself fresh in certain situations.
We follow the proof that reachability for reset Petri nets is undecidable [3].
We simulate a two-counter machine. Testing whether such a machine can reacha given control-state while having counters with value zero is undecidable.
Let the two counters be c1 and c2 . In the tree, we track the value of acounter c ∈ {c1 , c2 } by the number of live leaves labelled with the counter12

Matthew Hague and Anthony Widjaja Lin

name c. E.g. the tree •(c1 , •(c2 , ∗)) 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 incrementa counter we add a new leaf labelled c. To decrement a counter, we rewritea 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
reversal-bounded counters, the number of increments made to each counter, andin separate reversal-bounded counters,
the numberof decrements. That is, we
{
}
− + −
have reversal bounded counters c+
,
c
,
c
,
c
.
When
we simulate an increment112
2
of c1 we add a leaf and increment c+
.
When
we
simulatea decrement of c2 we
1rewrite a leaf to a null character and increment c−.
Similarly
for c2 . We simulate
1
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 control-state changes to fix thenodes corresponding to the counter. That is, we move to a control-state 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 thetarget control-state 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, thesimulated 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 c1 we will have c+
1 > c1 . This cannot be correctedby the simulation. Thus, at the end of the run, we check whether the numberof 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 thetwo-counter machine has a corresponding run. This completes the gist of thesimulation of a two-counter machine.

6

Extensions and Future Work

We proposed sGTRS with counters as a model of recursively parallel programswith unbounded recursion, thread creation, and integer variables. To obtain decidability, we gave an underapproximation in the form of weak sGTRS withreversal-bounded counters. We showed that the reachability problem for thismodel is NP-complete; in fact, polynomial-time 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 control-state reachability problem.

Integer-manipulating programs with recursive parallelism

13

One possible avenue of future work is to investigate what happens when local
integer values are permitted. That is, reversal-bounded counters can be stored on
the nodes of the tree. We may also study techniques that allow nodes to containmultiple labels, permitting the modelling of multiple local variables without animmediate exponential blow up.
Acknowledgments We thank anonymous reviewers for their helpful feedback.
This work was supported by the Engineering and Physical Sciences ResearchCouncil [EP/K009907/1] and Yale-NUS College Startup Grant.

References
1. P. A. Abdulla, M. F. Atig, and J. Cederberg. Analysis of message passing programs
using SMT-solvers. In ATVA, pages 272–286, 2013.
2. C. Aiswarya, P. Gastin, and K. N. Kumar. Verifying communicating multipushdown systems via split-width. In ATVA, pages 1–17, 2014.
3. T. Araki and T. Kasami. Some Decision Problems Related to the Reachability
Problem for Petri Nets. Theoretical Computer Science, 3(1):85–104, 1977.
4. M. F. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata
is 2etime-complete. In DLT, pages 121–133, 2008.
5. M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent
programs with dynamic creation of threads. Logical Methods in Computer Science,
7(4), 2011.
6. M. F. Atig and P. Ganty. Approximating petri net reachability along context-freetraces. In FSTTCS, pages 152–163, 2011.
7. M. F. Atig, K. N. Kumar, and P. Saivasan. Adjacent ordered multi-pushdown
systems. Int. J. Found. Comput. Sci., 25(8):1083–1096, 2014.
8. S. Bardin, A. Finkel, J. Leroux, and P. Schnoebelen. Flat acceleration in symbolicmodel checking. In ATVA, pages 474–488, 2005.
9. A. Blumensath, T. Colcombet, D. Kuperberg, P. Parys, and M. Vanden Boom.
Two-way cost automata and cost logics over infinite trees. In CSL-LICS, pages
16:1–16:9, 2014.
10. A. Bouajjani and M. Emmi. Analysis of recursively parallel programs. ACM Trans.
Program. Lang. Syst., 35(3):10, 2013.
11. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, pages 135–150, 1997.
12. L. Bozzelli, M. Kretı́nský, V. Rehák, and J. Strejcek. On decidability of LTL model
checking for process rewrite systems. Acta Inf., 46(1):1–28, 2009.
13. T. Colcombet and C. Löding. Regular cost functions over finite trees. In LICS,
pages 70–79, 2010.
14. W. Czerwinski, P. Hofman, and S. Lasota. Reachability problem for weak multipushdown automata. Logical Methods in Computer Science, 9(3), 2013.
15. M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In
LICS, pages 242–248, 1990.
16. L. M. de Moura and N. Bjørner. Z3: An eﬃcient smt solver. In TACAS, pages
337–340, 2008.
17. S. Demri, M. Jurdzinski, O. Lachish, and R. Lazic. The covering and boundedness
problems for branching vector addition systems. J. Comput. Syst. Sci., 79(1):23–
38, 2013.
18. J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded
programs. ACM Trans. Program. Lang. Syst., 36(3):9:1–9:29, 2014.

14

Matthew Hague and Anthony Widjaja Lin

19. J. Esparza and A. Podelski. Eﬃcient algorithms for pre* and post* on interprocedural parallel flow graphs. In POPL, pages 1–11, 2000.
20. P. Ganty, R. Majumdar, and M. Monmege. Bounded underapproximations. FMSD,
40(2), 2012.
21. S. Göller and A. W. Lin. Refining the process rewrite systems hierarchy via groundtree rewrite systems. In CONCUR, pages 543–558, 2011.
22. M. Hague. Senescent ground tree rewrite systems. In CSL-LICS, pages 48:1–48:10,
2014.
23. M. Hague and A. W. Lin. Model checking recursive programs with numeric datatypes. In CAV, pages 743–759, 2011.
24. M. Hague and A. W. Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, pages 260–276, 2012.
25. O. H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116–133, 1978.
26. M. Kretı́nský, V. Rehák, and J. Strejcek. Extended process rewrite systems: Expressiveness and reachability. In CONCUR, pages 355–370, 2004.
27. S. La Torre, M. Napoli, and G. Parlato. Scope-bounded pushdown languages. In
DLT, pages 116–128, 2014.
28. A. Lal, T. Touili, N. Kidd, and T. Reps. Interprocedural analysis of concurrent
programs under a context bound. In TACAS, pages 282–298, 2008. Springer-Verlag.
29. M. Lang and C. Löding. Modeling and verification of infinite systems with resources. Logical Methods in Computer Science, 9(4), 2013.
30. J. Leroux, M. Praveen, and G. Sutre. Hyper-ackermannian bounds for pushdown
vector addition systems. In CSL-LICS, pages 63:1–63:10, 2014.
31. A. W. Lin. Weakly-synchronized ground tree rewriting (with applications to verifying multithreaded programs). In MFCS, pages 630–642, 2012.
32. C. Löding. Reachability problems on regular ground tree rewriting graphs. Theory
Coput. Syst., 39(2):347–383, 2006.
33. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL,
pages 283–294, 2011.
34. R. Mayr. Decidability and Complexity of Model Checking Problems for InfiniteState Systems. PhD thesis, TU-Munich, 1998.
35. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing ofmultithreaded programs. In PLDI, pages 446–455, 2007.
36. S. Qadeer. The case for context-bounded verification of concurrent programs. In
SPIN, pages 3–6, 2008.
37. G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. Transactions on Programming Languages and Systems (TOPLAS), 2000.
38. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software.
In TACAS, pages 93–107, 2005.
39. B. Scarpellini. Complexity of subcases of Presburger arithmetic. Trans. of AMS,
284(1):203–218, 1984.
40. D. Suwimonteerabuth, J. Esparza, and S. Schwoon. Symbolic context-bounded
analysis of multithreaded java programs. In SPIN, pages 270–287, 2008.
41. A. W. To and L. Libkin. Algorithmic metatheorems for decidable LTL model
checking over infinite systems. In FOSSACS, pages 221–236, 2010.
42. S. L. Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive
languages. In In LICS, pages 161–170. IEEE Computer Society, 2007.
43. K. N. Verma and J. Goubault-Larrecq. Karp-Miller trees for a branching extension
of VASS. Discrete Mathematics & Theoretical Computer Science, 7(1):217–230,
2005.