Accelerating tree-automatic relations
Anthony Widjaja Lin
Oxford University Department of Computer Science

Abstract
We study the problem of computing the transitive closure of tree-automatic (binary) relations,which are represented by tree automata. Such relations include classes of infinite systems generated by pushdown systems (PDS), ground tree rewrite systems (GTRS), PA-processes, andTuring machines, to name a few. Although this problem is unsolvable in general, we provide
a semi-algorithm for the problem and prove completeness guarantee for PDS, GTRS, and PAprocesses. The semi-algorithm is an extension of a known semi-algorithm for structure-preserving
tree-automatic relations, for which completeness is guaranteed for several interesting parameterized systems over tree topology. Hence, there is a single generic procedure that solves reachability for PDS, GTRS, PA-processes, and several parameterized systems in a uniform way. As anapplication, we provide a single generic semi-algorithm for checking repeated reachability overtree-automatic relations, for which completeness is guaranteed for the aforementioned classes.
1998 ACM Subject Classification F.4 Mathematical Logic and Formal Languages
Keywords and phrases Semi-algorithm, Model Checking, Infinite Systems, Automata

1

Introduction

Real-world systems are complex and many sources of infinity naturally arise when modelingthem formally, e.g., recursions in function calls, data structures (lists, trees, etc.) of
unbounded size, numeric variables of unbounded size, multi-threading (unbounded number of
threads spawned). Given the modeling power of infinite-state systems, even checking simple
properties (e.g reachability) easily becomes undecidable over simple classes of infinite systems(e.g. those represented by counter machines). Despite this, many interesting properties (e.g.
safety, liveness, temporal-logic specifications) have been shown to be decidable over many
classes of infinite-state systems (e.g. pushdown systems, timed systems, Petri nets, lossy
channel systems, ground tree rewrite systems, and process rewrite systems). We refer thereader to [1, 12, 24, 26, 25, 27, 31] for a glimpse of these decidability results.
Another common approach to infinite-state model checking is to start with expressive(“Turing-powerful”) formalisms that can capture many complex real world features anddevelop semi-algorithms for model checking that can solve many practical instances. A
popular framework for reasoning about complex infinite-state systems has been proposed
under the rubric of regular model checking (e.g. see [5, 7, 9, 28]), in which systems are
represented by “regular” symbolic representations including finite-state automata (overwords, trees, ω-words, etc.) or logical formulas over a decidable theory (e.g. Presburger
formulas). Many regular model checking frameworks (differing in expressive power) havebeen considered in the literature, including (extended) counter systems (e.g. see [9, 7]),
rational graphs (e.g. see [18, 5]), word-automatic graphs with length-preserving relations (e.g.
see [5, 28]), tree-automatic graphs with structure-preserving relations (e.g. see [4, 14]), treetransducers (e.g. see [14]), and a natural subclass of ω-word automatic graphs (e.g. see [11]).
Two commonly considered problems in regular model checking are: (1) given a regularsymbolic representation of a set X of configurations, compute a regular symbolic representation of the set post∗ (X) (or pre∗ (X)) of reachable configurations, and (2) compute a© Anthony W. Lin;
licensed under Creative Commons License NC-ND
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

2

Accelerating tree-automatic relations

regular symbolic representation of the transitive closure R∗ of the transition relation R. The
second problem is more general than the first (e.g. see [5, 29]). Although these problems
are uncomputable in general, semi-algorithms have been developed which can solve these
problems for many interesting practical instances (e.g. see [4, 5, 7, 11, 14, 18, 28]), which
include parameterized systems (i.e. distributed protocols with any number of components
with some underlying topology, e.g., the dining philosopher problem), which cannot easily
be captured by known decidable subclasses. Such semi-algorithms usually employ certain
acceleration techniques, which compute the effect of arbitrarily long sequences of transitions.
From a theoretical perspective, an important problem when designing semi-algorithms inregular model checking is undoubtedly the question of convergence and completeness. As has
been pointed out in [7], many existing semi-algorithms in regular model checking lack generalcompleteness criteria. For example, it was not known if there is a generic semi-algorithm inregular model checking with completeness guarantee (i.e. always terminates and gives correct
solution) over the full class of pushdown systems, let alone strictly more powerful formalisms
like ground tree rewrite systems.
Contributions. We investigate regular model checking under the framework of treeautomatic structures [8]. More precisely, we study the problem of computing the transitive
closure of a given tree-automatic (binary) relation [8]. Such relations are represented by thestandard tree-automata over a product alphabet (extended by a padding symbol) allowing
configurations (i.e. trees) to grow unboundedly in some paths in the systems. Tree-automatic
relations are expressive, i.e., can model the transition graphs of pushdown systems (PDS),
PA-processes (PA), ground tree rewrite systems (GTRS), Petri nets, and even Minsky’s
counter machines and Turing machines.
Our contributions are as follows. We start by showing that the bounded local depth
acceleration technique given in [4] for structure-preserving tree-automatic relations (i.e. which
only relate trees with the same structure) can be extended to the full class of tree-automatic
relations. Roughly speaking, for each k and a tree-automatic relation R, the resulting
algorithm computes a tree-automatic relation bRck such that each pair (T, T 0 ) ∈ bRck has
a witnessing path in R, wherein each node is “modified” at most k times. In the casewhen bRck is transitive (which can be effectively checked), we have R∗ = bRck . The semialgorithm simply tries to find a number k such that bRck is transitive. Abdulla et al. hasgiven some interesting instances of parameterized systems with tree topology for which thesemi-algorithm (for structure-preserving case) is guaranteed to terminate [4]. Our main
contribution is to show that the extended semi-algorithm is also guaranteed to terminate
for several well-studied classes of infinite systems including PDS, PA-processes, and GTRS.
As an application, we combine this with the result from [29] to obtain a semi-algorithm fortesting repeated reachability, which is guaranteed to terminate for PDS, PA, and GTRS.
Hence, we have a uniform solution for (repeated) reachability for PDS, PA, and GTRS.
Discussion and Related Work. There are known specialized algorithms for computing
the reachability relations (i.e. transitive closure) for PDS [15], PA-processes [26], and GTRS
[19, 16] in polynomial time. Although our semi-algorithm has worse upper bounds on therunning time, it is more general since it can solve instances of parameterized systems with tree
topology [4]. The purpose of this paper has never been to provide more efficient algorithms
for PA-processes, GTRS, and PDS. Rather, we only intend to show the possibility of devising
a single generic semi-algorithm that is guaranteed to terminate for the aforementioned classesof systems, as well as other systems that cannot be easily captured by known decidable
subclasses. We leave it for future work to evaluate how the semi-algorithms perform inpractice on PA-processes, PDS, and GTRS, and if better acceleration techniques can be

