The Complexity of Verifying Ground Tree Rewrite
Systems
Stefan Göller

Anthony Widjaja Lin

Universität Bremen, Institut für Informatik

Oxford University Computing Laboratory

Abstract—Ground tree rewrite systems (GTRS) are an extension of pushdown systems with the ability to spawn newsubthreads that are hierarchically structured. In this paper, westudy the following problems over GTRS: (1) model checking
EF-logic, (2) weak bisimilarity checking against finite systems,and (3) strong bisimilarity checking against finite systems. Whilethey are all known to be decidable, we show that problems (1)and (2) have nonelementary complexity, whereas problem (3) isshown to be in coNEXP by finding a syntactic fragment of EF
whose model checking complexity is complete for PNEXP . The
same problems are studied over a more general but decidable
extension of GTRS called regular GTRS (RGTRS), where regularrewriting is allowed. Over RGTRS we show that all threeproblems have nonelementary complexity. We also apply ourtechniques to problems over PA-processes, a well-known classof infinite systems in Mayr’s PRS (Process Rewrite Systems)
hierarchy. For example, strong bisimilarity checking of PAprocesses against finite systems is shown to be in coNEXP,
yielding a first elementary upper bound for this problem.

I. I NTRODUCTION
Pushdown systems (PDS) are natural abstractions of sequential programs with unbounded recursions. The problems ofverifying pushdown systems have hitherto been well-studied(cf. [2], [25], [26]). In addition to recursions, concurrency is indisputably another feature that commonly arises in real-world
programs. Multithreading is often introduced by design, e.g.,
to achieve speedup or to make programming more convenient.
Ground tree rewrite systems (GTRS) (cf. [4], [8], [9],[14]), which were also studied under the name ground term
rewrite systems in the rewriting community, are an extensionof PDS with the ability to spawn new subthreads that are
hierarchically structured, which in turn may terminate andreturn some values to their parents. While the rules of a PDS
rewrite a prefix of a given word, the rules of a GTRS rewrite
a subtree of a given tree. The decidability status for many
standard verification (i.e. model checking and equivalence
checking) problems over GTRS is well-known. For example,
reachability, recurrent reachability, and fair termination are
decidable (cf. [4], [7], [14], [22]). Moreover, model checking
first-order logic with reachability predicates is decidable [9],which implies the decidability of model checking the common
fragment of Computation Tree Logic (CTL) known as EFlogic. In turn, by a reduction to EF-logic (as shown in [11]),
we also obtain the decidability of the problems of weak/strong
bisimilarity checking against finite systems over GTRS. In
fact, most of these decidability results are known to holdfor regular GTRS (RGTRS) [14], which are a well-known

extension of GTRS with more general rewrite rules that are
given by tree automata1. On the negative side, it is known thatmost linear-time and branching-time logics — such as LTL
and CTL — have undecidable model checking problems over
GTRS (cf. [14], [24]). This is in stark contrast with pushdown
systems, over which model checking monadic second-orderlogic is still decidable [17].
The precise complexities of some verification problems
over GTRS and extensions thereof are also known. For example, reachability and recurrent reachability are polynomial
time solvable even for RGTRS (cf. [14]). In contrast, model
checking first-order logic with reachability predicates over
GTRS has nonelementary complexity [21] since the infinite
binary tree with a descendant can be easily generated by afixed GTRS (in fact, by a one-state pushdown system). The
precise complexity of EF-logic model checking over GTRS
(and extensions thereof) was stated as an open question in [14].
The best known upper bound is currently nonelementary, while
the best known lower bound is only PSPACE (which holds
already for pushdown systems [2], [26]). Likewise, for the
problems of strong/weak bisimilarity checking against finite
systems over GTRS (and RGTRS), the best known upperbound is nonelementary, while the best known lower boundis only PSPACE (which holds already for pushdown systems[13], [20]). Interestingly, the same nonelementary gaps arealso currently present (cf. [20]) when these three problems are
considered over similar infinite-state models like PA and PAD
processes, which are well-known classes of infinite systems inMayr’s PRS (Process Rewrite Systems) hierarchy (cf. [16]).
Note that these three problems are only PSPACE-complete
over pushdown systems (cf. [2], [13], [20], [26]).
Contributions. We investigate the following verification problems over GTRS (and the extension RGTRS): (1) model
checking EF-logic, (2) weak bisimilarity checking against
finite systems, and (3) strong bisimilarity checking against
finite systems. Such problems are arguably the most basic
verification problems over infinite-state systems, especially inthe concurrent setting (cf. [16]). Our main contribution is to
pinpoint the complexity of these problems.
The starting point of our paper is a proof that EF-logic
model checking over GTRS has a nonelementary complexity,
already when considering EF formulas with two occurrences
1 This extension is analogous to how prefix-recognizable systems [5] extend
PDS.

of EF operators that are nested. This shows that the existing
automata-based algorithms for the problem (cf. [7], [9], [14])are in some sense optimal answering Löding’s open question[14]. The lower bound proof is achieved by an exponential reduction from the decidable first-order theory over finite words,
which is well-known to have a nonelementary complexity [21].
With the same arguments one can also show that HennesyMilner logic (i.e. the fragment with no EF operators) suffice
to show the nonelementary lower bound over the more generalclass of RGTRS.
We then proceed to look at the fragment EF1 of EF-logic
consisting of formulas with EF operator nesting depth at mostone (i.e. in the parse tree of the formula, every branch has
at most one occurence of the operator EF). This fragment
is interesting for two reasons. Firstly, as mentioned above,
our proof of the nonelementary lower bound for problem (1)over GTRS requires precisely two nested occurrences of EF
operators. Secondly, there is a polynomial time reduction fromproblem (3) to the problem of model checking EF1 formulas
over GTRS if the formulas are represented as DAGs, which
are single-exponentially more succinct than the standard tree
representation of formulas. Our result is that the problem
of model checking EF1 over GTRS is PNEXP -complete (i.e.
within the second level of the exponential hierarchy). This
result cannot be obtained by simply applying the existing
automata-based algorithms for EF-logic model checking (cf.
[7], [9], [14]). Moreover, a further analysis of our proof showsthat problem (3) is solvable in coNEXP. This has substantiallyclosed the nonelementary gap with the best known lower
bound for the problem, which is PSPACE. In fact, these proof
techniques can be easily applied to derive better upper/lower
bounds for verification problems PA-processes: (1) strong
bisimilarity checking of PA-processes against finite systems issolvable in coNEXP giving the first elementary upper boundfor this problem (cf. [20]), and (2) model checking EF-logic
over PA-processes is PNEXP -hard improving the best known
lower bound of PSPACE for the problem (cf. [16]).
We then consider two natural extensions of the problem ofchecking strong bisimilarity against finite systems over GTRS:(i) checking strong bisimilarity against finite systems over the
more general class RGTRS, and (ii) checking weak bisimilarity against finite systems over GTRS. In contrast, it turns outthat both of these extensions have a nonelementary complexity.
These results are the most technically involved in this paperwith the lower bound proof of problem (ii) building upon thelower bound proof of problem (i). Bisimilarity checking has
a standard interpretation as a game between two players (cf.
[13]) called Attacker (who aims to show non-bisimilarity) and
Defender (who aims to show bisimilarity). The difficulty ofproving a complexity lower bound for bisimilarity checking
problem is due to the asymmetry between the power ofAttacker and Defender (Attacker is often more powerful) insuch games. Known lower bound techniques for bisimilarity
checking, a.k.a. “Defender’s forcing”, are often implemented
by the help of finite control unit, which many infinite-statemodels have (e.g. PDS and Petri nets). The difficulty of pro-viding Defender’s forcing techniques in the absence of finite
control unit is witnessed by the plethora of open problems
concerning decidability/complexity of equivalence checking
over infinite-state models like PA and PAD processes (cf. [20]).
The lack of global finite control unit often means that Defender
does not have an immediate way of punishing Attacker (i.e.
forcing him not to do something bad). In the case of GTRSor RGTRS, this means that at any given time Attacker may
replace any of (potentially unbounded number of) the subtreesthat are present in the current configuration (i.e. a tree). In
this paper, we provide the first methods for implementing
Defender’s forcing technique over infinite-state models thatlack finite-control unit resulting in strong (i.e. nonelementary)lower bounds.
Our results for (R)GTRS are summarized in Table I.
Related work. Other related problems over GTRS have beenshown to be decidable: confluence (cf. [8]), model checking
fragments of LTL [23], and generalized recurrent reachability[24].
Several other extensions of PDS with multithreading capabilities have been considered in [3], [12], [16], [19]. Amongthese extensions, the class of process rewrite systems [16],which generalize both Petri nets and pushdown systems byproviding hierarchical structures to threads, seem to have tightconnections with GTRS. It is interesting to note that there isalso a nonelementary gap between the best known upper/lower
bounds for EF-logic model checking and strong/weak bisimilarity checking against finite systems over two proper subclasses of process rewrite systems known as PA-processes and
PAD-processes (cf. [15], [16], [20]). PA-processes have also
been shown to be a good abstraction of parallel programs forthe purpose of interprocedural data-flow analysis (cf. [10]).
Organization. Section II contains preliminaries. In Section
III, we analyze the complexity of model checking EF-logic(and its fragments). We prove a nonelementary lower boundfor strong bisimilarity checking against finite systems in Section IV. Results concerning weak bisimilarity checking against
finite systems for GTRS are discussed in Section V. Section
V depends on Section IV which in turn depends on Section
III-A.
For detailed proofs and applications to PA-processes, see
our technical report.
II. P RELIMINARIESFor each i, j ∈ Z, we denote by [i, j] the interval {i, i +1, . . . , j − 1, j}. Throughout the rest of this paper, we fix acountable set of action labels Act. For a set X let 2X denotethe powerset of X.
Complexity theory: The following complexity classes will
be of relevance: P, AP S= PSPACE, NEXP, coNEXP, kEXP, ELEMENTARY = k k-EXP. The class PNEXP denotes
deterministic polynomial time with oracle access to NEXP.
It is in the second level of exponential hierarchy, which isin EXPSPACE. Unless stated otherwise reductions are always

