Weakly-Synchronized Ground Tree Rewriting(with applications to verifying multithreaded programs)

Anthony Widjaja Lin
Oxford University Department of Computer Science

Abstract. Ground tree rewrite systems (GTRS) are a well-known treeextension of prefix-rewrite systems on words (a.k.a. pushdown systems),
where subtrees (instead of word prefixes) are rewritten. GTRS can model
programs with unbounded recursion depth and thread-spawning, wherein
the threads have a tree-shaped dependency graph. We consider the extension of GTRS with a finite (global) control unit for synchronizing
among the active threads, a.k.a. state-extended GTRS (sGTRS). SincesGTRS is Turing-complete, we restrict the finite control unit to dags
possibly with self-loops, a.k.a. weakly-synchronized GTRS (wGTRS).
wGTRS can be regarded as a generalization of context-bounded analysis of multipushdown systems with dynamic thread spawning. We showthat reachability, repeated reachability, and the complement of model
checking deterministic LTL over weakly-synchronized GTRS (wGTRS)
are NP-complete by a polynomial reduction to checking existential Presburger formulas, for which highly optimized solvers are available.

1

Introduction

Pushdown systems (PDS) are a natural abstraction of sequential programs withunbounded recursions. Their verification problems have been extensively studied(e.g. see the survey [5]), many of which are not only decidable, but also relatively
tractable.
Apart from having function calls, real-world programs are often multithreaded. Given the rapidly increasing popularity of multi-core computers, multithreaded applications are only becoming increasingly more popular. Most popular programming languages (e.g. Java, Python, C++, C#) now have builtin constructs to support multithreading, e.g., Fork/Join, parbegin-parend,
Parallel.For. Such constructs allow an unbounded number of threads at any
given time (due to thread-spawning). This motivates the study of verification
problems on extensions of pushdown systems with multithreading.
In this paper, we start with a well-known extension of PDS called groundtree rewrite systems (GTRS), e.g., see [14]. Since PDS can be thought of as
prefix-rewrite systems (prefixes are rewritten based on a given set of rewrite
rules on words), GTRS can be construed as a tree-extension of PDS, wherein
subtrees (instead of prefixes) are rewritten based on a given set of rewrite rules
on ranked trees. Owing to the tree structure of GTRS, one can easily mimic theeffect of parbegin-parend and Parallel.For language constructs, whereby a2Anthony Widjaja Lin

parent thread spawns several child threads and waits for the return values ofcomputation of these child threads. This statement actually only holds so longas there is no “shared” (global) variables, which permit synchronization between
the active (instead of waiting) threads.
A natural way to extend GTRS so as to allow synchronization via sharedvariables between the active threads is to extend GTRS with a finite number of (global) control states. Such an extension is called state-extended GTRS(sGTRS). Unlike GTRS, for which reachability and repeated reachability aresolvable in polynomial time, sGTRS can easily simulate multistack pushdown
automata for which most verification problems quickly become undecidable [19].
One way to extend GTRS with control states while staying within the realmof decidability is to disallow cycles (other than self-loops) in the transition graphof the control states of sGTRS. Such transition graphs of (with initial/accepting
states) are often called 1-weak automata [16]. The class of sGTRS which satisfies this restriction is called weakly-synchronized (or weakly-extended) GTRS,
which we abbreviate as wGTRS [21]. It is known [21] that reachability, repeatedreachability, and the complement of model checking deterministic fragment of
LTL (LTLdet ) over wGTRS are all solvable in exponential time, but are NPhard. LTL model checking over GTRS is known to be undecidable (e.g. see [4,11]). For GTRS, reachability and repeated reachability are in P (e.g. [14]).
What is the modeling power of wGTRS? Useful timing and event constraints can be embedded in 1-weak automata (e.g. see [9]). In addition, we shallsee later that wGTRS: (1) generalizes multipushdown systems with bounded context switches [18] by allowing dynamic thread creation using parbegin-parend
or Parallel.For constructs, and (2) provides a natural underapproximation ofsGTRS, where global synchronizations take place for at most a given bound nof times.
Contributions. The main contribution of this paper is a technique for showing
optimal complexity of model checking weakly-synchronized GTRS by a polytime reduction to satisfiability of existential Presburger formulas, which is NPcomplete and for which there are highly-optimized solvers. We firstly consider
the global reachability problem: given a wGTRS P over ranked alphabet Σ andtwo tuples (s0 , S), (t0 , T ) of control states of P and tree automata over Σ, decide
if there exists a path from some configuration (s0 , T1 ) of P, where T1 ∈ L(S)to some configuration (t0 , T2 ) of P, where T2 ∈ L(T ). We show in Section 4that this problem is NP-complete by a reduction to satisfiability of existential
Presburger formulas.
We give several further applications of this upper bound in Section 5: (1)another poly-time algorithm for global reachability for GTRS and (2) NPcompleteness for repeated reachability and the complement of LTLdet model
checking for wGTRS.
In the sequel, when deriving upper bounds, we allow infinitely many rewrite
rules in the input (w)GTRS compactly represented by means of tree automata.
Other related work. There are two other approaches to extend pushdown
systems with dynamic thread spawning. Process rewrite systems hierarchy pro-

Weakly-Synchronized Ground Tree Rewriting3

posed by Mayr [17]. Some classes of systems in this hierarchy (including PA andPAD processes) are intimately connected to GTRS [11]. Another approach wasconsidered by Bouajjani et al. [3] in their work on networks of pushdown systems(called CPDN).
The authors of [13] studied the extension of process rewrite systems andother classes in the hierarchy with 1-weak finite control unit. They showed that
decidability can still be retained for reachability, among others. Decidability andundecidability of fragments of LTL have also been fully classified [4]. The techniques considered in this paper can be easily adapted to show that reachability,
repeated reachability for weakly extended PA and PAD are NP-complete, while
LTLdet model checking for weakly extended PA and PAD are coNP-complete.
Context-bounded model checking over multipushdown systems was first studied in [18] and is shown to be NP-complete for multipushdown systems. Various
extensions have been proposed including phase-bounds [22], ordered multi-stackmachines [1], bounded languages [8, 10], dynamic thread creation [2], and moregeneral approach [15]. The work of [2] considers a different style of multithreading than what we consider in this paper. The difference is akin to the difference
between GTRS and CPDN, which are unexplored. We leave it as future work to
explore the connections.

2

Preliminaries

General notations For two given natural numbers i ≤ j, we define [i, j] ={i, i + 1, . . . , j}. Define [k] = [0, k]. Given a function f : S1 → S2 and a subset
S1′ ⊆ S1 , the notation f|S′ is used to denote the restriction of f to the domain
1S1′ . Vectors v over a set S are simply elements of S k for some positive integer
k. An example is when S = N, which gives us vectors of naturals. In the sequel,
vectors are also thought of as a function v : I → S, where I is some nonempty
finite index set. Vectors in the standard sense use I = [1, k] for some positive
integer k. When comparing two vectors of naturals u, v over the same index
set I, we use the component-wise ordering. We write u ≤ v iff, for each i ∈ I,u(i) ≤ v(i). This partial ordering ≤ is well-known to be well-founded.
Transition systems Let ACT be a finite set of action symbols. A transition system over ACT is a tuple S = hS, {→a }a∈ACT i, where S is a set of configurations,and →over S. We use → to denote the relaSa ⊆ S × S is a binary relation
+
tion
.
The
notation→(resp.
→∗ ) is used to denote the transitive
→
a
a∈ACT
(resp. transitive-reflexive) closure of →. Given two sets S1 , S2 ⊆ S of configurations, we write S1 →+ S2 if s1 →+ s2 for some s1 ∈ S1 and s2 ∈ S2 . The
notations S1 →∗ S2 and S1 → S2 are defined likewise. We say that a sequence
s1 → · · · → sn is a path (or run) in S (or in →). Given two paths π1 : s1 →∗ s2
and π2 : s2 →∗ s3 in →, we may concatenate them to obtain π1 ⊙ π2 (by gluing together s2 ). Given a subset S ′ ⊆ S, denote by Rec→ (S ′ ) to be the set ofelements s0 ∈ S for which there exists an infinite path s0 → s1 → · · · visiting
S ′ infinitely often, i.e., sj ∈ S ′ for infinitely many j ∈ N. A transition system
S = hS, {→a }a∈ACT i is said to be 1-weak if each path s1 → · · · → sn in S with

4

Anthony Widjaja Lin

s1 = sn satisfies si = si+1 for all i ∈ [1, n − 1]. In other words, every cycle in S
is a self-loop.
Word languages and Parikh images An alphabet Σ is a finite set of symbols.
We use standard notations from word language theory (e.g. [12]). Given a wordw ∈ Σ ∗ and a ∈ Σ, we use |w|a to denote the number of occurrences of a inw (e.g. |abaa|a = 3). The Parikh image of w, denoted by P(w), is the integral
vector v : Σ → N such that v(a) = |w|a . Given a language L ⊆ Σ ∗ , its Parikh
image is P(L) = {P(w) : w ∈ L}.
Tree automata and languages A ranked alphabet is a nonempty finite set ofsymbols Σ equipped with a rank function rank : Σ → N. When the context is
clear, a ranked alphabet will simply be referred to as an alphabet. Let rank(Σ)
denote max{rank(a) : a ∈ Σ}. A tree domain D is a nonempty finite subset ofN∗ satisfying (1) prefix closure, i.e., if vi ∈ D with v ∈ N∗ and i ∈ N, then v ∈ D,(2) younger-sibling closure, i.e., if vi ∈ D with v ∈ N∗ and i ∈ N, then vj ∈ D foreach natural number j < i. Standard terminologies (e.g. nodes, parents, children,
ancestors, descendants) will be used. A tree over a ranked alphabet Σ is a pair
T = (D, λ), where D is a tree domain and the node-labeling λ is a function
mapping D to Σ such that, for each node v ∈ D, the number of children of v inD equals the rank rank(λ(v)) of the node label of v. Write Tree(Σ) for the setof all trees over Σ. In the sequel, we also use the standard term representationsof trees (cf. [6]).
A (bottom-up) nondeterministic tree-automaton (NTA) over a ranked alphabet Σ is a tuple A = hQ, ∆, F i, where Q is a finite nonempty set of states, ∆ isaa finite set of rules of the form (q1 , . . . , qr ) ֒→ q, where a ∈ Σ, r = rank(a), andaq, q1 , . . . , qr ∈ Q, and F ⊆ Q is a set of final states. A rule of the form () ֒→ qa
is also written as ֒→ q. For a state q ∈ Q, the notation Aq is used to denotethe NTA hQ, ∆, {q}i. A run of A on a tree T = (D, λ) is a mapping ρ from D
to Q such that, for each node v ∈ D (with label a = λ(v)) with its all childrenav1 , . . . , vr , it is the case that (λ(v1 ), . . . , λ(vr )) ֒→ λ(v) is a transition in ∆. For′
a subset Q ⊆ Q, the run is said to be accepting if ρ(ǫ) ∈ F . The NTA is said toaccept T if it has an accepting run on T . The language L(A) of A is the set oftrees which are accepted by A. A language L is said to be regular if there exists
an NTA accepting L.
A context tree with (context) variables x1 , . . . , xn is a tree T = (D, λ) over thealphabet Σ ∪ {x1 , . . . , xn }, where Σ ∩ {x1 , . . . , xn } = ∅ and for each i = 1, . . . , n,
it is the case that rank(xi ) = 0 and there exists a unique context node ui with
λ(ui ) = xi . In the sequel, we will often denote such a context tree as T [x1 , . . . , xn ]and, by convention, assume that u1 , . . . , un appear in an inorder tree traversal
ordering. Given trees T1 = (D1 , λ1 ), . . . , Tn = (Dn , λn ) over Σ, we use thenotation T [T1 , . . . , Tn ] toSdenote the tree (D′ , λ′ ) obtained by filling each holenxi by Ti , i.e., D′ = D ∪ i=1 ui · Di and λ′ (ui v) = λi (v) for each i = 1, . . . , nand v ∈ Di . Given a tree T , if T = C[t] for some context tree C[x] and a tree t,then t is called a subtree of T .

Weakly-Synchronized Ground Tree Rewriting

5

Notation for Context-free Grammars. A context-free grammar (CFG) overan alphabet Σ is a tuple G = (Nt, Tt, Rules, Start), where Nt is a finite set of
nonterminals, Tt = Σ is a finite set terminals, Rules is a finite set of production
rules of the form X → α where X ∈ Nt and α ∈ (Nt ∪ Tt)∗ , and Start ∈ Nt is
the start nonterminal. In the sequel, for each X ∈ Nt, we use the notation G X todenote the CFG (Nt, Tt, Rules, X). We denote by L(G) the language of words
generated by G.
Existential Presburger formulas Existential Presburger formulas are formulas in the existential fragment of Presburger arithmetic, i.e., first-order theory over hN, +i. If ϕ(x) is a formula with the vector x of free variables, wherex : I → {x1 , . . . , xm } is a vector with some index set I, and v : I → N is avector over natural numbers, we write hN, +i |= ϕ(v) if ϕ is a true formula inhN, +i under the interpretation that maps each variable x(i) to v(i). A formulaϕ(x) is said to be satisfiable in hN, +i if there exists v such that hN, +i |= ϕ(v).
It is well-known that deciding satisfiability over hN, +i is NP-complete [20], forwhich there are highly optimized solvers (e.g. Z3 [7]).

3Weakly extended ground tree rewrite systems

A state-extended ground tree rewrite systems (sGTRS) over a finite set ACT ofaction symbols is a tuple P = hQ, Σ, ∆i, where Q is a nonempty finite set ofcontrol states, Σ is a ranked alphabet, and ∆ is a finite set of rules of the formα(q1 , A1 ) ֒→ (q2 , A2 ), where q1 , q2 ∈ Q, α ∈ ACT, and A1 , A2 are NTA over Σ. A
configuration of P is a tuple (q, T ), where q ∈ Q and T ∈ Tree(Σ). Let Conf(P)denote the set of configurations of P. The transition system generated by P is
SP = hConf(P), {→a }a∈ACT i, where (q1 , T1 ) →α (q2 , T2 ) iff there exist a context
αtree T [x], a rule (q1 , A1 ) ֒→ (q2 , A2 ) in ∆, and trees t1 ∈ L(A1 ) and t2 ∈ L(A2 )such that T1 = T [t1 ] and T2 = T [t2 ]. We define →P to be the union of all →a ,where a ranges over ACT.
The underlying control graph of P = hQ, Σ, ∆i is the finite transition systema
S = hQ, {→a }a∈ACT i, where q1 →a q2 iff (q1 , A1 ) ֒→ (q2 , A2 ) is a rule in ∆. We
say that P is a weakly-synchronized (or weakly-extended) ground tree rewrite systems (wGTRS) if its underlying control graph is 1-weak. In the case of wGTRS,
we often denote edge relation of this underlying control graph as ≺. We saythat P is a ground tree rewrite systems (GTRS) if its underlying control graphis h{q}, {→a }a∈ACT i, where q →a q, for each a ∈ ACT. In this case, a GTRS
P = hQ, Σ, ∆i is also written as hΣ, ∆i (or simply ∆) for simplicity. If eachletter in Σ is of rank ≤ 1, P is also called a pushdown system (PDS).
Remark: “Ground tree rewrite systems” are often defined in a rather restrictive
form, wherein each NTA A in the rewrite rule is explicitly given as a tree t ∈Tree(Σ) representing the singleton set {t}. Our definition of GTRS coincides
with what is commonly referred to as “regular GTRS”. See [14].
Notation: In the sequel, given s ∈ Q and an NTA A over Σ, we shall use thenotation (s, L(A)) to mean {s} × L(A).

6

Anthony Widjaja Lin

We define the (global) reachability problem for sGTRSs as follows: given two
NTAs A1 , A2 over the ranked alphabet Σ, an sGTRS P = hQ, Σ, ∆i, and twostates q1 , q2 ∈ Q, decide if (q1 , L(A1 )) →∗P (q2 , L(A2 )). When we restrict the
input sGTRSs to wGTRSs (resp. GTRSs), we call the resulting subproblems tobe global reachability problem for wGTRSs (resp. GTRSs).
An intuitive example Modeling sequential programs as PDS is standard (e.g.
see [17]): the stack is used to record program points (function names and valuesof local variables), while the finite control is used to record the return values
from the previous function call. Modeling with (s)GTRS is similar except thatthe tree structure can model multithreading.
Consider a program with two functions called fun1 and fun2 (among others).
The function fun2, which we leave unspecified, inputs and outputs a boolean
value. The function fun1 is defined in as follows:
bool b[5]; Par.For(0,4,i,=>){b[i] = fun2(a[i])}; return

4
^

b[i];

i=0

In this example, we assume that the boolean array a is given as input to fun1 andhas size 5. This program simply executes the assignment b[i] = fun2(a[i])in parallel for each i ∈ [0, 4], and afterwards outputs the boolean value obtainedby taking the conjunction of all the boolean variables b[i].
Assuming there is no global variables, the above program can be easily modeled as a GTRS. For example, a GTRS model may contain the following rules:(1) hfun1, s 2, ai → hfun1, s 3, ai(hfun2, s 1, a[0]i, . . . , hfun2, s 1, a[4]i), reflecting the Par.For step (s i means step i), and (2) for all j1 , . . . , j4 ∈ {0, 1},V
hfun1, s 3, ai(j1 , . . . , j4 ) → 4i=0 ji , reflecting the return step of fun1.
With the existence of global (shared) variables, the above GTRS does not
suffice because after rule of type (1) has been applied, the five subthreads can nolonger communicate in this GTRS. Communication in general can be captured
by sGTRS by embedding synchronization in the finite control. wGTRS actually
suffices provided that the vector of values of the shared variables can change
only for a bounded number of times.
Modeling power of wGTRS wGTRS can be used to underapproximatesGTRS. Intuitively, given an sGTRS P and a “depth” parameter d ∈ N, awGTRS Pd is constructed in polynomial time that underapproximates P up tod switches of control states. We can also show that context-bounded analysis
of multipushdown systems [18] can be efficiently reduced to analyzing wGTRS.
Both are shown in the full version.

4

Reachability

Theorem 1. Global reachability for wGTRS is NP-complete. In fact, it is polytime reducible to satisfiability of existential Presburger formulas.
NP-hardness follows from the proof of Proposition 5.4.6 in [21] (by a reduction
from hamiltonian path problem). We now show the upper bound. The idea of theWeakly-Synchronized Ground Tree Rewriting

7

reduction to satisfiability of existential Presburger formulas is as follows: first
construct a CFG G which “overapproximates” the given wGTRS P; the behaviorof G is then limited by adding an extra existential Presburger constraint ψ. Since
there is a linear-time algorithm [24] for computing the Parikh image of L(P) as
existential Presburger formulas Ψ , the desired formula will be Ψ ∧ ψ.
We now provide the details of the reduction. We are given a wGTRS P =hQ, Σ, ∆i over the action alphabet ACT, and two tuples (s0 , S) and (t0 , T ) ofstates s0 , t0 ∈ Q and NTA S, T over Σ representing, respectively, a set {(s0 , T ) :T ∈ L(S)} of start configurations and a set {(t0 , T ) : T ∈ L(T )} of target
configurations. Denote by SP = hConf(P), {→a }a∈ACT i the transition systemgenerated by P. The task is to decide whether (s0 , L(S)) →∗ (t0 , L(T )).
Denote the a-labeled edge relation of the underlying control graph G of P
byclosure (resp. transitive-reflexive closure) of ≺ :=S ≺a , and the transitive
+
∗
≺
by
≺
(resp.
≺). Since G is a DAG possibly with self-loops, it
a
a∈ACT
+
follows that ≺ is antisymmetric, i.e., if s1 ≺+ s2 and s2 ≺+ s1 , then s1 = s2 .
Without loss of generality, we assume that: (1) s0 ≺∗ t0 (for, otherwise, we
immediately have (s0 , L(S)) 6→∗ (t0 , L(T ))), and (2) each state s ∈ Q satisfys0 ≺∗ s ≺∗ t0 (for all T, T ′ ∈ Tree(Σ), i.e., each path (s0 , T ) →∗ (t0 , T ′ ) cannot
go via configurations of the form (s, T ′′ ) with either s0 6≺∗ s or s 6≺∗ t0 ).
We now define the CFG G = (Nt, Tt, Rules, Start). In the following, we
use the notation M (possibly with a subscript) to range over the NTAs S,
T , or NTAs appearing in ∆. The notation q M (possibly with a subscript) will
be used to denote a state in the NTA M. The notation qFM will be used todenote a final state of M. The starting nonterminal Start ∈ Nt is marked. Add
the rule Start → X(s0 ,qFS ),(t0 ,qFT ) , for each qFS and each qFT . The nonterminalX(s0 ,qFS ),(t0 ,qFT ) is initially unmarked. We then repeat the following two rules
until all elements of Nt have been marked. If X(s,qM1 ),(t,qM2 ) ∈ Nt is unmarked,
then mark X(s,qM1 ),(t,qM2 ) and apply the following rules:aa(Rule I) For all transitions (q1M1 , . . . , qrM1 ) ֒→ q M1 and (q1M2 , . . . , qrM2 ) ֒→q M2 in M1 and M2 , respectively, add the ruleX(s,qM1 ),(t,qM2 )→X(s,qM1 ),(t,qM2 ) · · · X(s,qrM1 ),(t,qrM2 )1

1

to Rules and add each X(s,qM1 ),(t,qM2 ) on the r.h.s. of the rule to Nt uni
imarked (if not already a member of Nt).
α
(Rule II) For each wGTRS rule r = (s′ , A) ֒→ (t′ , B) with s ≺∗ s′ ≺ t′ ≺∗ t,and each qFA and each qFB , add the ruleX(s,qM1 ),(t,qM2 )→α(s′ , t′ )X(s,qM1 ),(s′ ,qFA ) X(t′ ,qFB ),(t,qM2 )to Rules, add X(s,qM1 ),(s′ ,qFA ) and X(t′ ,qFB ),(t,qM2 ) to Nt unmarked (if notalready a member of Nt), and add (s′ , t′ ) and each letter in α ∈ ACT∗ to Tt.
Observe that s ≺+ t for each X(s,qM1 ),(t,qM2 ) ∈ Nt is an invariant throughout the above procedure.
Termination of this proceS: s ≺+
dure is immediate since (1) Nt ⊆M1 ,M2 {X(s,qM1 ),(t,qM2 )8Anthony Widjaja Lint, and for each i = 1, 2, q Mi is a state of Mi } and the size of the set on the
r.h.s. is at most |Q|2 × (total number of NTA states in P)2 , and (2) the r.h.s.
of each production rule is a word of length at most max{rank(Σ), 4}.
Let m := |Tt|. We use the linear-time algorithm from [24] on the input G toproduce an existential Presburger formula Ψ (x), where x : Tt → {x1 , . . . , xm },capturing the Parikh image of L(G), i.e., for each v : Tt → N, we have v ∈P(L(G)) iff hN, +i |= Ψ (v). We also write x(s, t) to mean x((s, t)), if (s, t) ∈ Tt.
We now define several constraints as quantifier-free Presburger formulas:V– Dom := s≺t,s6=t x(s, t) ≤ 1. This “domain” formula asserts that advancing
from control V
state s to its strict successor t can take place at most once.
– Out≤1 := s≺t1 ,s≺t2 ,distinct(s,t1 ,t2 ) (x(s, t1 ) = 1 → x(s, t2 ) = 0). This formula asserts that from control state s, the system can only advance to at
most one of its successors.
VV– NoIncomp :=s′ :s′ 6=s,s6≺+ s′ ,s′ 6≺+ s ¬Invs′ , wheres:s0 ≺+ s≺+ t0 Invs →W
W
Invt is a shorthand for the formula s≺t x(s, t) = 1 ∨ t≺s x(t, s) = 1.
Intuitively, if a control state s is involved in a path, then no control statesthat are incomparable to s (with respect to ≺+ ) can be involvedin this path.
W– if s0 = t0 , then Init := ⊤, and if s0 6= t0 , then Init := s0 ≺t,s0 6=t x(s0 , t) =1. This formulaVstates that the system must advance from the initial state.
– Progress := t∈Q,s0 ≺+ t≺+ t0 ,distinct(s0 ,t,t0 )WW′t≺t′ ,t6=t′ x(t, t ) = 1 . This formula states that thes≺t,s6=t x(s, t) = 1 →system must advance from a control state it is in to one of its successors.
In the sequel, we let ϕ1 denote the formula Dom ∧ Out≤1 ∧ NoIncomp, and ϕ2
denote the formula Init∧Progress. The desired existential Presburger formulais ϕ := Ψ ∧ϕ1 ∧ϕ2 . Correctness of the reduction follows from the following lemma.
Lemma 2 (Correctness of Reduction). For each w ∈ ACT∗ , (s0 , L(S)) →v(t0 , L(T )) for some v ∈ ACT∗ with P(v) = P(w) iff there exists v : Tt → N suchthat v(a) = |w|a for each a ∈ ACT and hN, +i |= ϕ(v).
It is not hard to show that the reduction takes polynomial time; more precisely,2
2
O(|Q|3 + (rank(Σ) × N )) time, where N := (|Q|2 × Nmax
) × (Mmax+ |∆|), Nmax
be the maximum number of automata states in any given NTA appearing in P
or S or T , and Mmax be the maximum number of automata transitions in any
given NTA in P or S or T . The analysis is given in the full version.
Remark: Adding a “counting constraint” on the path as an existential Presburger
formula is easy. Such a counting constraint is simply an existential Presburger
formula ψ(x′ ), where x′ = x|ACT . In this case, the desired formula is simply ϕ ∧ ψ.
Correctness: Proof of Lemma 2 The proofs for both directions of Lemma
2 are done by induction. However, in both cases, we will have to strengthen
the statements; for, otherwise, the induction hypothesis will not get us off theground. To this end, we will define a slight variant of the transition system SP
generated by P (which we call S′P ).

Weakly-Synchronized Ground Tree Rewriting

9

Let S′P be the transition system obtained by adding to SP each ǫ-transition(s, T ) →ǫ (t, T ), for each T ∈ Tree(Σ) and s ≺+ t. Given a path
π = (p0 , T0 ) →a1 · · · →an (pn , Tn )in S′P and w = a1 · · · an , we define χ(π) to be the vector v : Tt → N such that(1) if a ∈ ACT, then v(a) = |w|a , and (2) if a = (s, t) with s ≺ t, then v(a) is
the number of indices i ∈ [1, n] with (pi−1 , pi ) = (s, t) and ai 6= ǫ.
Lemma 3. For all X(s,qM1 ),(t,qM2 ) ∈ Nt, if w ∈ L(GX(s,qM1 ),(t,qM2 )) withM1
M2
hN, +i |= ϕ1 (P(w)), then there exists a path π : (s, L(Mq1 )) →v (t, L(Mq2 ))in S′P with χ(π) = P(w).

It is not hard to see that Lemma 3 implies the direction (⇐) of Lemma 2. A
proof can be found in the full version.
Proof (of Lemma 3). As we previously saw, we have s ≺+ t for eachX(s,qM1 ),(t,qM2 ) ∈ Nt. The proof is by induction on the length of derivationsof the word w from X(s,qM1 ),(t,qM2 ) .
The base case is when X(s,qM1 ),(t,qM2 ) → ǫ, which is a production rule generaaated by Rule I. This means that there exists a ∈ Σ such that ֒→ q M1 and ֒→ q M2
M1
M2
are transitions of M1 and M2 , respectively, and thus a ∈ L(Mq1 )∩L(Mq2 ).
Since s ≺+ t, it follows that (s, a) →ǫ (t, a) is path π in S′P . It is also easy to
see that P(ǫ) = χ(π) = 0, and that hN, +i |= ϕ1 (0).
We now proceed to the induction cases. There are two cases. We only consider
the first case; the second case is considered in the full version.
The first induction case is when the first production rule applied in thederivation of w from X(p1 ,qM1 ),(p2 ,qM2 ) (with p1 = s and p2 = t) isX(p1 ,qM1 ),(p2 ,qM2 )→α(p3 , p4 )X(p1 ,qM1 ),(p3 ,qM3 ) X(p4 ,qM4 ),(p2 ,qM2 )where q M3 and q M4 are final states of M3 and M4 , respectively. This productionαrule is generated by Rule II, which means that there exists a rule r = (p3 , M3 ) ֒→
(p4 , M4 ) with p1 ≺∗ p3 ≺ p4 ≺∗ p2 in P. We may also write w as α(p3 , p4 )w1 w2 ,X
X
where w1 ∈ L(G (p1 ,qM1 ),(p3 ,qM3 ) ) and w2 ∈ L(G (p4 ,qM4 ),(p2 ,qM2 ) ). Furthermore,since hN, +i |= ϕ1 (P(w)) and P(w1 ), P(w2 ) ≤ P(w), it follows that hN, +i |=ϕ1 (P(wi )) for each i = 1, 2. By induction, there exist paths π1 : (p1 , T1 ) →∗Mi
(p3 , T3 ) and π2 : (p4 , T4 ) →∗ (p2 , T2 ) in S′P such that Ti ∈ L(Mqi ), for eachi ∈ [1, 4], and χ(πj ) = P(wj ), for each j = 1, 2. By applying the rule r above,
we also see that π3 : (p3 , T3 ) →α (p4 , T4 ) is a transition in SP . Therefore,
π := π1 ⊙ π3 ⊙ π2 is a path from (p1 , T1 ) to (p2 , T2 ) in S′P . We have χ(π) =P3i=1 χ(πi ) = P(w1 ) + P(w2 ) + P(α(p3 , p4 )) = P(w). This completes the proof
for the second induction case.
⊓⊔
It remains to prove the direction (⇒) of Lemma 2. To this end, we need thefollowing lemma.

10Anthony Widjaja Lin∈

Lemma 4. For all X(s,qM1 ),(t,qM2 )Nt, if there exists a path π

:

M1
M2
(s, L(Mq1 )) →v (t, L(Mq2 )) in S′P , then there exists w ∈ Tt∗ with P(w) =X(s,qM1 ),(t,qM2 )χ(π) such that w ∈ L(G).

To show the direction (⇒) of Lemma 2, first observe that each path π :(s0 , L(S)) →v (t0 , L(T )) in SP is also a path in S′P . By Lemma 4, there exists aword w ∈ L(G) with χ(π) = P(w). Let v := P(w). It follows that hN, +i |= Ψ (v).
It suffices to show that hN, +i |= ϕ1 (v) ∧ ϕ2 (v). If s0 = t0 , it is easy to see thathN, +i |= ϕ1 (v)∧ϕ2 (v). Therefore, assume that s0 6= t0 . In this case, we take theprojection of π on to its first component (i.e. control states), say, p0 , . . . , pk suchthat p0 = s and pk = t. By removing duplicates, we may assume that p0 , . . . , pk
are pairwise distinct control states. This means that for all distinct p, p′ ∈ Q, wehave v(p, p′ ) = 1 iff p = pi−1 and pi for some i ∈ [1, k]. Since p0 , . . . , pk is a pathin the underlying graph of P, it is easy to check now that hN, +i |= ϕ1 (v)∧ϕ2 (v)by exhausting all the five subconjuncts in the formula ϕ1 ∧ ϕ2 .
We now prove Lemma 4. To this end, we need the following technical lemma
about path decompositions for wGTRS.
Lemma 5. For each path π : (p, T1 ) →v (q, T2 ) in S′P , there exists a context
tree C[x1 , . . . , xn ] for some n ∈ N such that:
1. T1 = C[t1 , . . . , tn ] for some trees t1 , . . . , tn ∈ Tree(Σ),
2. T2 = C[t′1 , . . . , t′n ] for some trees t′1 , . . . , t′n ∈ Tree(Σ),
3. for each i ∈ [1, n], there exists a path πi : (p, ti ) →∗ (p1i , t1i ) →αi (p2i , t2i ) →∗αi(q, t′i ) in S′P for some rewrite rule (p1i , Ai ) ֒→ (p2i , Bi ) in P such that t1i ∈2
L(Ai ) andPnti ∈ L(Bi ).
4. χ(π) = i=1 χ(πi ).
It is not hard to see that Lemma 5 implies Lemma 4. The proof is done by induction on χ(π) (with componentwise ordering ≤). The above path decomposition
lemma is used to prove the inductive case. The proof is not hard but tedious,and so is relegated into the full version. For space reasons, we also relegate theproof of Lemma 5 into the full version.

5

Applications

A polynomial-time algorithm for GTRS reachability The reduction fromthe previous section can be easily modified to give another polynomial-timealgorithm for GTRS global reachability. Given the GTRS P and two tuples(s0 , S) and (t0 , T ) of control states and NTAs, consider the CFG G and formulaϕ = Ψ ∧ ϕ1 ∧ ϕ2 produced by the reduction. Observe that, in the case of GTRS,
we have ϕ1 ∧ ϕ2 ≡ ⊤. Therefore, Lemma 2 implies that (s0 , L(S)) →∗P (t0 , L(T ))iff Ψ is a satisfiable Presburger formula iff L(G) 6= ∅. Therefore, we have reduced
global GTRS reachability to language emptiness of CFG, which is solvable inpolynomial time. This gives us another proof of the following proposition.

Weakly-Synchronized Ground Tree Rewriting

11

Proposition 6. GTRS global reachability is solvable in polynomial-time.
Repeated reachability Repeated reachability for sGTRS is the following problem: given an sGTRS P = hQ, Σ, ∆i, an initial set (s0 , L(S)) of configurationsof P given as (s0 , S), a final set C of target configurations of P given as a function mapping a control state p ∈ Q to an NTA Ap over Σ (here, C consistsof configurations of the form (p, T ) for some p ∈ Q and T ∈ L(Ap )), decide
whether (s0 , L(S)) ∩ Rec→P (C) 6= ∅. As for reachability problem, this problem
is undecidable.
Theorem 7. Repeated reachability for wGTRS is NP-complete. In fact, it ispoly-time reducible to satisfiablity of existential Presburger formulas.
NP-hardness follows from the proof of Proposition 5.4.6 in [21] (by a reduction
from hamiltonian path problem). To obtain the upper bound for this theorem,
we reduce this problem to satisfiability of existential Presburger formulas inpolynomial time. To this end, for each p ∈ Q, we define Pp to be GTRS obtainedby restricting P to control state p, i.e., Pp = h{p}, Σ, ∆p i, where ∆p consists of
all rules in ∆ of the form (p, A) →a (p, B). We first use Löding’s result [14] thatan NTA A′p representing Rec→Pp ((p, L(Ap ))) is computable in time polynomial
in kAp k + kPp k, for each p ∈ Q. It follows that (s0 , L(S)) ∩ Rec→P (C) 6= ∅iff, for some p ∈ Q, (s0 , L(S)) →∗P (p, L(A′p )). Applying our poly-time reduction
from the previous section for the problem instance (s0 , L(S)) →∗P (p, L(A′p )), foreach p, and existentially quantifying all free variables, we obtained existential
Presburger sentences ϕp such that (s0 , L(S)) →∗P (p, L(A′p )) iff hN,
W +i |= ϕp . It
immediately follows that (s0 , L(S)) ∩ Rec→P (C) 6= ∅ iff hN,+i|=q∈Q ϕp . ThisW
shows that the desired existential Presburger sentence is q∈Q ϕp .
Model checking deterministic LTL over wGTRS Deterministic LTL(LTLdet ) over ACT is the fragment of LTL with the following syntax:
ϕ, ϕ′ := p | Xϕ | ϕ ∧ ϕ′ | (p ∧ ϕ) ∨ (¬p ∧ ϕ′ ) |(p ∧ ϕ)Op(¬p ∧ ϕ′ )where p ranges over boolean combinations of ACT, and Op ranges over {U, W}.
The semantics [[ϕ]] ⊆ ACTω of an LTL formula ϕ can be defined in the same
way as for LTL, which is standard (e.g. see [23]). Given a transition system
S = hS, {→a }a∈ACT i over ACT, we write [[ϕ]]S to denote the set of configurationss0 ∈ S from which all infinite paths π : s0 →a1 s1 →a2 · · · in S satisfy a1 a2 . . . ∈[[ϕ]]. The problem of model checking deterministic LTL for sGTRS is defined asfollows: given an LTLdet formula ψ and a sGTRS P = hQ, Σ, ∆i over the sameset ACT of action symbols, and an initial set of configurations (s0 , L(S)) of P
represented as the tuple (s0 , S) of control state s0 ∈ Q and NTA S over Σ,
decide if (s0 , L(S)) ⊆ [[ψ]]S .
Theorem 8. LTLdet model checking over wGTRS is coNP-complete. In fact, it
is poly-time reducible to non-satisfiablity of existential Presburger formulas.
coNP-hardness for the problem is known [21]. For space reasons, we relegate theproof for the upper bound into the full version.
Acknowledgment. I thank Matthew Hague and anonymous reviewers for theirhelpful feedback. I am grateful to EPSRC (EP/H026878/1) for their support.

12

Anthony Widjaja Lin

References
1. M. F. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata
is 2ETIME-complete. In DLT, pages 121–133, 2008.
2. M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent
programs with dynamic creation of threads. LMCS, 7(4), 2011.
3. A. Bouajjani, M. Müller-Olm, and T. Touili. Regular symbolic analysis of dynamic
networks of pushdown systems. In CONCUR, pages 473–487, 2005.
4. 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.
5. O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures.
In Handbook of process algebra, pages 545–623. Elsevier, North-Holland, 2001.
6. H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison,and M. Tommasi. Tree automata techniques and applications, 2007.
7. L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages
337–340, 2008.
8. J. Esparza and P. Ganty. Complexity of pattern-based verification for multithreaded programs. In POPL, pages 499–510, 2011.
9. K. Fisler. Toward diagrammability and efficiency in event-sequence languages. Int.
J. Softw. Tools Technol. Transf., 8(4):431–447, Aug. 2006.
10. P. Ganty, R. Majumdar, and B. Monmege. Bounded underapproximations. Formal
Methods in System Design, 40(2):206–231, 2012.
11. S. Göller and A. W. Lin. Refining the process rewrite systems hierarchy via groundtree rewrite systems. In CONCUR, pages 543–558, 2011.
12. D. C. Kozen. Automata and Computability. Springer, 2007.
13. M. Kretı́nský, V. Rehák, and J. Strejcek. Extended process rewrite systems: Expressiveness and reachability. In CONCUR, pages 355–370, 2004.
14. C. Löding. Infinite Graphs Generated by Tree Rewriting. PhD thesis, RWTH
Aachen, 2003.
15. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL,
pages 283–294, 2011.
16. M. Maidl. The common fragment of CTL and LTL. In FOCS, pages 643–652,
2000.
17. R. Mayr. Decidability and Complexity of Model Checking Problems for InfiniteState Systems. PhD thesis, TU-Munich, 1998.
18. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software.
In TACAS, pages 93–107, 2005.
19. G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst., 22(2):416–430, Mar. 2000.
20. B. Scarpellini. Complexity of subcases of presburger arithmetic. Trans. of AMS,
284(1):203–218, 1984.
21. A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches.
PhD thesis, LFCS, School of Informatics, University of Edinburgh, 2010.
22. S. L. Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive
languages. In LICS, pages 161–170, 2007.
23. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program
verification (preliminary report). In LICS, pages 332–344, 1986.
24. K. N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational hornclauses. In CADE, pages 337–352, 2005.