A. W. Lindevised for them.
Bouajjani & Touili [14] gave a semi-algorithm for computing the reachability sets in theframework of regular tree model checking, where tree transducers (and structure-preserving
tree-automatic relations) are adopted. Among others, their semi-algorithms are guaranteed
to compute the reachability sets (but not reachability relations) for process rewrite systems(which subsume PA), GTRS (and its extensions), provided that the relations are well-founded(i.e. have no infinite decreasing chain). Process rewrite systems and GTRS are in general
not well-founded, but they showed that PA can be transformed into a well-founded PA while
preserving reachability. The class of relations generated by tree transducers is more expressive
than tree-automatic relations in general, but is less well-behaved than tree-automatic relations(e.g. see [16] and [8]). In particular, it is open whether we can decide repeated reachability,
given a tree transducer that generates R∗ (which is the case for tree-automatic relations[29]). There are also other acceleration techniques in regular tree model checking (e.g. see[3, 6, 13]), but they do not have termination guarantee for PA-processes, PDS, and GTRS.
Using flat acceleration techniques [7, 17], semi-algorithms for computing the reachability
sets (e.g. represented as Presburger formulas) over extended counter systems can be developedthat are guaranteed to solve the subcases of reversal-bounded counter systems, and many
interesting subclasses of Petri nets (e.g. 2-dim vector addition systems). A similar resultof this form can be found in [10], which provides a semi-algorithm which is guaranteed tocompute the reachability sets of timed automata (and more general hybrid systems).

2Preliminaries

General notations For two given natural numbers i ≤ j, we define [i, j] = {i, i + 1, . . . , j}.
Define [k] = [0, k]. Given a set S, we use S ∗ to denote the set of all finite sequences of elementsfrom S. The set S ∗ always includes the empty sequence which we denote by . Given two
sets of words S1 , S2 , we use S1 · S2 to denote the set {v · w : v ∈ S1 , w ∈ S2 } of words formedby concatenating words from S1 with words from S2 . Given two relations R1 , R2 ⊆ S × S,
we define their composition as R1 ◦ R2 = {(s1 , s3 ) : (∃s2 )((s1 , s2 ) ∈ R1 ∧ (s2 , s3 ) ∈ R2 )}.
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 →a ⊆ S × S
S
is a binary relation over S. We use → to denote the relation→. The notationaa∈ACT→+ (resp. →∗ ) is used to denote the transitive (resp. transitive-reflexive) closure of →. 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 (bygluing together s2 ). Given a relation →⊆ S × S and subsets S1 , . . . , Sn ⊆ S, denote by
Rec→ ({Si }ni=1 ) to be the set of elements s0 ∈ S for which there exists an infinite path
s0 → s1 → · · · visiting each Si infinitely often, i.e., such that, for each i ∈ [1, n], there areinfinitely many j ∈ N with sj ∈ Si .
Trees, automata, and languages A ranked alphabet is a nonempty finite set of symbols
Σ equipped with an arity function ar : Σ → N. A tree domain D is a nonempty finite subsetof N∗ 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 for each natural
number j < i. The elements of D are called nodes. Standard terminologies (e.g. parents,
children, ancestors, descendants) will be used when referring to elements of a tree domain.
For example, the children of a node v ∈ D are all nodes in D of the form vi for some i ∈ N.
A tree over a ranked alphabet Σ is a pair T = (D, λ), where D is a tree domain and thenode-labeling λ is a function mapping D to Σ such that, for each node v ∈ D, the number of3

4

Accelerating tree-automatic relations

children of v in D equals the arity ar(λ(v)) of the node label of v. We use the notation |T |to denote |D|. Write Tree(Σ) for the set of all trees over Σ. We also use the standard term
representations of trees (cf. [16]).
A nondeterministic tree-automaton (NTA) over a ranked alphabet Σ is a tuple A =hQ, ∆, F i, where (i) Q is a finite nonempty set of states, (ii) ∆ is a finite set of rules of theaform (q1 , . . . , qr ) −→ q, where a ∈ Σ, r = ar(a), and q, q1 , . . . , qr ∈ Q, and (iii) F ⊆ Q is aaaset of final states. A rule of the form () −→ q is also written as −→ q. 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))
awith its all children v1 , . . . , vr , it is the case that (ρ(v1 ), . . . , ρ(vr )) −→ ρ(v) is a transition in∆. For a subset Q0 ⊆ Q, the run is said to be accepting at Q0 if ρ() ∈ Q0 . It is said to be
accepting if it is accepting at F . The NTA is said to accept T at Q0 if it has an run on Tthat is accepting at Q0 . Again, we will omit mention of Q0 if Q0 = F . The language L(A) of
A is precisely the set of trees which are accepted by A. A language L is said to be regular if
there exists an NTA accepting L. In the sequel, we use kAk to denote the size of A.
A context with (context) variables x1 , . . . , xn is a tree T = (D, λ) over the alphabetΣ ∪ {x1 , . . . , xn }, where Σ ∩ {x1 , . . . , xn } = ∅ and for each i = 1, . . . , n, it is the case thatar(xi ) = 0 and there exists a unique context node ui with λ(ui ) = xi . In the sequel, we
will sometimes denote such a context as T [x1 , . . . , xn ]. Intuitively, a context T [x1 , . . . , xn ]is a tree with n “holes” that can be filled in by trees in Tree(Σ). More precisely, given
trees T1 = (D1 , λ1 ), . . . , Tn = (Dn , λn ) over Σ, we use the notation T [T1 , . . . , Tn ] to denoteSnthe tree (D0 , λ0 ) obtained by filling each hole xi by Ti , i.e., D0 = D ∪ i=1 ui · Di andλ0 (ui v) = λi (v) for each i = 1, . . . , n and v ∈ Di . Given a tree T , if T = C[t] for somecontext tree C[x] and a tree t, then t is called a subtree of T . If u is the context node of C,
then we use the notation T (u) to obtain this subtree t. Given an NTA A = hQ, ∆, F i over Σand states q̄ = q1 , . . . , qn ∈ Q, we say that T [x1 , . . . , xn ] is accepted by A from q̄ (written
T [q1 , . . . , qn ] ∈ L(A)) if it is accepted by the NTA A0 = hQ, ∆0 , F i over Σ ∪ {x1 , . . . , xn },xiwhere ∆0 is the union of ∆ and the set containing each rule of the form −→qi .