Model checking

GTRS

EF0

PSPACE-complete

EF1

PNEXP -complete

EFk, k≥2

NONELEMENTARY

Bisimilarity
against finite
systems

GTRS∼

PSPACE · · · coNEXP

≈

RGTRS

RGTRS

NONELEMENTARYTABLE IOVERVIEW OF OUR RESULTS

polynomial time many-to-one reductions. We define the tower
function TOWER : N → N as TOWER(0) = 1 and
TOWER(n + 1) = 2TOWER(n) for each n ∈ N.
First-order logic over words: A (binary) word is a finite
sequence a1 a2 . . . an , where ai ∈ {0, 1} for each i ∈ [1, n] that
we also identify with the logical structure w = (U, P0 , P1 , <),where U = [1, n] is the universe, unary predicates Pa = {i ∈[1, n] | ai = a} for each a ∈ {0, 1} and the binary predicate<. By a result of Stockmeyer the first-order theory over words
is nonelementary [21]. We assume in this paper that first-orderformulas are given in prenex normal form.
Transition systems and EF logic: A transition system isaa tuple S = (C, A, {−→| a ∈ A}), where C is a setof configurations, A ⊆ Act is some finite set of actions,aand −→⊆ C × C is a set of transitions for each actiona ∈ A. Let us fix a subset Σ ⊆ A of S’s actions. BySaΣ−→ we abbreviate a∈Σ −→. We prefer to use the infixaanotation c −→ d instead of (c, d) ∈−→. Similar remarks
Σapply to −→. We say that S is finite in case C is finite – weoften use the notation F to refer to finite transition systems.
Formulas of EF-logic are given by the following grammar,
where Σ ⊆ A: ϕ ::= true | ¬ϕ | ϕ ∧ ϕ | hΣiϕ | hΣ∗ iϕ. We
introduce the usual abbreviations false = ¬true, ϕ1 ∨ ϕ2 =¬(¬ϕ1 ∧ ¬ϕ2 ), [Σ]ϕ = ¬hΣi¬ϕ, and [Σ∗ ]ϕ = ¬hΣ∗ i¬ϕ.
We note that all of our lower bound proofs also hold for the
more restricted version of EF logic where each occurenceof the operator hΣ∗ i satisfies Σ = A. For each transitionasystem S = (C, A, {−→| a ∈ A}) and each EF-formula ϕdefine the set of all configurations [[ϕ]]S ⊆ C that satisfy
ϕ by induction on the structure of ϕ as [[true]]S = C,[[¬ϕ]]S = C \ [[ϕ]]S , [[ϕ1 ∧ ϕ2 ]]S = [[ϕ1 ]]S ∩ [[ϕ2 ]]S ,Σ[[hΣiϕ]]S = {c ∈ C | ∃d ∈ [[ϕ]]S : c −→ d}, [[hΣ∗ iϕ]]S =∗Σ{c ∈ C | ∃d ∈ [[ϕ]]S : c −→ d}. We write (S, c) |= ϕwhenever c ∈ [[ϕ]]S . The EF nesting depth nd(ϕ) of an EFformula ϕ is inductively defined as follows: nd(true) = 0,nd(¬ϕ) = nd(ϕ), nd(ϕ1 ∧ ϕ2 ) = max{nd(ϕ1 ), nd(ϕ2 )},nd(hΣiϕ) = nd(ϕ), nd (hΣ∗ i ϕ) = nd(ϕ) + 1. For each i ≥ 0,
we denote by EFi the syntactic fragment of EF restricted toformulas of EF nesting depth at most i. We remark that EF0
is Henessy-Milner logic (HM).
aStrong bisimulation equivalence: Let S1 = (C1 , A, {−→1 |aa ∈ A}) and S2 = (C2 , A, {−→2 | a ∈ A}) be twotransition systems over a common set of actions A. A relation
R ⊆ C1 × C2 is a strong bisimulation if for each (c1 , c2 ) ∈ R
the following two conditions hold for each a ∈ A: (1) foraaevery c1 −→1 c′1 there is some c2 −→2 c′2 with (c′1 , c′2 ) ∈ Raa′
and (2) for every c2 −→2 c2 there is some c1 −→1 c′1′′with (c1 , c2 ) ∈ R. We say that c1 is strongly bisimilar toc2 (abbreviated by c1 ∼ c2 ) whenever there is a strong
bisimulation R such that (c1 , c2 ) ∈ R.
Weak bisimulation equivalence: Let us fix a silent action τ 6∈aA and let Aτ = A ∪ {τ }. Moreover let S1 = (C1 , Aτ , {−→1 |aa ∈ Aτ }) and S2 = (C2 , Aτ , {−→2 | a ∈ Aτ }) be twotransition systems over the common alphabet Aτ . We define
τ
τ
a
τ
a
the binary relations =⇒i = (−→i )∗ and =⇒i = (−→i )∗ ◦ −→iτ∗◦(−→i ) for each a ∈ A and for each i ∈ {1, 2}. A binary
relation R ⊆ C1 × C2 is a weak bisimulation if for each(c1 , c2 ) ∈ R the following two conditions hold for eachaaa ∈ Aτ : (1) for every c1 −→1 c′1 there is some c2 =⇒2 c′2a′′′with (c1 , c2 ) ∈ R and (2) for every c2 −→2 c2 there is someac1 =⇒1 c′1 with (c′1 , c′2 ) ∈ R. We say that c1 is weakly
bisimilar to c2 (abbreviated by c1 ≈ c2 ) whenever there is aweak bisimulation R such that (c1 , c2 ) ∈ R. In the appendix
we describe how bisimilarity corresponds to a game between
Attacker and Defender.
Ranked trees: Let  denote the prefix order on N∗ , i.e. x  yfor x, y ∈ N∗ if there is some z ∈ N∗ such that y = xz, andx ≺ y if x  y and x 6= y. A ranked alphabet is a collectionof pairwise disjoint finite alphabets A =S (Ai )i∈[k] for somek ≥ 0. For simplicity we identify A with i∈[k] Ai . A (ranked)
tree (over the ranked alphabet A) is a mapping T : DT → A,
where for DT ⊆ [1, k]∗ we have (1) DT is nonempty, finite
and prefix-closed and (2) for each x ∈ DT with T (x) ∈ Ai
we have x1, . . . , xi ∈ DT and xj 6∈ DT for each j > i.
We say that DT is the domain of T – we call these elements
nodes. A leaf is a node x with T (x) ∈ A0 . We also referto ε ∈ DT as the root of T . By TreesA we denote the setof all ranked trees over the alphabet A. Let T be a ranked
tree and let x be a node of T . We define xDT = {xy ∈[1, k]∗ | y ∈ DT } and x−1 DT = {y ∈ [1, k]∗ | xy ∈ DT }.
By T ↓x we denote the subtree of T with root x, i.e. the treewith domain DT ↓x = x−1 DT defined as T ↓x (y) = T (xy).
Let S, T ∈ TreesA and let x be a node of T . We define
T [x/S] to be the tree that is obtained by replacing T ↓x in
T by S, more formally DT [x/S] = (DT \ xDT ↓x ) ∪ xDS
with T [x/S](y) = T (y) if y ∈ DT \ xDT ↓x and S(z) if
y = xz with z ∈ DS . Define |T | as the number of nodes in atree T . We also use the notation t to refer to ranked trees, inparticular subtrees.
Regular tree languages: A nondeterministic (bottom-up) tree
automaton (NTA) is a tuple A = (Q, F, A, ∆), where Q is afinite set of states, F ⊆ Q is a set of
S final states, A = (Ai )i∈[k]
is a ranked alphabet, and ∆ ⊆ i∈[k] Qi × Ai × Q is thetransition relation. By L(A) = {T ∈ TreesA | there is anaccepting run of A on T }. A set of trees S ⊆ TreesA is≤nregular if S = L(A) for some NTA A. By TreesA= {T ∈
TreesA : |T | ≤ n} we denote the set of all trees over A withat most n nodes.
(Regular) ground tree rewriting systems: A regular groundtree rewriting system (RGTRS) is a tuple R = (A, A, R),
where A is a ranked alphabet, A ⊆ Act is finite set of actions,aand R is finite set of rewriting rules of the form L ֒→ L′ ,where L and L′ are regular tree languages given as NTA. A
ground tree rewriting system (GTRS) is an RGTRS such thateach regular tree language is singleton (given explictly). Theatransition system of R is S(R) = (TreesA , A, {−→| a ∈ A}),a′where for each a ∈ A, we have T −→ T if and only if there isasome x ∈ DT and some rule L ֒→ L′ ∈ R such that T ↓x = S′′
and T = T [x/S ] for some S ∈ L and some S ′ ∈ L′ .
Decision problems: In this paper we will be interested in thefollowing decision problems.
EF model checking asks, given a (R)GTRS R = (A, A, R), a
T ∈ TreesA and an EF-formula ϕ, to decide if (S(R), T ) |= ϕholds? The analogous question can be asked for the syntactic fragments EFi of EF. EF model checking of RGTRS
is proven to be decidable in time TOWER(O(n)) in [14].
Strong Bisimilarity Checking against Finite Systems asks,
given a (R)GTRS R = (A, A, R), T ∈ TreesA , a finiteaF = (C, A, {−→| a ∈ A}) and a configuration c ∈ C, todecide if T ∼ c holds. Weak Bisimilarity Checking against
Finite Systems asks, given a (R)GTRS R = (A, Aτ , R),a
T ∈ TreesA , a finite F = (C, Aτ , {−→| a ∈ Aτ }) and aconfiguration c ∈ C, to decide if T ≈ c holds.
By a result from [11] (see also Theorem 1 and Corollary
1 of [13]) weak bisimilarity checking against finite systems
is polynomial time reducible to model checking EF logic,
where formulas are given in DAG representation. Analogously,
strong bisimilarity can be reduced in polynomial time to model
checking formulas of the kind ϕ1 ∧ [A∗ ]ϕ2 , where ϕ1 , ϕ2 are
EF0 formulas in DAG representation.
III. M ODEL C HECKING
A. EF2 (resp. EF0 ) is nonelementary over GTRS (resp.
RGTRS)
Our first result is that model checking EF2 over GTRS has
nonelementary complexity, which answers the open question
by Löding [14].
Theorem 1. Model checking EF2 over GTRS is nonelementary.
This proof of this theorem can easily be adapted to showthat model checking EF0 over RGTRS has nonelementarycomplexity. This lower bound proof is achieved by an exponential reduction from the decidable first-order theory overfinite words, which is well-known to have a nonelementarycomplexity [21]. Roughly speaking, we design our GTRS insuch a way that in the first phase it reaches from an input treea huge tree whose yield (a.k.a. frontier) we interpret as a word,
which will correspond to a word that witnesses satisfiabilityof an input first-order formula over finite words. This canbe realized by the first occurrence of the EF operator in the
input formula. In a second phase we mimic the assignmentof variables of the first-order sentence by labeling leaves
appropriately. In the third and final phase, we check via adeterministic bottom-up tree automaton whether the huge tree
(whose leaves are now labeled with variables of the first-ordersentence) satisfies the remaining unquantified subformula. Thiscan be realized by the second occurrence of the EF operator.
Let us now proceed with the proof. Fix afirst-order sentence over binary words ψ=∃x1 ∀x2 . . . ∃x2n−1 ∀x2n ϕ(x1 , . . . , x2n ). Without lossof generality we will assume w 6|= ψ for each binary word
w with |w| < 2. Our goal is to compute in exponential timea GTRS R = (A, A, R), some initial tree start ∈ TreesA ,and an EF2 -formula θ such that ∃w ∈ {0, 1}∗ : w |= ϕ iff
start |= θ.
We define our set of actions as A = {ai | i ∈ [1, 2n]} ∪{down, up0 , up1 , up2 } and let P = ( 2[1,2n] ∪ {⊥} × {0, 1}
denote the set of proper leaf labels. The first component label⊥ will not be relevant in this but in subsequent sections. We
define the ranked alphabet A = (Ai )i∈{0,1,2} of R as follows,
where the set Q will be defined later: A0 = {start} ∪ P ∪ Q,
A1 = {root} and A2 = {⋆}.
The regular tree language Combs consists of precisely those
trees T ∈ TreesA such that (1) T −1 (root) = {ε}, i.e. the (oneand) only node of T that is labeled with root is the root ofT , (2) for each leaf x of T we have T (x) ∈ P , (3) for each
inner node x 6= ε of T we have that T (x) = ⋆ and that x
has a left child that is a leaf, and finally (4) there is at least
one inner node x (with T (x) = ⋆) that is the child of ε. For
each I ⊆ [1, 2n] define the regular tree language CombsI to
consist of precisely those combs T ∈ Combs such that (1)for each leaf x of T we have T (x) ∈ 2I × {0, 1} and (2) for
each two distinct leaves x, x′ of T with T (x) = (J, α)
S and
T (x′ ) = (J ′ , α′ ) we have J ∩ J ′ = ∅ and (3) I = {J |x is a leaf of T and T (x) = (J, α)}.
Let us give an example for a tree in Combs{2,3,5,7} :root⋆(∅, 0)⋆({2, 5}, 1)⋆({3}, 1)⋆(∅, 0)({7}, 1)
Intuitively, think of the sequence of the second componentsof leaf labels of T ∈ CombsI (i.e. the second-component
projection of the labels of the yield of T ) to correspond toa binary word, and moreover, for each leaf x of T , thinkof the first component of T (x) to correspond to the index
set of variables {x1 , . . . , xn } of ϕ that have been bound tothe corresponding position in the word. Hence every comb
in CombsI corresponds to a unique binary word along witha variable valuation with domain I. By Combsϕ denote thetrees from Combs[1,2n] whose word and variable assignment
interpretation satisfies ϕ.
The following three rewriting rules allow to reach all membersof Combs∅ from the singleton tree start, where α ∈ {0, 1}:
down

root
⋆

start ֒→(∅, α)

down

⋆

⋆ ֒→
(∅, α)⋆down⋆⋆ ֒→ (∅, α)

Next, we add the following rules that allows to rewrite theleafs of combs (this rewriting will correspond to assigningvariables to the leaves), where α ∈ {0, 1} and I ⊆ [1, 2n]:aihI, αi ֒→ hI ∪ {i}, αi for each i ∈ [1, 2n] \ I.
In a next step, we compute in exponential time in |ψ| a nondeterministic tree automaton A = (Q, F, A, ∆) that accepts
Combsϕ . We add the state set Q to A0 of our GTRS R.
Then we add the following rewriting rules to R (which willrealize the bottom-up computation of A): (1) for each rule(q, q ′ , a, q ′′ ) ∈ ∆ ∩ Q2 × A2 × Q we add the rewriting ruleup2a(q, q ′ ) ֒→ q ′′ , (2) for each rule (a, q ′ ) ∈ ∆ ∩ (A0 × Q)
up0
we add the rewriting rule a −→q ′ , and (3) for each rule′(q, root, q ) ∈ ∆ ∩ (Q × {root} × Q) where q ′ ∈ F we add
up1
the rewriting rule root(q ′ ) −→root.
Finally we define θ as
hdown∗ i ha1 i[a2 ] · · · ha2n−1 i[a2n ] {up0 , up2 }∗ hup1 i true.
One can easily check that ∃w ∈ {0, 1}∗ : w |= ψ iff(S(R), start) |= θ which concludes the proof.
B. Model checking EF1 over GTRS is complete for PNEXPOur nonelementary lower bound proof above uses nested
occurences of two EF operators. Our main result now isthat prohibitting nested occurences of EF operators yields anelementary model checking complexity.
Theorem 2. Over GTRS model checking formulas hΣ∗ iϕ withΣ ⊆ A and ϕ ∈ EF0 is in NEXP.
Before sketching a proof of this theorem, we mention thefollowing corollary, which can be easily derived by (1) establishing a polynomial space procedure using NEXP oracles(invoked whenever subformulas of the form hΣ∗ iψ are seen),and (2) using the fact that PSPACENEXP = PNEXP [1].
Corollary 3. Model checking EF1 over GTRSs is in PNEXP .
We now sketch the proof of Theorem 2. Let us now supposethat hΣ∗ iϕ is the given formula, R = (A, A, R) is the given
GTRS, and T0 ∈ TreesA is the input tree. We wish to check
whether (S(R), T0 ) |= hΣ∗ iϕ. Let us compute in polynomial∗
time (cf. [14]) an NTA A that recognizes the set postΣR (T0 ) ofconfigurations of R reachable from T0 by applications of ruleswith labels from Σ. It now suffices to show how to compute
NTAs that recognize [[ϕ]]S(R) . We do not use the standard

automata construction (e.g. [14]) for the set of trees satisfying
a given EF0 formula with respect to a given GTRS since it
suffers from a nonelementary blow-up. Given an EF0 formula,
let mrank(ϕ) be the modality rank of ϕ, i.e., the maximum
nesting depth of h·i operators in ϕ.
We now show that [[ϕ]]S(R) can be expressed as a unionof regular tree languages, each of which can be expressed bya tree automaton Ai of singly-exponential size. Furthermore,
we can check whether some L(Ai ) intersects with L(A) in
nondeterministic time exponential in |ϕ| and |R|.
S
Lemma 4. We have [[ϕ]]S(R) = i∈I L(Ai ), for a family{Ai }i∈I , where |Ai | = exp(|ϕ|, |R|). One can nondeterministically check whether L(A) intersects with some L(Ai ) intime exp(|ϕ|, |R|).
As we shall see in our proof below, the parameter |ϕ|in the above lemma can be replaced by mrank(ϕ). As acorollary, this yields the same NEXP upper bound for themodel checking problem when ϕ is given as a DAG.
We now give a proof of Lemma 4. Let r = mrank(ϕ). We
start by defining a standard equivalence relation on TreesA
based on the modality rank of EF0 formulas: given two trees
T, T ′ ∈ TreesA and i ∈ N, write T ≃i T ′ if for every
EF0 formula ψ with mrank(ψ) ≤ i: (S(R), T ) |= ψ iff(S(R), T ′ ) |= ψ. In other words, T ≃i T ′ iff T and T ′ agree
on every formula ψ with modality rank at most i. It is obviousthat ≃i is an equivalence relation and that T ≃i+1 T ′ implies
T ≃i T ′ . Furthermore, it is well-known that the equivalence
relation ≃i is of finite index, i.e., the number of equivalenceclasses of ≃i is finite. For each equivalence class C of ≃r ,it is clear that either (S(R), T ) |= ϕ for all T ∈ C, or
S(R), T 6|= ϕ for all T ∈ C. For the former case, we say thatthe equivalence class C is positive; otherwise, it is negative.
Therefore, one idea is to define the family {Ai }i∈I of NTAs
by associating an NTA for each positive equivalence class Cof ≃r . Two problems with this approach, however, are: (1)this does not give a good way of computing an NTA for eachpositive equivalence class, and (2) this does not reveal an upperbound on the index of ≃r .
We now define a finer relation ≡i (for each i ∈ N) thatwill give extra information which will help us solve thesetwo problems. To this end, let K be the maximum number ofnodes in the tree appearing in any rewrite rule in R. Also, let
Ni = i · K. Given any two trees T, T ′ ∈ TreesA , we define
T ≡i T ′ iff for each tree t ∈ TreesA either of the following
is true: (i) the number of times t appears as a subtree of T
equals the number of times t appears as a subtree of T ′ , and(ii) the number of times t appears as a subtree exceeds Ni
both for T and T ′ . In other words, T ≡i T ′ iff each subtreewith at most Ni nodes appears in T and T ′ the same numberof times (up to some threshold). As before, it is easy to checkthat ≡i is an equivalence relation and that T ≡i+1 T ′ implies
T ≡i T ′ . To complete the proof of Lemma 4, we proceed
as follows: (1) show that ≡i is finer than ≃i , (2) checkingi→ [0, Ni ] actually describes
whether a function f : Trees≤NA
an equivalence class of ≡i can be done rather efficiently, (3)testing whether an equivalence class of ≡i is positive (withrespect to ϕ) can be done rather efficiently, and (4) for eachpositive equivalence class C of ≡i , an NTA AC recognizing
C can be computed rather efficiently. As we will see, thesewill imply Lemma 4. For step (1) the following lemma canbe shown.
Lemma 5. For each tree T, T ′ ∈ TreesA , it is the case thatT ≡i T ′ implies T ≃i T ′ .
Intuitively, this lemma holds since satisfaction of EF0 formulas of modality rank i is only affected by the number ofoccurences of trees of depth Ni (up to some threshold).
Let us now proceed to step (2). Recall that each equivalence class C of ≡r can be described by a function fromr
→ [0, Nr ]. The converse, however, is false,fC : Trees≤NAe.g., it is impossible to have a class C with fC (T ) > 1 for atree T with two nodes but fC (T ′ ) = 0 for all trees T ′ with
one node. Also note that the special case where f (T ) = 0r
is impossible for an equivalence classfor all T ∈ Trees≤NA
since trees have nonempty domain by definition. Therefore,
we need to be able to check whether a given functionr→ [0, Nr ] actually describes an equivalence
f : Trees≤N
A
class in ≡r . To this end, recall first that any function f that
describes an equivalence class of ≡r counts each subtree ofrwith fC (T ) > 0, i.e., if t is a subtree oftrees T in Trees≤NA
T , then t contributes to the value of f (t). We will first define ar→ [0, Nr ] that avoids this “double
new function g : Trees≤NA
counting”. This can be done by the following algorithm: “Setr
and repeat the following forg(T ) := 0 for all T ∈ Trees≤NA≤Nrwith f (T ) > 0 (ordered by the number
each T ∈ TreesAof nodes, starting from the largest): (1) Let f (T ) := f (T ) − 1,(2) g(T ) := g(T ) + 1, (3) Go through all nodes u of T
(except when u is the root of T ) and substract f (T ↓u ) by 1
(if becomes negative, then terminate abruptly)”. Observe that
if this algorithm terminates abruptly, then f does not actuallydescribe an equivalence class of C. Furthermore, the algorithm
runs in time exponential in r ≤ |ϕ| and |R| simply becauser| = exp(r, |R|) can be shown. . Now, suppose that
|Trees≤NA
the function g has been successfully computed from the givenfunction f . This implies that g describes a forest F with eachroccurring g(T ) many times. The originaltree T ∈ Trees≤NA
function f then describes an equivalence class iff such a forest
can be further “connected into a big tree”. This last check canbe done using the following lemma.
r→ [0, Nr ] deLemma 6. The function f : Trees≤NA
scribes an equivalence class in ≡r iff the function g :≤Nr→ [0, Nr ] (and the forest F corresponding to it)
TreesAcan be successfully computed from f by the above algorithm
andP conditions are satisfied: (1)P that one of the following≤Nr g(T ) = 1. (2)r g(T ) > 1, and forT ∈Trees≤N
T ∈TreesAA
some letter a with some rank h ∈ N and some trees T1 , . . . , Th
occuring in the forest F , the tree a(T1 , . . . , Th ) has more thanNr nodes.

Observe that this lemma completes step (2) since this test
can be performed in time exponential in r and |R| and polyno-

mial in |f |. We now proceed to step (3). This step is rather easy
since checking whether an equivalence class C of ≡r describedr→ [0, Nr ] is positive can be done
by a function fC : Trees≤NAin time exponential in r and |R|. Intuitively, the idea is topick a representative T of C of exponential size and computea finite transition system consisting of the neighborhood of T
up to depth r. It turns out that the finite system also has size
exponential in r ≤ |ϕ| and |R|. Therefore, we may use thestandard linear-time algorithm for model checking HenessyMilner (i.e. EF0 ) formulas over finite systems.
We now proceed to step (4), which is the final step. For
this, we need to show how to compute an NTA recognizing
an equivalence class C of ≡r described by a function fC :r
→ [0, Nr ].
Trees≤NAr→ [0, Nr ] that
Lemma 7. Given a function f : Trees≤NA
witnesses an equivalence class C of ≡r , we can compute an
NTA recognizing precisely C in time |f |poly(r,|R|) · exp(r, |R|).

Roughly speaking, this lemma can be proven as follows.
r→ [0, Nr ] using theFirst, compute the function g : Trees≤NA
above algorithm, which avoids double counting of subtrees.
rsuch that g(t) = Nr .
Let U denote all trees t ∈ Trees≤NAr
Let t1 , . . . , tm be an enumeration of all trees t ∈ Trees≤NA
with g(t) > 0 without counting multiplicities. One can now
design an NTA that counts that precisely g(ti ) many nodes v
occur such that the subtree rooted at v equals ti , and that anarbitrary number of nodes v can occur such that the subtree
rooted at v is a tree in U . It is easy to see that such an NTA
of size exponential in r and |R| can be computed.
To summarize, the proof of Lemma 4 can now be done asfollows. The NTAs Ai in the statement of Lemma 4 will correspond to positive equivalence classes C described by somer
→ [0, Nr ]. Using the last step above,
functions fC : Trees≤NA
the NTA Ai can be computed in time exponential in r and |R|
if f is given as an input. Checking whether L(A)∩L(Ai ) 6= ∅for some i requires us to nondeterministically guess one suchfunction f , check whether it describes an equivalence class,compute the NTA Ai corresponding to it, and check for
language intersection with A in the standard way.
Let us discuss the ideas of a matching lower bound for EF1 .
Lemma 8. Over GTRS model checking formulas hA∗ iϕ,where ϕ ∈ EF0 , is NEXP-hard.
Proof sketch. The reduction is from the 2n × 2n tilingA ∗problem [18]. The idea is to reach via −→ some binary
tree with superleafs, where a superleaf is a tree of depth
one whose root has arity 2n. Each child of a superleaf will
either have a nullary symbol b0 or b1 , where the root of asuperleaf contains a tile type. Each superleaf corresponds toa grid element (i, j) ∈ [0, 2n − 1] × [0, 2n − 1] where thenullary symbols of the first n (resp. last n) children encode i(resp. j) in binary. The formula ϕ is now a conjunction of EF0
formulas expressing the following: (1) A superleaf for (0, 0)
exists, (2) whenever there are two superleafs corresponding to
the same (i, j) then their tile types are the same, (3) if there

is a superleaf for (i, j) with i < 2n − 1 (resp. j < 2n − 1),then there is a superleaf for (i + 1, j) (resp. (i, j + 1)), andfinally (4) the horizontal and vertical tile conditions hold forevery superleaf.
⊓⊔
By encoding circuit value into nodes of trees (gates andits evaluations will be represented in nodes in the tree) andinvoking a subroutine to the trees that realized the domino
problem one can prove a matching lower bound for EF1 .
Theorem 9. Over GTRS model checking EF1 is hard for
PNEXP .
Remark. PNEXP -completeness for EF1 model checking over
PA-processes (cf. [16]) can be shown using the same techniques; see the technical report for a sketch.
IV. S TRONG BISIMILARITY AGAINST FINITE SYSTEMS
Since strong bisimilarity checking can be reduced to EFmodel checking, the following theorem is known.
Theorem 10 ([14], [11]). Strong bisimilarity checkingof RGTRS against finite systems is decidable in time
TOWER(O(n)).
Over GTRS, however, we obtain an elementary upper bound. It
can be derived via a reduction to model checking formulas of
the kind ϕ1 ∧[A∗ ]ϕ2 where ϕ1 and ϕ2 are EF0 DAG-formulas
and then applying our upper bound result from Theorem 2. [Bythe above remark, this technique can also be used to prove a
coNEXP upper bound for the same problem over PA-processes(cf. [20]).]
Theorem 11. Strong bisimilarity checking of GTRS against
finite systems is in coNEXP.
As a main result of this section we prove that strong
bisimilarity between a regular ground tree rewrite system anda finite system has nonelementary complexity.
Theorem 12. Strong bisimilarity checking of RGTRS against
finite systems is nonelementary.
Although the proof also goes via an exponential reduction
from the first-order theory over finite words, due to the lack offinite control unit in (R)GTRS it is not merely an adaptationof the proof of the nonelementary lower bound for EF2 model
checking over GTRS from the previous section. Roughly
speaking, we implement Defender’s forcing technique by
providing rewriting rules of the form L ֒→ T , where L isa regular tree language and T is an explicit ranked tree. Suchrules will allow Defender to punish Attacker in case he did
not play in a way that corresponds to evaluating the first-ordersentence on the huge tree. However, the biggest obstacle wehave to overcome is the possibility of Attacker assigning an
arbitrary permutation of the variables in the input first-ordersentence to leaves of the tree.
Let us proceed to the proof of Theorem 12. We reuse someof the notation that was introduced in Section III-A. Again, let
us fix a first-order sentence interpreted over binary words ψ =∃x1 ∀x2 . . . ∃x2n−1 ∀x2n ϕ(x1 , . . . , ϕ2n ) and let us assume

again w 6|= ψ for each binary word w with |w| < 2. Our goal
is to compute in exponential time a RGTRS R = (A, A, R),some initial tree start ∈ TreesA , some finite transition systema
F = (C, A, {−→F | a ∈ A}), and a configuration s∅ ∈ C suchthat there is some w ∈ {0, 1}∗ with w |= ψ iff start 6∼ s∅ . We
call a subset I ⊆ [1, 2n] game-conform if I = [1, k] for somek ∈ [0, 2n] and non-game-conform otherwise. Analogously,
we call a comb T ∈ CombsI game-conform (resp. non-gameconform) if I is game-conform (resp. non-game-conform).
Each game-conform comb T ∈ Combs[1,k] naturally induces avaluation νT of variables with indices from [1, k] to positionsof the yield string defined by T . Let ϕ[νT ] denote the formulathat is obtained from ϕ by replacing the information given byνT . This can be extended to define ψ[νT ]. Hence, e.g. ψ[νT ]is of the form ∃xk+1 · · · ∀x2n ϕ[νT ] in case k is even.
In case I ⊂ [1, 2n] and i ∈ [1, 2n] \ I we say a tree
T ′ ∈ CombsI∪{i} is an i-extension of T if T ′ can be obtained
from T by choosing exactly one leaf x and replacing its label
T (x) = (J, α) by (J ∪ {i}, α). Recall that by Combsϕ wedenote the trees from Combs[1,2n] whose word and variableassignment interpretation satisfies ϕ. Likeweise let Combsϕdenote the trees from Combs[1,2n] whose word and variableassignment interpretation does not satisfy ϕ.
For each game-conform I we have two configurations sIand sI in F. For each non-game-conform I we have one
corresponding configuration uI in F. In addition our finite
system F has the configurations succ and fail. We define asaction labels A = {ai | i ∈ [1, 2n]} ∪ {ϕ}.
The idea of the bisimulation game and difficulties
The high level idea of the strong bisimulation game goes asfollows, and uses Defender’s forcing techniques as e.g. in [13]:(initial round) Attacker chooses a comb T from Combs[1,1]for which he claims that T |= ψ[νT ] holds. Defender can only
a1
respond s∅ −→F s[1,1] . Hence the new pebble configuration
is (T, s[1,1] ).
Next, we repeat the following round game, where the current
pebble configuration is (T, s[1,k] ) where T ∈ Combs[1,k] foreach round k = 1, . . . , 2n − 1: (universal round) If k is odd,
ak+1
then Attacker is supposed to move in F, namely s[1,k] −→ F
ak+1
s[1,k+1] although the move s[1,k] −→ F s[1,k+1] is possible.
ak+1
Defender is now forced to move in S(R), namely T −→ T ′for some k+1-extension T ′ of T . This response corresponds tothe universal quantification ∀xk+1 in ψ. (existential round)If k is even, then Attacker is supposed to move in S(R),ak+1
namely T −→ T ′ for some k + 1-extension T ′ of T . This
move corresponds to the existential quantification ∃xk+1 in ψ.
ak+1
Defender’s only possible response in F is s[1,k] −→ F s[1,k+1] .
(final round) Finally, when we are in the pebble configuration(T, s[1,2n] ), where T ∈ Combs[1,2n] , the action ϕ can be
performed that allows Attacker to win (via a rule in R that
contains Combsϕ on the left-hand side) iff T |= ϕ[νT ].
In order to implement such a game, several difficulties arise.
Let us discuss these difficulties for the universal round (theexistential round can be treated dually) and give solutions
to them. The question is: In the universal round, how can

ak+1

we force Attacker to make in F the move s[1,k] −→ F
ak+1
s[1,k+1] ? 1. Difficulty: What if Attacker moves s[1,k] −→ Fs[1,k+1] (which will exist in F)? Solution: We add the ruleu[1,3]∪{6,7}a7u{1,3}
ak+1
Combs[1,k] ֒→ s[1,k+1] to R such that Defender has theu[1,3]∪{6} u[1,3]∪{7}u· · · [1,3]∪{2n}
possibility to establish syntactic equivalence by respondingu{2,3}
ak+1
a7
a2
a2n succ
T −→ s[1,k+1] in S(R) and hence wins. 2. Difficulty: What
a6
ak+1
′
a1
if Attacker moves T −→ T in S(R) for some k+1-extension
ak,k∈[1,3]ϕof T rather than playing in F? Solution: Defender can reacts[1,n−1]saiin F, depending on whether T ′ |= ψ[νT ′ ] or T ′ 6|= ψ[νT ′ ]. s∅ a1 s[1,1] a2 s[1,2] a3 s[1,3]an [1,2n]′···
In case T |= ψ[νT ′ ] she can move to s[1,k+1] and can win.
ai
a1
a2
a3
an
In case T ′ 6|= ψ[νT ′ ] she can move to s[1,k+1] and can win. s
s
s
s
s
s
[1,1]
[1,2]
[1,3]
[1,n−1][1,2n]
∅
a1
a2
a3
an
ai
T ′ where
3. Difficulty: What if Attacker plays T −→i ∈ [1, k]? I.e. Attacker plays an action that has alreadyϕai failbeen played. Solution: We allow a simple transition to aconfiguration in F from which Defender can surely win since Fig. 1. A snapshot of F and the outgoing transitions of s[1,3] in the strong
surely T ′ ∈ Combs⊥ and hence T ′ 6∈ Combsϕ . 4. Difficulty: bisimulation game (i ranges over [1, 2n]).
ai
T ′ in S(R) where i > k +1?
What if Attacker plays in T −→I.e. Attacker deviates from playing a sequence of actions
a1 · · · ak that correspond to assigning variables to positions of
The infinite system: Recall that C denotes the set of conthe yield string of the tree. We also say that the current pebble
figurations of F and that P denotes the set of proper leaf labels
configuration is non-game-conform. Solution: We allow inai
as defined in Section III-A. We define the ranked alphabet
u[1,k]∪{i} thatF a special transition for Defender s[1,k] −→A = (Ai )i∈{0,1,2} of R as follows: A0 = {start} ∪ P ∪ C,
allows her to win.
A1 = {root} and A2 = {⋆}. We note that the only relevant
The solutions to Difficulty 1 and 2 are standard and are similar trees (i.e. configurations) in S(R) in our reduction whose
to a technique elaborated in [13]. The solution to Difficulty leafs are labeled with C are singleton trees. To R we addbb′
3 is straightforward. The real difficulty in the absence of a the rewriting rules c ֒→ c′ for each transition c −→F c in F.
finite control (pushdown systems have a finite control) in the Furthermore, we add the following leaf rewriting rules, whereaigame is Difficulty 4. We have to provide configurations in α ∈ {0, 1}: (1) hI, αi ֒→
hI ∪ {i}, αi for each i ∈ [1, 2n] \ I,aaii
F that allow to remember the set of variables in the current (2) hI, αi ֒→h⊥, αi for each i ∈ I, and (3) h⊥, αi ֒→ h⊥, αitree T that have been assigned. The difficulty that now arises for each i ∈ I. We define the regular tree language Combs⊥ =is that Attacker can continue labeling leafs in T and pretend Combs \ S
I⊆[1,2n] CombsI . In other words, Combs⊥ consists
some moves later that the current tree T is game-conform all of those combs T ∈ Combs that satisfy (1) there is some leafof a sudden (and hence threaten to play the above-mentioned x of T with T (x) ∈ {⊥} × {0, 1} or (2) there are two distinct
punishing moves for instance). We have to carefully design leaves x, x′ of T with T (x) = (J, α) and T (x′ ) = (J ′ , α′ )transitions in F that sooner or later punish Attacker since he such that J ∩ J ′ 6= ∅.
was the one who deviated from playing game-conform.
Let us add for each possible I ⊆ [1, 2n] and k ∈ [0, 2n−1], theak+1
The finite system: We now define the outgoing transitions
following rules to R: (1) Combs[1,k] ֒→ s[1,k+1] if k is odd,of s[1,k] and of s[1,k] , for each possible k ∈ [0, 2n − 1]: (1)
ak+1
ai
ak+1
ak+1
ak+1
(2) Combs[1,k] ֒→ s[1,k+1] if k is even, (3) Combs[1,k]\{i} ֒→s[1,k] −→ F s[1,k+1] , (2) s[1,k] −→ F s[1,k+1] , (3) s[1,k] −→ Faiak+1s[1,k] for each i ∈ [1, k − 2], (4) Combs[1,k]\{i} ֒→ s[1,k] fors[1,k+1] if k is odd, (4) s[1,k] −→ F s[1,k+1] if k is even,aiaiaiuI for each i ∈ I if I(5) s[1,k] −→F s[1,2n] for each i ∈ [1, k], (6) s[1,k] −→F each i ∈ [1, k − 2], (5) CombsI\{i} ֒→
ai
ai
֒→
s
is
non-game-conform,
(6)
Combs
I
[1,2n] for each i ∈ I,s[1,2n] for each i ∈ [1, k], (7) s[1,k] −→F u[1,k+1]∪{i} forϕϕaieach i ∈ [k + 2, 2n], (8) s[1,k] −→F u[1,k+1]∪{i} for each (7) Combsϕ ֒→ fail, and (8) Combsϕ ∪ Combs⊥ ֒→ succ.
ϕai
One can easily verify that for each T ∈ Combsϕ ∪ Combs⊥i ∈ [k + 2, 2n], (9) s[1,2n] −→F succ, (10) s[1,2n] −→F s[1,2n]ϕ
wehave T ∼ s[1,2n] . This following lemma establishes
for each i ∈ [1, 2n], (11) s[1,2n] −→F fail and the transitionaicorrectnessof the construction.
(12) fail −→ fail for each i ∈ [1, 2n].
F

Let us now define the outgoing transitions of uI for each nonai
game-conform I ⊆ [1, 2n]: (1) uI −→F s[1,2n] for each i ∈ I,ai(2) uI −→F uI∪{i} for each i 6∈ I for which I ∪ {i} is nonai
game-conform, (3) uI −→F sI∪{i} for each i 6∈ I for whichaiI ∪ {i} is game-conform, and (4) uI −→F sI∪{i} for eachi 6∈ I for which I ∪ {i} is game-conform.
A snapshot of F is depicted in Figure 1.

Lemma 13. Let I ⊆ [1, 2n]. If I is game-conform, then(1) sI 6∼ sI , (2) ∀T ∈ CombsI : T 6∼ sI iff T |= ψ[νT ],and (3) ∀T ∈ CombsI : T ∼ sI iff T |= ψ[νT ]. (4) If I
is non-game-conform, then for each T ∈ CombsI we haveT ∼ uI .

Proof: We prove the lemma by downward induction on|I| = 2n, 2n − 1, . . ..
Induction base. Let |I| be maximal, i.e. I = [1, 2n] and so I
is game-conform. Thus, we only have to prove Points (1),(2),and (3). (1) We have to prove that s[1,2n] 6∼ s[1,2n] . Attacker
ϕmoves from s[1,2n] −→F succ and hence reaches a deadϕend. Defender can only respond with s[1,2n] −→F fail anddoes not reach a dead-end. Thus s[1,2n] 6∼ s[1,2n] . (2) Let
T ∈ Combs[1,2n] . On the one hand, assume T |= ψ[νT ] orequivalently T |= ϕ[νT ]. Hence, T ∈ Combsϕ by definition,
ϕso Attacker can move T −→ fail in S(R) and thus reaches
a configuration that is not a dead-end, whereas Defender canϕonly respond with s[1,2n] −→F succ in F which is a dead-end.
Hence T 6∼ s[1,2n] . On the other hand, assume T 6|= ϕ[νT ].
Hence T ∈ Combsϕ and therefore Hence T ∼ s[1,2n] . Point(3) can be proven similar to (2).
Induction step. Let I ⊂ [1, 2n]. Let us assume that I is gameconform, i.e. I = [1, k] for some k ∈ [2n − 1].
ak+1(1) If k is odd, then Attacker plays s[1,k] −→ F s[1,k+1] andak+1
Defender can only respond with s[1,k] −→ F s[1,k+1] . By
induction hypothesis we have s[1,k+1] 6∼ s[1,k+1] , so s[1,k] 6∼
ak+1
s[1,k] . If k is even, then Attacker plays s[1,k] −→ F s[1,k+1]
ak+1
and Defender can only respond with s[1,k] −→ F s[1,k+1] .
By induction hypothesis we have s[1,k+1] 6∼ s[1,k+1] , sos[1,k] 6∼ s[1,k] .
(2) Let T ∈ Combs[1,k] . We only treat the case where k isodd. Then recall that ψ[νT ] = ∀xk+1 ∃xk+2 · · · ∀x2n ϕ[νT ].
On the one hand, assume T |= ψ[νT ]. Hence, in other words,
for each k + 1-extension T ′ of T we have T ′ |= ψ[νT ′ ].
ak+1
Attacker can now play s[1,k] −→ F s[1,k+1] . Defender cannot
ak+1
play T −→ s[k+1] since s[1,k+1] 6∼ s[1,k+1] by Point (1)of induction hypothesis. Defender only has the possibility toarespond T −→ T ′ in S(R) for some k + 1-extension T ′ ofT . Since T ′ |= ψ[νT ′ ] we have T ′ ∼ s[1,k+1] by Point (2) of
induction hypothesis, hence T 6∼ s[1,k] .
On the other hand, assume T 6|= ψ[νT ]. Thus, there is someextension T ′ ∈ Combs[k+1] of T such that T ′ 6|= ψ[νT ′ ]. We
ak+1
have to show that T ∼ s[1,k] . • If Attacker plays s[1,k] −→ F
ak+1
s[1,k+1] , then Defender responds T −→ T ′ and wins by
Point (2) of induction hypothesis. Conversely, if Attacker plays
ak+1
T −→ T ′′ for some extension T ′′ ∈ Combs[1,k+1] of T , wedistinguish two cases. In case T ′′ 6|= ψ[νT ′′ ], then Defender
ak+1
plays s[1,k] −→ F s[1,k+1] and wins by Point (2) of induction
hypothesis. In case T ′′ |= ψ[νT ′′ ], then Defender responds
ak+1
s[1,k] −→ F s[1,k+1] and wins by Point (3) of induction hypothak+1
esis. • If Attacker plays s[1,k] −→ F s[1,k+1] , then Defender
ak+1
plays T −→ s[1,k+1] in T (R) and vice versa. Defenderwins by establishing syntactic equivalence. • If Attacker playsais[1,k] −→F s[1,2n] for some i ∈ [1, k], then Defender respondsai
T ′′ for some T ′′ ∈ Combs⊥ by labeling a leaf of T andT −→vice versa. We know that each tree from Combs⊥ is bisimilarai
to s[1,2n] . • If Attacker plays s[1,k] −→F u[1,k]∪{i} for someaiu[1,k]∪{i}i ∈ [k + 2, 2n], then Defender responds T −→and vice versa. Hence Defender wins by establishing syntacticai
T ′′ for some iequivalence. • If Attacker plays T −→′extension T ∈ Combs[1,k]∪{i} of T where i ∈ [k + 2, 2n],aithen Defender responds s[1,k] −→F u[1,k]∪{i} and vice versa.
By Point (4) of induction hypothesis, we have T ′′ ∼ u[1,k] ,hence Defender wins.
We omit the proof of Point (3).
Let I ⊆ [1, k] be non-game-conform and let T ∈ CombsI . We
have to prove that T ∼ uI .
ai
T ′ for some i ∈ I and some
• If Attacker moves T −→ai′
T ∈ Combs⊥ , then Defender responds with uI −→F s[1,2n]and vice versa, which results in a pair of bisimilar conaiT ′ where T ′ ∈figurations. • If Attacker moves T −→CombsI∪{i} is an i-extension of T , where i ∈ [1, 2n] \ I andI ∪ {i} is non-game-conform, then Defender responds withaiuI −→F uI∪{i} and vice versa. Defender wins by Point 2 ofai
induction hypothesis. • If Attacker plays uI −→F s[1,k] (resp.
aiuI −→F s[1,k] ), i.e. in particular I ∪ {i} is game-conform,aiais[1,k] (resp. T −→then Defender responds with T −→s[1,k] )and vice versa. Hence Defender wins by establishing syntacticai
T ′ for some i-extension
equivalence. • If Attacker plays T −→′T ∈ Combs[1,k] of T , i.e. I ∪ {i} = [1, k] is game-conform,ai′then Defender responds uI −→F s[1,k] in case T |= ψ[νT ′ ]ai
and with uI −→F s[1,k] in case T ′ 6|= ψ[νT ′ ]. In the formercase Defender wins since T ′ ∼ s[1,k] by Point (2) of induction
hypothesis. In the latter case Defender wins since T ′ ∼ s[1,k]by Point (3) of induction hypothesis.
In order to realize the initial round (as mentioned above)a1
a1
we add the rules start ֒→ s[1,1] and start ֒→ Combs[1,1] to R.
Theorem 12 now easily follows.

V. W EAK BISIMILARITY AGAINST FINITE SYSTEMS
Since weak bisimilarity checking can be reduced to EFmodel checking, the following theorem follows from known
results.
Theorem 14 ([14], [11]). Weak bisimilarity checkingof RGTRS against finite systems is decidable in time
TOWER(O(n)).
Our main result in this section is a nonelementary lower boundfor weak bisimilarity checking of GTRS against finite systems.
Theorem 15. Weak bisimilarity of GTRS against finite systems
is nonelementary.
This is technically the most involved result. Although its
proof is based on the previous nonelementary lower boundfor strong bisimiliarity of RGTRS against finite systems, it
is not a straightforward adaption of the proof for strong
bisimulation of Section IV. In a nutshell, we mimic one suchrewriting rule L ֒→ T of a RGTRS, where L is a regulartree language and T is an explicit ranked tree by simulating atree automaton for L via a sequence of τ -transitions. However,again due to the absence of a finite control unit, we are now
faced with new obstacles. Firstly, we have to provide bottomup computations for numerous tree automata and we haveto provide means of making these bottom-up computations

“visible” to the finite system. Secondly, we should not allow
two bottom-up computations at the same time although wehave to be able to realize the first obstacle. Thirdly, it is still
possible that during the bottom-up computation the scanned
tree is modified (in particular for the tree language Combsϕ ).
The finite system has to be able to react to this.
The goal of this section is to sketch our proof that weakbisimilarity checking of GTRS against finite systems has
nonelementary complexity. Due to lack of space, we mainly
describe the difficulties that one has to deal with in the proof
in more details. The reader is recommended to consult our
technical report to get a feeling for the proof.
Recall that in Section IV we provided in the RGTRS rulesof the kind L ֒→ c, where L is a regular tree language andc ∈ C is a configuration of F. These rules allowed Defender topunish Attacker in case e.g. Attacker played in F rather thanin S(R) or Attacker deviates from playing game-conform.
However, since in GTRS the rewriting rules only allow torewrite trees rather than trees from a tree language, we have tofind a way of simulating the computations of tree automata. An
ad-hoc approach we follow is to simulate such a rule L ֒→ c
by a sequence of τ -transitions in S(R) that correspond to abottom-up computation of the respective tree automaton.
Let us fix a game-conform comb T . The major difficulties
that now arise are the following: (1) Due to the absence ofa finite control unit in our GTRS R we must provide in
the rewriting rules of R the possibility to simulate from T
all possible tree automata. Hence Defender must have thepossibility to react in F to each of such computations. (2)Assume that we construct in our finite system F a response
for Defender to react to an initialization of a bottom-up
computation of a tree language. We have to be guarantee
in F that each two such responses are not weakly-bisimilar
in order to distinguish different (intializations of) tree
languages. (3) Since we allow the bottom-up computation for
Combsϕ , Attacker can in theory initialize from T a bottom-up
computation for Combsϕ although T 6∈ Combs[1,2n] , i.e.
not all of the variables have yet been assigned. In doing so,
Attacker might add to T the remaining variables that have
not yet been assigned and threaten to label the leafs of comb
during the bottom-up computation. We have to provide amechanism for Defender to win always as soon as Attacker
initializes Combsϕ too early.
ACKNOWLEDGEMENTS :We thank Thomas Colcombet, Lane Hemasspaandra,
Markus Lohrey and Carsten Lutz for discussions. Anthony
W. Lin is supported by EPSRC (EP/H026878/1).
R EFERENCES[1] E. Allender, M. Koucky, D. Ronneburger and S. Roy. The
Pervasive Reach of Resource-Bounded Kolmogorov Complexity
in Computational Complexity Theory. To appear at JCSS’10.
[2] A. Bouajjani, J. Esparza and O. Maler. Reachability Analysisof Pushdown Automata: Application to Model-Checking. In
CONCUR’97, p. 135–150.

[3] A. Bouajjani, M. Müller-Olm and T. Touili. Regular Symbolic
Analysis of Dynamic Networks of Pushdown Systems. In
CONCUR’05, p. 473–487.
[4] W. S. Brainerd. Tree Generating Regular Systems. Information
and Control, 14(2):217–231, 1969.
[5] D. Caucal. On infinite transition graphs having a decidable
monadic theory. TCS 290(1):79–115, 2003.
[6] H. Comon et al. Tree Automata Techniques and Applications.
Available at: http://www.grappa.univ-lille3.fr/tata.
[7] J. -L. Coquidé, M. Dauchet, R. Gilleron and S. Vágvölgyi.
Bottom-Up Tree Pushdown Automata: Classification and Connection with Rewrite Systems. Theor. Comput. Sci., 127(1):69–
98, 1994.
[8] M. Dauchet, T. Heuillard, P. Lescanne and S. Tison. Decidabilityof the Confluence of Finite Ground Term Rewrite Systems
and of Other Related Term Rewrite Systems. Inf. Comput.,
88(2):187–201, 1990.
[9] M. Dauchet and S. Tison. The Theory of Ground Rewrite
Systems is Decidable. In LICS’90, p. 242–248.
[10] J. Esparza and A. Podelski. Efficient algorithms for pre* andpost* on interprocedural parallel flow graphs. In POPL’00, p.
1–11.
[11] P. Jancar, A. Kucera and R. Mayr. Deciding bisimulation-likeequivalences with finite-state processes. Theor. Comput. Sci.,
258(1–2):409–433, 2001.
[12] V. Kahlon and A. Gupta. On the analysis of interacting
pushdown systems. In POPL’07, p. 303–314.
[13] A. Kucera and R. Mayr. On the Complexity of Checking
Semantic Equivalences between Pushdown Processes and Finitestate Processes. Inf. Comput., 208(7):772–796, 2010.
[14] C. Löding. Infinite Graphs Generated by Tree Rewriting. PhD
Thesis, RWTH Aachen, 2003.
[15] D. Lugiez and Ph. Schnoebelen. The regular viewpoint on PAprocesses. Theor. Comput. Sci., 274(1–2):89–115,2002.
[16] R. Mayr. Decidability and Complexity of Model Checking
Problems for Infinite-State Systems. PhD thesis, TU-Munich,
1998.
[17] D. E. Muller and P. E. Schupp. The Theory of Ends, Pushdown
Automata, and Second-Order Logic. Theor. Comput. Sci., 37:51–
75, 1985.
[18] C. Papadimitriou. Computational Complexity. Addison Wesley,
1994.
[19] S. Qadeer and J. Rehof. Context-Bounded Model Checking ofConcurrent Software. In TACAS’05, p. 93–107.
[20] J. Srba. Roadmap of Infinite Results. Bulletin of the EATCS,
78:163–175, 2002. Updated version: http://www.brics.dk/∼srba/
roadmap/[21] L. J. Stockmeyer. The complexity of decision problems in
automata theory and logic. PhD Thesis, MIT, 1974.
[22] S. Tison. Fair Termination is Decidable for Ground Systems.
In RTA’89, p. 462–476.
[23] A. W. To and L. Libkin. Algorithmic Metatheorems for
Decidable LTL Model Checking over Infinite Systems. In
FoSSaCS’10, p. 221–236.
[24] A. W. To. Model Checking Infinite-State Systems: Genericand Specific Approaches. PhD Thesis, University of Edinburgh,
2010.
[25] I. Walukiewicz. Pushdown Processes: Games and Model Checking. In CAV’96, pages 62–74.
[26] I. Walukiewicz. Model Checking CTL Properties of Pushdown
Systems. In FSTTCS’00, p.127–138.