3Tree-automatic relations

Fix a nonempty ranked alphabet Σ. We reserve a special symbol ⊥ such that ⊥ ∈/ Σ withar(⊥) := 0. Let Σ⊥ = Σ ∪ {⊥}, and ⊥ := (⊥, ⊥). In order to define the notion of treeautomatic relations, we will need to first define the convolution operator ⊗, which maps a pairof trees over Σ into a tree over the “product alphabet” Σ⊥ := (Σ⊥ × Σ⊥ ) \ ⊥ containing labelsof the form (a, b) with arity ar((a, b)) := max{ar(a), ar(b)}. Given two trees T1 = (D1 , λ1 )and T2 = (D2 , λ2 ) over Σ, their convolution is the tree T1 ⊗ T2 := (D1 ∪ D2 , λ) over Σ⊥such that λ(v) = (λ01 (v), λ02 (v)), where λ0i is the extension of the function λi to the domain
D1 ∪ D2 such that λ0i (w) = ⊥ whenever w ∈/ Di .
Consider a binary relation R ⊆ Tree(Σ) × Tree(Σ). We say that the relation is treeautomatic [8] (also see [16, Chapter 3]) if the language {T ⊗ T 0 : (T, T 0 ) ∈ R} over Σ⊥ isregular. In this case, a presentation of R is any NTA recognizing the language. In the sequel, apresentation of tree-automatic relations is also referred to as a synchronous (tree)-automaton.
The relation R ⊆ Tree(Σ) × Tree(Σ) is said to be structure-preserving if it contains only
pairs (T, T 0 ) of trees with the same tree domains. Therefore, a synchronous automaton
presenting a structure-preserving binary relation runs over the alphabet Σ := Σ × Σ (i.e.
may not take tuples involving ⊥).
A tree-automatic transition system [8] is a transition system of the form S = hS,{→a }a∈ACT i, where for some ranked alphabet Σ: (1) the domain S is the language of someA. W. Lin

5

NTA ADom over Σ, and (2) for each action a ∈ ACT, →a ⊆ Tree(Σ) × Tree(Σ) is atree-automatic relation presented by some NTA Aa . The tuple υ = hADom ; {Aa }a∈ACT i
is said to be a presentation for the transition system S. Given a first-order formulaϕ(x1 , . . . , xn ) over the vocabulary {→a }a∈ACT , we write [[ϕ]]S for the set of interpretations(T1 , . . . , Tn ) ∈ Tree(Σ)n such that S satisfies the formula ϕ, i.e., S |= ϕ(T1 , . . . , Tn ). When
S is understood, we simply write [[ϕ]]. The following are basic results from the theory of(tree)-automatic structures.
I Proposition 1 ([8]). Given a tree-automatic transition system S presented by the presentation υ and a first-order sentence ϕ over the vocabulary of S, checking whether S |= ϕ isdecidable. In fact, if ϕ has free variables x1 , x2 , then a synchronous automaton for [[ϕ]]S iscomputable.
When the input formula is existential, model checking is solvable in exponential time [8].
This implies that given an NTA A presenting the relation R, checking whether R is transitive
can be done in exponential time. This is because non-transitivity can be expressed as∃x, y, z(R(x, y) ∧ R(y, z) ∧ ¬R(x, z)). A simple analysis of the proof of Proposition 1 (e.g. see[29]) also shows that given an automatic transition system S presented by the presentation
υ and a fixed existential positive (i.e. negation-free) first-order formula ϕ(x1 , x2 ), we may
compute a synchronous automaton for [[ϕ]] in time polynomial in the size kυk of υ.

4

Synchronized automata of finite local depth

In this section, we consider an arbitrary tree-automatic binary relation R ⊆ Tree(Σ) ×Tree(Σ) presented by any given synchronous automaton A = hQ, ∆, F i over the alphabetΣ⊥ . We shall keep our terminologies as close to [4] as possible.
The suffix of a state q ∈ Q is the set of contexts T [x] accepted by A from q, i.e.,Ssuff(q) := {T [x] : T [q] ∈ L(A)}. For a subset Q0 ⊆ Q, define suff(Q0 ) := q∈Q0 suff(q). A
context T [x] = (D, τ ) over the alphabet Σ⊥ , with the unique node u such that τ (u) = x, issaid to be copying if for each v ∈ D \ {u} it is the case that τ (v) = (a, a) for some a ∈ Σ.
The state q is said to be idempotent if suff(q) contains only copying contexts, and that, for(a,b)

each transition (q1 , . . . , qm ) −→ q, we have a, b =6 ⊥. [The latter restriction is not imposedin the definition of copying contexts in [4], but is a necessary technical restriction.]
The prefix pref(q) of a state q ∈ Q is defined to be the set of trees accepted by A at {q}.
A tree T = (D, τ ) over Σ⊥ is said to be copying if each v ∈ D satisfies τ (v) = (a, a) for somea ∈ Σ. The state q is said to be a copying (prefix) state if pref(q) contains only copying trees.
Local depth Let Q0 ⊆ Q. Consider a run π := T0 = (D0 , τ0 ), . . . , Tm = (Dm , τm ) throughR such that Ti ⊗ Ti+1 ∈ L(A) with a witnessing run ρi of A, for each i ∈ [m − 1]. Let D
Smdenote the set i=0 Di , and let ρ̄ denote the sequence ρ0 , . . . , ρm−1 . The Q0 -local depth of anode v ∈ D in π with respect to the runs ρ̄ is defined to be the number of indices i ∈ [m − 1]such that ρi (v) ∈ Q0 . Intuitively, it is the number of times v is “touched” by Q0 in the runs
ρ̄. The Q0 -local depth of π with respect to ρ̄ is the maximum of Q0 -local depths of nodesv ∈ D in π wrt ρ̄. The Q0 -local depth of the run π is the minimum of Q0 -local depths of πwith respect to some witnessing runs of A. The Q0 -local depth of a pair (T, T 0 ) ∈ R∗ of trees(with respect to A) is the minimum of Q0 -local depths of runs π = T0 , . . . , Tm through R,
where T0 = T and Tm = T 0 . The Q0 -local depth of the relation R (with respect to A) is thesupremum over all Q0 -local depths of pairs (T, T 0 ) ∈ R∗ . [To understand this last concept,
an analogy to the notion of “diameter” of a graph G (supremum of lengths of paths in G) canbe drawn.] Whenever Q0 is clear, we shall omit mention of Q0 and simply say “local depth”.

6

Accelerating tree-automatic relations

I Example 1. Let Σ = {0, 1, 0̂, 1̂} with ar(0) = ar(1) = 0 and ar(0̂) = ar(1̂) = 2. Define
the relation R ⊆ Tree(Σ) × Tree(Σ) containing tuples (T, T 0 ), where T = C[i] (i = 0, 1)
and T 0 = C[î(j, k)] for some context tree C[x], and some j, k ∈ {0, 1}. It is easy to givean NTA N = hQ, ∆, F i for this relation, where Q = {q, qcpy , qidm } with a copying (resp.
idempotent) state qcpy (resp. qidm ), with {q}-local depth 1. For example, for each i = 0, 1,
(i,i)

(⊥,i)

(î,î)(i,î)

add to ∆ the following transitions: −→ qcpy , −→ q, (qcpy , qcpy ) −→ qcpy , (q, q) −→ qidm ,(î,î)(î,î)(qcpy , qidm ) −→ qidm , and (qidm , qcpy ) −→ qidm . The unique final state is qidm .
Bounded local depth accelerations Given a positive integer k, the k-local depth acceleration bRck,Q0 of the relation R with respect to the state-set Q0 ⊆ Q is the relation
containing all pairs (T, T 0 ) ∈ R∗ of Q0 -local depth at most k. Define the identity relation
Rid = {(T, T ) : T ∈ Tree(Σ)}. Observe that R ∪ Rid ⊆ bRck,Q0 ⊆ R∗ for each positive
integer k. In the case when R has finite Q0 -local depth, we have bRck,Q0 = R∗ for some k.
Again, whenever Q0 is clear from the context, we will simply write bRck .
I Theorem 2. Given a copying state qcpy and an idempotent state qidm of A, the k-local
depth acceleration bRck := bRck,Q\{qcpy ,qidm } of R is tree-automatic. Furthermore, an NTA
presenting bRck can be computed in time polynomial in kAk and exponential in k.
The above theorem is proven by a reduction to the computation of k-local depth accelerationof a structure-preserving relation with two special copying states; the latter can be provenby a simple adaptation of the proof for the subcase shown in [4] with one special copying
state qcpy . [In the technical report of [4], an extension is given with several special copying
states but has a different condition from the above theorem.] This reduction itself is achieved
by “reserving” enough space in the resulting structure-preserving relation (by means of
padding) to simulate computation paths in the original system. Details for the reduction
and adaptation of the proof of [4] are given in the full version.
Using Theorem 2, we can design a simple semi-algorithm (call it bounded local depth
acceleration semi-algorithm) for computing an NTA A∗ for the reachability relation R∗ ofthe tree-automatic relation R presented by A:
1. Let k := 1;
2. Repeat3.
Construct A∗ presenting bRck ; let k := k + 1;
4. Until the relation presented by A∗ is transitive
Checking transitivity of a tree-automatic relation is done using Proposition 1 (see the related
remark). Since R ∪ Rid ⊆ bRck ⊆ R∗ for each positive integer k, termination implies thatthe output is an NTA presenting R∗ .
We will see other examples of (presentations of) tree-automatic relations with finite local
depth in the subsequent sections. The reader is also referred to [4] for nice examples ofparameterized systems modeled by structure-preserving tree-automatic relations.
Checking (generalized) repeated reachability The problem of generalized repeatedreachability for tree-automatic relations is defined as follows: given an NTA presenting atree-automatic relation →⊆ Tree(Σ) × Tree(Σ) and a set {Ni }mi=1 of m NTAs over Σ,
compute the set Rec→ ({L(Ni )}m
)
of
trees
from
which
there
existsa path visiting each
i=1
L(Ni ) infinitely often. As for checking safety, this problem is also undecidable (in fact,
Σ11 -complete); see [29]. However, it is known that whenever →∗ is given as an NTA A∗ aspart of the input, the problem becomes decidable:
I Proposition 2 ([29, 30]). Given two NTAs A and A∗ presenting, respectively, a relation→ and its closure →∗ , and given the set {N }mi=1 of m NTAs over the alphabet Σ, we may

A. W. Lin

7∗compute the set Rec→ ({L(Ni )}mi=1 ) in time polynomial in kAk × kA k ×

Qm

i=1 kNi k.

This proposition (proven in [29]) is a corollary of the result on repeated reachability with
m = 1, which initially appeared in [30] and was proven using Ramsey theory on infinite
graphs. Thus, we may combine this proposition with the bounded local depth acceleration
semi-algorithm to obtain a semi-algorithm for generalized repeated reachability, which isguaranteed to terminate for relations → of finite local depth. In the sequel, we refer to thissemi-algorithm as bounded local depth repeated reachability semi-algorithm.

5

PA-processes

PA-processes [27] are a well-known generalization of basic parallel processes (BPP) andpushdown systems with one-state (a.k.a. BPA). They are known to be incomparable to both
pushdown systems and Petri nets, and are an important class in the well-known process
rewrite systems hierarchy [27].
We follow the presentation of [25] to define PA-processes. Let V = {X, Y, . . .} be a given
finite set whose elements are called process constants. A Process term over V is simply atree in Tree(Γ), where Γ = V ∪ {0, k, ◦} and ar(0) = ar(X) = 0, for each X ∈ V, andar(k) = ar(◦) = 2. Let FV = Tree(Γ). Here, 0 denotes a “nil” process, and ◦ (resp. k)is the sequential (resp. parallel) composition. Process terms are usually represented using
standard term representation of trees where k and ◦ are written in infix notations. A PA
declaration P over V is a set of PA transition rules of the form X → t, where X ∈ V andt ∈ FV . The PA declaration P defines a relation RP ⊆ FV × FV , which we will also write as→P (in infix notation), as given by the following inference rules:
t1 →P t01
t1 kt2 →P t01 kt2
t2 →P t02
t1 kt2 →P t1 kt02

t1 →P t01
t1 ◦ t2 →P t01 ◦ t2
t2 →P t02
t1 ∈ IsNil
t1 ◦ t2 →P t1 ◦ t02

X →P t(X → t) ∈ P

Here IsNil = Tree({0, ◦, k}) is the set of “terminated” process terms.
t2 →P t02t ∈ IsNil

Due to the condition t1 ∈ IsNil in the inference rule t1 ◦ t2 →P t1 ◦ t02 1, an NTA
presenting RP will need two special copying states (one to cater for copying trees in
IsNil, and another for copying trees that are not in IsNil), which is prohibited in ourframework1 . In order to capture PA within our framework, we will have to modify theabove semantics slightly. Extend the ranked alphabet Σ with a new binary symbol ◦R , i.e.,Σ = Γ ∪ {◦R } with ar(◦R ) = 2. The PA declaration P now gives rise to another relation
RP,1 ⊆ Tree(Σ) × Tree(Σ) (also written →P,1 ) obtained from the above inference rules,
t2 →P,1 t02

t ∈ IsNilbut replacing the inference rule t1 ◦ t2 →P,1 t1 ◦ t02 1
by the following two inference rules:(R1) t1 →P,1 t2 , where t1 = (D, τ1 ) and t2 = (D, τ2 ) such that there exists a unique v ∈ D
t2 →P,1 t02

with τ1 (v) = ◦, τ2 (v) = ◦R , and τ1 (u) = τ2 (u) for each u ∈ D \ {v} (R2) t1 ◦R t2 →P,1 t1 ◦R t02 .
Intuitively, trees rooted at a node with label ◦ (resp. ◦R ) can only modify its left (resp.
right) subtrees; the only exception to this is an application of Rule (R1). Note that, once ◦is relabeled to ◦R by Rule (R1), then it cannot be further relabeled.
We now show that the two semantics are equivalent in some precise sense. Let IsNil0 :=Tree({0, ◦, ◦R , k}), i.e., the set IsNil where each ◦-labeled node may possibly be relabeled by1

It is possible to extend our framework to allow several special copying states in a way that subsumes
PA, which we refrain from doing for space reasons

8

Accelerating tree-automatic relations◦R . Let FV0 be the set of trees T ∈ Tree(Σ) such that (i) the left subtree of each ◦R -labelednode is in IsNil0 , and (ii) the left subtree of each ◦-labeled node is not in IsNil0 (i.e. someprocess constant must be found at a leaf). Observe that we can easily construct an NTA
of size O(|Σ|) recognizing FV0 . Let R← ⊆ FV0 × FV consists of tuples (T, T 0 ) where T 0 is
obtained by relabeling each ◦R -labeled node in T by ◦. Notice that this is also a bijectivefunction (by virtue of the conditions (i) and (ii) above), and additionally a tree-automatic
relation which can be presented by an NTA A← of size O(|Σ|).
I Proposition 3. The following statements are equivalent for all trees T1 , T10 , T2 , T20 with
(T10 , T1 ), (T20 , T2 ) ∈ R← :1. (T1 , T2 ) ∈ R∗P
2. (T10 , T20 ) ∈ R∗P,1
Hence, given a synchronous automaton A∗P,1 presenting R∗P,1 , we may compute a synchronous
automaton A∗P presenting R∗P in time polynomial in kA∗P,1 k.
The proof can be found in the full version.
The relation RP,1 is tree-automatic and can be presented by the NTA AP,1 = hQ, ∆, F iover Σ⊥ defined as follows. Suppose that there are n rules in P, where the ith rule is
Xi → ti where ti = (Di , τi ). The set Q includes the states qcpy , qidm , q◦ , and a state qi,v
for each i ∈ [1, n] and v ∈ Di . The set F of final states is {qidm , q◦ } ∪ {qi, : i ∈ [1, n]}.
(a,a)

For each (a, a) ∈ Σ with ar((a, a)) = k, we add the transition (q1 , . . . , qk ) −→ qcpy to ∆,
(k,k)

(k,k)

where q1 = · · · = qk = qcpy . Add the transitions (qcpy , qF ) −→ qidm , (qF , qcpy ) −→ qidm ,(◦R ,◦R )(◦,◦)(qcpy , qF ) −→ qidm , and (qF , qcpy ) −→ qidm , for each final state qF ∈ F , to ∆. Add the(◦,◦R )

transition (qcpy , qcpy ) −→ q◦ to ∆. For each i ∈ [1, n] and  6= v ∈ Di with ar(τi (v)) = k,
add the transition (qi,v0 , . . . , qi,v(k−1) )(⊥,τi (v))−→

qi,v to ∆. For each i ∈ [1, n] with ar(τi ()) = k,

(Xi ,τi ())add the transition (qi,0 , . . . , qi,k−1 ) −→ qi, to ∆. It is easy to see that AP,1 presents
the relation RP,1 and has size O(kPk). Furthermore, it is easy to see that qcpy (resp. qidm )is a copying (resp. idempotent) state. In the sequel, we shall not distinguish P from AP,1 .
I Theorem 3. The local depth of a PA AP,1 is at most O(kPk). Therefore, bounded local
depth acceleration and repeated reachability semi-algorithms terminate on the class of PA.
The proof idea is as follows. Suppose T1 →∗P,1 T2 . If a rule X → t with |t| > 1 is applied toan X-labeled node v along a witnessing path, the label of v will next be in {k, ◦, ◦R }. So,
the only rule that may modify v in the rest of the path is (R1), which can only be applied
at most once at any node. The only problematic case is when we apply rule of the form
X → Y , where X, Y ∈ V. To account for this case, observe that once such rules are applied
for more than |V| times at node v, we have detected redundant applications of PA rules andmay remove them to ensure that such rules are applied at most |V| times at node v. The full
proof is given in the full version.

6

Ground tree rewrite systems

Ground-tree rewrite systems (e.g. [24]) are an extension of prefix-rewrite systems (equivalently,
pushdown systems), where rewrite rules are given as pairs of trees over some ranked alphabet
and they rewrite subtrees (instead of word prefixes). They are incomparable to PA-processes
up to strong bisimulations, but subsume PA-processes up to branching bisimulations [20].
Although local model checking (e.g. fragments of LTL) of PA-processes can be reduced toA. W. Lin

9the same problem over GTRS in polynomial time [20], the same is not known for global
model checking (e.g. computing pre∗ (S) or reachability relations).
A ground-tree rewrite systems (GTRS) [24] over the ranked alphabet Σ is a set P of rulesof the form t1 → t2 , where t1 , t2 ∈ Tree(Σ). A pushdown system (PDS) is a GTRS where Σcontains no label a with ar(a) > 1. We write Dom(P) for the set of trees t on the l.h.s. or
r.h.s. of some rule in P. The GTRS P defines a binary relation RP ⊆ Tree(Σ) × Tree(Σ)
as follows: given two trees T1 , T2 ∈ Tree(Σ), we have (T1 , T2 ) ∈ RP iff there exists a context
C[x] such that T1 = C[t1 ] and T2 = C[t2 ] for some rule (t1 → t2 ) ∈ P. For convenience, wewill also denote (T1 , T2 ) ∈ RP by T1 →P T2 .
We now give an obvious presentation of the relation RP as a synchronous automaton
AP = hQ, ∆, F i over the alphabet Σ⊥ . In the sequel, when understood from the context,
we will confuse GTRS and their presentations. Suppose that there are n rules in P, where
the ith rule is ri : ti → t0i with ti = (Di , τi ) and t0i = (Di0 , τi0 ). We extend the function τi(resp. τi0 ) to N∗ so that whenever v ∈/ Di (resp. v ∈/ Di0 ) we have τi (v) = ⊥ (resp. τi0 (v) = ⊥).
Then, for each i ∈ [1, n] and each node v ∈ Di ∪ Di0 , we add a state qi,v to Q. We also
add two states qidm and qcpy to Q. We now define the transition relation ∆. For each(a,a)

a ∈ Σ with ar(a) = k, we add the transition (q1 , . . . , qk ) −→ qcpy , where q1 = · · · qk = qcpy .
Such a transition will be used in the subtrees that are not rewritten by P. Likewise, foreach i ∈ [1, n] and node v ∈ Di ∪ Di0 with children v0, . . . , v(k − 1) (so vk ∈/ Di ∪ Di0 ), add(τi (v),τ 0 (v))

the transition (qi,v0 , . . . , qi,v(k−1) )−→iqi,v to ∆. Such a transition will occur in thesubtree that is rewritten by P. Finally, for each a ∈ Σ with arity ar(a) = k, we add each(a,a)

possible transition of the form (q1 , . . . , qk ) −→ qidm , where: (1) for a unique index j ∈ [1, k]
we have qj = qidm or qj = qi, for some i ∈ [1, n], and (2) for each other index j 0 6= j, wehave qj 0 = qcpy . The set F of final states consists of qidm and qi, for each i ∈ [1, n]. Notethat kAP k = O(kPk). Observe that qcpy is a copying state, and qidm an idempotent state.
Moreover, it is easy to see that AP presents the relation RP .
I Theorem 4. The local depth of a GTRS AP is bounded exponentially by kAP k. So, bounded
local depth acceleration and repeated reachability semi-algorithms terminate on GTRS.
The proof of this theorem is much more involved than the proof for the case of PA-processes.
This is because in GTRS (and PDS) a subtree may be rewritten (expanded and shrunk) ad
infinitum, unlike for PA-processes where applying any rewrite rule of the form X → t (with t
has more than one node) at a node v guarantees that v can only be touched once more withrule (R1). The proof idea for the theorem is as follows. We will first prove a path factorization
lemma for GTRS, which allows us to consider “simpler” paths. Intuitively, simpler paths arepaths that visit Dom(P), i.e., of the form π : T →∗ t →∗ T 0 , where t ∈ Dom(P). We thenprove upper bounds on the local depths of such paths, which will transfer to local depths for
P. We will spend the rest of this section to sketch the proof of Theorem 4. We first need thefollowing path factorization lemma for GTRS.
I Lemma 5. For two arbitrary trees T1 , T2 ∈ Tree(Σ), it is the case that T1 →∗P T2 iff
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[t01 , . . . , t0n ] for some trees t01 , . . . , t0n ∈ Tree(Σ).
3. for each i ∈ [1, n], there exists a tree t00i ∈ Dom(P) such that ti →∗P t00i →∗P t0i .
Notice that the condition on the r.h.s. of Lemma 5 allows context trees with no variables(i.e. an element of Tree(Σ)), which accounts for the case when T1 →∗P T2 within zero step(i.e. T1 = T2 ). We give the proof of Lemma 5 in the full version.

10

Accelerating tree-automatic relations

Let us now prove Theorem 4. Consider any path σ : T1 →∗ T2 in RP . Let Acpy denote(a,b)

the NTA obtained from AP by removing all transitions in AP of the form (q1 , . . . , qk ) −→ qwith q, q1 , q2 , . . . , qk ∈ Q \ {qcpy , qidm }. That is, we remove the transitions which rewrite
subtrees.
Suppose now that T1 →∗P T2 . By Lemma 5, there exists a context tree
C[x1 , . . . , xn ] = (DC , τC ), along with trees ti , t0i , t00i ∈ Tree(Σ) (for each i ∈ [1, n]), satisfying
the three stated conditions. Let u1 , . . . , un denote the context nodes of C. Let C denotethe context tree (DC , τC0 ) obtained from C by replacing each label a in non-context nodesby (a, a) and leave variables in context nodes as they are, i.e., C is over the alphabet
Σid := {(a, a) : a ∈ Σ} ∪ {x1 , . . . , xn } with ar((a, a)) = ar(a) such that, if v is not a context
node in C, then τC0 (v) = (τC (v), τC (v)); otherwise, τC0 (v) = τC (v). Then, for each i ∈ [1, n],
we see that C[q1 , . . . , qn ] ∈ L(Acpy ), for every q̄ satisfying qi ∈ F and qj = qcpy (j 6= i). We
now need the following lemma.
I Lemma 6. Given two trees t ∈ Dom(P) and T ∈ Tree(Σ), if t →∗P T , then there exists a
witnessing run π : t →∗P T of bounded local depth that is exponentially bounded by kPk.
By considering the new GTRS P −1 obtained by swapping the l.h.s. with the r.h.s. of eachrule in P, this lemma also implies that T →∗P t has a witnessing run of local depth thatis exponentially bounded by kPk. By condition (3) in Lemma 5, this lemma gives a path
π : T1 →∗P T2 in RP of local depth that is exponentially bounded by kPk, which implies
Theorem 4.
It remains to prove Lemma 6. To this end, we will need two ingredients. The first
ingredient (Lemma 7) is an upper bound on local depth of a given tuple (T1 , T2 ) with
T1 →∗P T2 , which will be given by bounds on the length of the shortest witnessing paths.
The second ingredient (Lemma 8) is a lemma for using the first ingredient to derive themaximum of local depths of all tuples (T1 , T2 ) with T1 →∗P T2 .
I Lemma 7. Given two trees T1 , T2 ∈ Tree(Σ), if T1 →∗P T2 , then T1 can reach T2 within
at most k steps, where k is exponentially bounded by kPk + kT1 k + kT2 k.
I Lemma 8. Let T1 = (D1 , τ1 ), T2 = (D2 , τ2 ) ∈ Tree(Σ). Then, T1 →∗P T2 implies that
there exists a context tree C[x1 , . . . , xn ] = (D0 , τ 0 ), for some n ∈ N, with context nodes
u1 , . . . , un such that
1. {u1 , . . . , un } ⊆ D2 , {u1 , . . . , un } ∩ D1 = ∅ and D0 \ {u1 , . . . , un } = D1 ∩ D2 , i.e., each ui
is a node of D2 of the form vj for some leaf node v in D1 and some j ∈ N.
2. for some trees t1 , . . . , tn ∈ Tree(Σ) with |ti | ≤ kPk for each i ∈ [1, n], we have T1 →∗P
C[t1 , . . . , tn ],3. T2 = C[t01 , . . . , t0n ] for some trees t01 , . . . , t0n ∈ Tree(Σ) with ti →∗P t0i for each i ∈ [1, n],Lemma 7 is an immediate corollary of [23, Theorem 1 and Lemma 2]. Intuitively, Lemma 8means that T1 →∗P T2 can go via a tree C[t1 , . . . , tn ], which is not much bigger than T1 , suchthat T2 = C[t01 , . . . , t0n ] and ti →∗P t0i for each i = 1, . . . , n. That is, if we assume that T1 issmall, the intermediate configuration C[t1 , . . . , tn ] is also small, and we can use Lemma 7 on
the path from T1 to C[t1 , . . . , tn ] and apply the same reasoning on the path from ti to t0i , foreach i ∈ [1, n], since each ti is small.
Proof of Lemma 8. Let us take the unique context tree C[x1 , . . . , xn ] = (D0 , τ 0 ) as definedby Condition 1 of the statement of the lemma (note that this context tree depends only on
T1 and T2 ). Let t01 , . . . , t0n ∈ Tree(Σ) be the unique trees such that T2 = C[t01 , . . . , t0n ]. It
suffices to show that Condition 2 and 3 are satisfied. Let π : G0 →P · · · →P Gm be a pathsuch that G0 = T1 and Gm = T2 . Then, for each i ∈ [1, m] there exists a context tree Ci [x]A. W. Linwith context node vi ∈ N∗ and a rule αi → αi0 in P such that Gi−1 = Ci [α] and Gi = Ci [αi0 ].
For each i ∈ [1, n], let ni be the maximum index j ∈ [1, m] such that vj ≺ ui (i.e. vj is anancestor of ui excluding ui ), which must exist since ui ∈/ D1 . Intuitively, ni denotes the lastpoint in the path π which modifies ancestors of ui (excluding itself). This means also that ui
is not a node of Gni −1 , but is a node of Gni (introduced by the rule αni → αn0 i of P). Let ti
denote the subtree of Gni +1 rooted at the node ui . We have |ti | ≤ |αi0 | ≤ kPk. It is also easy
to see that ti →∗P t0i . A witnessing path is the sequence Gni +1 (ui ), . . . , Gm (ui ) (removing
duplicates). [Recall that T (u) denotes the subtree of T rooted at u.] Furthermore, the path
witnessing T1 →∗P C[t1 , . . . , tn ] can be obtained from π by removing each application of rulesthat operate on descendants of ui after Gni +1 (for each i ∈ [1, n]).
J
To prove Lemma 6, we use Lemma 8 starting with T1 = t ∈ Dom(P). ReachingC[t1 , . . . , tn ] requires a path of length exponential in kPk by Lemma 7. We now apply thesame reasoning again to ti →∗P t0i , for each i ∈ [1, n], and so build the path from C[t1 , . . . , tn ]to C[t01 , . . . , t0n ] in this fashion. Since each application of this reasoning can only modify
descendants of the root of T1 of at most exponential distance, the constructed path witnessingt →∗P T has local depth that is exponential in kPk, which completes the proof of Lemma 6.
A more detailed argument is given in the full version.
I Remark. Even for PDS, an exponential upper bound on the local depth of P is tight. It
is well-known that the shortest path from a configuration C to another configuration C 0 in
PDS can be exponential in the size of the PDS P (more precisely, in the number of states).
A witnessing PDS exhibiting this lower bound (e.g. see [21]) simply represents a number
with k bits in the stack in binary, and counts from 0 to 2k − 1. Since the least significant bit
has to be toggled 2k − 1 times, the local depth of the PDS also has 2k − 1 as the lower bound.

7

Future work

We mention two possible future avenues: (1) Can other interesting classes of infinite systems(e.g. PAD-processes [27] and order-2 collapsible pushdown automata [22]) be captured withinbounded local depth acceleration framework? (2) Improve the framework of bounded local
depth acceleration techniques so that the semi-algorithm has faster termination guarantee
for PA-processes, PDS, and GTRS. One technique that might also help the latter is thesimulation-based antichain technique for language inclusion proposed in [2].
Acknowledgements Many thanks to P. Abdulla for answering questions about [4], M. Hague
and anonymous reviewers for their comments, and EPSRC (H026878) for the support.

1
2
3
4
5

References
P. A. Abdulla, K. Cerans, B. Jonsson, and Y. K. Tsay. General decidability theorems forinfinite-state systems. In LICS, pages 313–321, 1996.
P. A. Abdulla, Y.-F. Chen, L. Holík, R. Mayr, and T. Vojnar. When simulation meetsantichains. In TACAS, pages 158–174, 2010.
P. A. Abdulla, N. B. Henda, G. Delzanno, F. Haziza, and A. Rezine. Parameterized treesystems. In FORTE, pages 69–83, 2008.
P. A. Abdulla, B. Jonsson, P. Mahata, and J. d’Orso. Regular tree model checking. In
CAV, pages 555–568, 2002.
P. A. Abdulla, B. Jonsson, M. Nilsson, and M. Saksena. A survey of regular model checking.
In CONCUR, pages 35–48, 2004.

11

12

Accelerating tree-automatic relations

6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

P. A. Abdulla, A. Legay, J. d’Orso, and A. Rezine. Tree regular model checking: A
simulation-based approach. J. Log. Algebr. Program., 69(1-2):93–121, 2006.
S. Bardin, A. Finkel, J. Leroux, and Ph. Schnoebelen. Flat acceleration in symbolic model
checking. In ATVA, pages 474–488, 2005.
A. Blumensath and E. Grädel. Finite presentations of infinite structures: Automata andinterpretations. Theory Comput. Syst., 37(6):641–674, 2004.
B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universitéde Liège, 1999.
B. Boigelot and F. Herbreteau. The power of hybrid acceleration. In CAV, pages 438–451,
2006.
B. Boigelot, A. Legay, and P. Wolper. Iterating transducers in the large (extended abstract).
In CAV, pages 223–235, 2003.
A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata:Application to model-checking. In CONCUR, pages 135–150, 1997.
A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract regular (tree) model
checking. STTT, 14(2):167–191, 2012.
A. Bouajjani and T. Touili. Widening techniques for regular tree model checking. To
appear in Int J Softw Tools Technol Transfer, (Published online: Aug. 2011).
D. Caucal. On the regular structure of prefix rewriting. In CAAP, pages 87–102, 1990.
H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, andM. Tommasi. Tree automata techniques and applications, 2007.
H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger
arithmetic. In CAV, pages 268–279, 1998.
D. Dams, Y. Lakhnech, and M. Steffen. Iterating transducers. J. Log. Algebr. Program.,
52-53:109–127, 2002.
M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In LICS,
pages 242–248, 1990.
S. Göller and A. W. Lin. Refining the process rewrite systems hierarchy via ground tree
rewrite systems. In CONCUR, pages 543–558, 2011.
M. Hague and A. W. Lin. Model checking recursive programs with numeric data types. In
CAV, pages 743–759, 2011.
A. Kartzow. Collapsible pushdown graphs of level 2 are tree-automatic. In STACS, pages
501–512, 2010.
A. W. Lin. Weakly synchronized ground tree rewriting. In MFCS, pages 630–642, 2012.
C. Löding. Infinite Graphs Generated by Tree Rewriting. PhD thesis, RWTH Aachen,
2003.
D. Lugiez and Ph. Schnoebelen. The regular viewpoint on PA-processes. Theor. Comput.
Sci., 274(1-2):89–115, 2002.
D. Lugiez and Ph. Schnoebelen. Decidable first-order transition logics for PA-processes.
Inf. Comput., 203(1):75–113, 2005.
R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, TU-Munich, 1998.
M. Nilsson. Regular Model Checking. PhD thesis, Uppsala Universitet, 2005.
A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD
thesis, LFCS, School of Informatics, University of Edinburgh, 2010.
A. W. To and Leonid Libkin. Recurrent reachability analysis in regular model checking.
In LPAR, pages 198–213, 2008.
I. Walukiewicz. Pushdown processes: Games and model-checking. Inf. Comput.,
164(2):234–263, 2001.