Refining the Process Rewrite Systems Hierarchy via
Ground Tree Rewrite Systems
Stefan Göller1 and Anthony Widjaja Lin2
1
2

Universität Bremen, Institut für Informatik, Germany
Oxford University Department of Computer Science, UK

Abstract. In his seminal paper, R. Mayr introduced the well-known Process
Rewrite Systems (PRS) hierarchy, which contains many well-studied classes of
infinite systems including pushdown systems, Petri nets and PA-processes. A
seperate development in the term rewriting community introduced the notion of
Ground Tree Rewrite Systems (GTRS), which is a model that strictly extends
pushdown systems while still enjoying desirable decidable properties. There havebeen striking similarities between the verification problems that have been shown
decidable (and undecidable) over GTRS and over models in the PRS hierarchy
such as PA and PAD processes. It is open to what extent PRS and GTRS areconnected in terms of their expressive power. In this paper we pinpoint the exact
connection between GTRS and models in the PRS hierarchy in terms of their expressive power with respect to strong, weak, and branching bisimulation. Amongothers, this connection allows us to give new insights into the decidability results for subclasses of PRS, e.g., simpler proofs of known decidability results ofverifications problems on PAD.

1 Introduction
The study of infinite-state verification has revealed that unbounded recursions and unbounded parallelism are two of the most important sources of infinity in the programs.
Infinite-state models with unbounded recursions such as Basic Process Algebra (BPA),
and Pushdown Systems (PDS) have been studied for a long time (e.g. [2, 21]). The samecan be said about infinite-state models with unbounded parallelism, which include Basic
Parallel Processes (BPP) and Petri nets (PN), e.g. [10, 14]. While these aforementioned
models are either purely sequential or purely parallel, there are also models that simultaneously inherit both of these features. A well-known example are PA-processes [3],which are a common generalization of BPA and BPP. It is known that all of these models are not Turing-powerful in the sense that decision problems such as reachability is
still decidable (e.g. see [9]), which makes them suitable for verification.
In his seminal paper [18], R. Mayr introduced the Process Rewrite Systems (PRS)
hierarchy (see leftmost diagram in Figure 1) containing several models of infinite-statesystems that generalize the aforementioned well-known models with unbounded recursions and/or unbounded parallelism. The idea is to treat models in the hierarchy as aform of term rewrite systems, and classify them according to which terms are permitted on the left/right hand sides of the rewrite rules. In addition to the aforementioned
models of infinite systems, the PRS hierarchy contains three new models: (1) ProcessRewrite Systems (PRS), which generalize PDS, PA-processes, and Petri nets, (2) PADprocesses, which unify PDS and PA-processes, and (3) PAN-processes, which unify
both PA-processes and Petri nets. Mayr showed that the hierarchy is strict with respect
to strong bisimulation. Despite of its expressive power PRS is not Turing-powerfulsince reachability is still decidable for this class. Before the PRS hierarchy was introduced, another class of infinite-state systems called Ground Tree/Term Rewrite Systems(GTRS) already emerged in the term rewriting community as a class with nice decidability properties. While extending the expressive power of PDS, GTRS still enjoys
decidability of reachability (e.g. [8, 11]), recurrent reachability [15], model checking
first-order logic with reachability [12], and model checking the fragments LTLdet and
LTL(Fs , Gs ) of LTL [24, 23]. Due to the tree structures that GTRS use in their rewrite
rules, GTRS can be used to model concurrent systems with both unbounded parallelism(a new thread may be spawned at any given time) and unbounded recursions (eachthread may behave as a pushdown system).
When comparing the definitions of PRS (and subclasses thereof) and GTRS, one
cannot help but notice their similarity. Moreover, there is a striking similarity between
the problems that are decidable (and undecidable) over subclasses of PRS like PA/PADprocesses and GTRS. For example, reachability, EF model checking, and LTL(Fs , Gs )and LTLdet model checking are decidable for both PAD-processes and GTRS [7, 15,
18, 19, 23, 24]. Furthermore, model checking general LTL properties is undecidable forboth PA-processes and GTRS [7, 24]. Despite these, the precise connection between the
PRS hierarchy and GTRS is currently still open.
Contributions: In this paper, we pinpoint the precise connection between the expressive powers of GTRS and models inside the PRS hierarchy with respect to strong,branching, and weak bisimulation. Bisimulations are well-known and important notions of semantic equivalences on transition systems. Among others, most properties
of interests in verification (e.g. those expressible in standard modal/temporal logics)
cannot distinguish two transition systems that are bisimilar. Strong/weak bisimulations
are historically the most important notions of bisimulations on transition systems inverification [20]. Weak bisimulations extend strong bisimulations by distinguishing observable and non-observable (i.e. τ ) actions, and only requiring the observable behaviorof two systems to agree. In this sense, weak bisimulation is a coarser notion than strong
bisimulation. Branching bisimulation [25] is a notion of semantic equivalence that isstrictly coarser than strong bisimulation but is strictly finer than weak bisimulation. It
refines weak bisimulation equivalence by preserving the branching structure of two processes even in the presence of unobservable τ -actions; it is required that all intermediate
states that are passed through during τ -transitions are related.
Our results are summarized in the middle and right diagrams in Figure 1. Our firstmain result is that the expressive power of GTRS with respect to branching and weakbisimulation is strictly in between PAD and PRS but incomparable with PAN. This
result allows us to transfer many decidability/complexity results of model checking
problems over GTRS to PA and PAD-processes. In particular, it gives a simple proof ofthe decidability of model checking the logic EF over PAD [19], and decidability (withgood complexity upper bounds) of model checking the common fragments LTLdet and
LTL(Fs , Gs ) of LTL over PAD (this decidability result was initially given in [7] with2

out upper bounds). In fact, we also show that Regular Ground Tree Rewrite Systems(RGTRS) [15] — the extension of GTRS with possibly infinitely many GTRS rules
compactly represented as tree automata — have the same expressive power as GTRS
up to branching/weak bisimulation. Our proof technique also implies that PDS is equivalent to prefix-recognizable systems (e.g. see [9]), abbreviated as PREF, up to branching/weak bisimulation. On the other hand, when we investigate the expressive power of
GTRS with respect to strong bisimulation, we found that PAD (even PA) is no longer
subsumed in GTRS. Despite this, we can show that up to strong bisimulation GTRS isstrictly more expressive than BPP and PDS, and is strictly subsumed in PRS. Finally,
we mention that our results imply that Mayr’s PRS hierarchy is also strict with respect
to weak bisimulation equivalence.
Related work: Our work is inspired by the work of Lugiez and Schnoebelen [16] andBouajjani and Touili [6], which study PRS (or subclasses thereof) by first distinguishing process terms that are “equivalent” in Mayr’s sense [18]. This approach allows themto make use of techniques from classical theory of tree automata for solving interesting problems over PRS (or subclasses thereof). Our translation from PAD to GTRS issimilar in spirit.
There are other models of multithreaded programs with unbounded recursions thathave been studied in the literature. Specifically, we mention Dynamic Pushdown Networks (DPN) and extensions thereof (e.g. see [5]) since an extension of DPN given
in [5] also extends PAD-processes. We leave it for future work to study the precise
connections between these models and GTRS.
Organization: Preliminaries are given in Section 2. We provide the models of infinite
systems (PRS, GTRS, etc.) in Section 3. Our containment results (e.g. PAD is subsumed in GTRS up to branching bisimulation) can be found in Section 4. Section 5gives the separation results for the refined PRS hierarchies. Finally, we briefly discuss
applications of our results in Section 6.
PRS

PRS

PAD

GTRS

PAN

PAD

PRS
GTRS = RGTRS

PAN

PA

PA

PAN

PAD
PN

PDS

PN
BPA

BPP
FIN

PDS = PREF

PDS
BPA

BPP
FIN

PA

BPA

PN
BPP

FIN

Fig. 1. Depictions of Mayr’s PRS hierarchy and their refinements via GTRS as Hasse diagrams(the top being the most expressive). The leftmost diagram is the original (strict) PRS hierarchy
where expressiveness is measured with respect to strong bisimulation. The middle (resp. right) diagram is a strict refinement via GTRS with respect to strong (resp. weak/branching) bisimulation.

3

2 Preliminaries
By N = {0, 1, 2, . . .} we denote the non-negative integers. For each i, j ∈ N we define
the interval [i, j] = {i, i + 1, . . . , j}.
Transition systems and weak/branching/strong bisimulation equivalence: Let usa
fix a countable set of action labels Act. A transition system is tuple T = (S, A, {−→|a ∈ A}), where S is a set of states, A ⊆ Act is a finite set of action labels, and whereaaa−→⊆ S × S is a set of transitions. We write s −→ t to abbreviate (s, t) ∈−→. We
apply similar abbreviations for other binary relations over S. For each R ⊆ S × S, we
write sR to denote that there is some t ∈ S with (s, t) ∈ R. For each Λ ⊆ A, we defineSaΛA−→= a∈Λ −→ and we define −→=−→. Whenever T is clear from the context andΛ ∗U ⊆ S, we define post∗Λ (U ) = {t ∈ S | ∃s ∈ U : s −→ t}. In case U = {s} is asingleton, we also write post∗Λ (s) for post∗Λ (U ).
A pointed transition system is a pair (T , s), where T is a transition system and sais some state of T . Let T = (S, A, {−→| a ∈ A}) be a transition system. A relation
R ⊆ S × S is a strong bisimulation if R is symmetric and for each (s, t) ∈ R and foraaeach a ∈ A we have that if s −→ s′ , then there is t −→ t′ such that (s′ , t′ ) ∈ R. We
say that s is strongly bisimilar to t (abbreviated by s ∼ t) whenever there is a strong
bisimulation R such that (s, t) ∈ R.
Next, we define the notions of branching bisimulation and weak bisimulation. For
this, let us fix a silent action τ 6∈ A and let Aτ = A ∪ {τ }. Moreover let T =a
τ(S, Aτ , {−→| a ∈ Aτ }) be a transition system. We define the binary relations =⇒=
τ
a
τ
a
τ
(−→)∗ and =⇒= (−→)∗ ◦ −→ ◦(−→)∗ for each a ∈ A.
A binary relation R ⊆ S × S is a branching bisimulation if R is symmetric and ifτfor each (s, t) ∈ R the following two conditions hold: (i) if s −→ s′ , then (s′ , t) ∈ R
τ
τ
a
′ a
′
and (ii) if s −→ s for some a ∈ A, then there is t =⇒ t −→ t′′ =⇒ t′′′ such that
′
′ ′′
′ ′′′
(s, t ), (s , t ), (s , t ) ∈ R. We say that s is branching bisimilar to t (abbreviated bys ≃ t) whenever there is a branching bisimulation R such that (s, t) ∈ R.
A binary relation R ⊆ S × S is a weak bisimulation if R is symmetric and for eachaa(s, t) ∈ R and for each a ∈ Aτ we have that if s −→ s′ , then there is t =⇒ t′ such
′ ′that (s , t ) ∈ R. We say that s is weakly bisimilar to t (abbreviated by s ≈ t) whenever
there is a weak bisimulation R such that (s, t) ∈ R.
Each of the three introduced bisimulation notions can be generalized between statess1 and s2 where s1 (resp. s2 ) is a state of some transition system T1 (resp. T2 ), by
simply taking the disjoint union of T1 and T2 .
Let C1 and C2 be classes of transition systems and let ≡∈ {∼, ≃, ≈} be some notionof equivalence. We write C1 ≤≡ C2 if for every pointed transition system (T1 , s1 ) with
T1 ∈ C1 there exists some pointed transition system (T2 , s2 ) with T2 ∈ C2 such thats1 ≡ s2 . We write C1 ≡ C2 in case C1 ≤≡ C2 and C2 ≤≡ C1 .
These above-mentioned equivalences can also be characterized by the standard
Attacker-Defender game, see e.g. [13] and the references therein.
Ranked trees: Let  denote the prefix order on N∗ , i.e. x  y for x, y ∈ N∗ if there issome z ∈ N∗ such that y = xz, and x ≺ y if x  y and x 6= y. A ranked alphabet is a4collection of finite and pairwiseSdisjoint alphabets A = (Ai )i∈[0,k] for some k ≥ 0. For
simplicity we identify A with i∈[0,k] Ai . A ranked tree (over the ranked alphabet A)
is a mapping t : Dt → A, where Dt ⊆ [1, k]∗ satisfies the following: Dt is non-empty,
finite and prefix-closed and 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 refer to ε ∈ Dt as the root of t. By
TreesA we denote the set of all ranked trees over the ranked alphabet A. We also use
the usual term representation of trees, e.g. if t is a tree with root a and left (resp. right)
subtree t1 (resp. t2 ) we have t = a(t1 , t2 ).
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 rootx, i.e. the tree with 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 replacingt↓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 t[x/s](y) = s(z) if y = xz with z ∈ Ds .
Define |t| = |Dt | as the number of nodes in a tree t.
Regular tree languages: A nondeterministic tree automaton (NTA) is a tuple A =(Q, F, A, ∆), where Q is a finite set of S
states, F ⊆ Q is a set of final states, A =(Ai )i∈[0,k] is a ranked alphabet, and ∆ ⊆ i∈[0,k] Qi ×Ai ×Q is the transition relation.
A run of A on some tree t ∈ TreesA is a mapping ρ : Dt → Q such that for each x ∈ Dt
with t(x) ∈ Ai we have (ρ(x1), . . . , ρ(xi), t(x), ρ(x)) ∈ ∆. We say ρ is accepting if
ρ(ε) ∈ F . By L(A) = {t ∈ TreesA | there is an accepting run of A on t} we denotethe language of A. A set of trees U ⊆ TreesA is regular if U = L(A) for some NTA
A. The size of an NTA A is defined as |A| = |Q| + |A| + |∆|.

3 The models
3.1 Mayr’s PRS hierarchy
In the following, let us fix a countable set of process constants (a.k.a. process variables)
X = {A, B, C, D, . . .}. The set of process terms is given by the following grammar,
where X ranges over X:
t, u

::=

0

|

X

|

t.u

|

t||u

The operator . is said to be sequential composition, while the operator k is referred to as
parallel composition. In order to minimize clutters, we assume that both operators . andk are left-associative, e.g., X1 .X2 .X3 .X4 stands for ((X1 .X2 ).X3 ).X4 . The size |t| ofa term is defined as usual. Mayr distinguishes the following classes of process terms:

1 Terms consisting of a single constant X ∈ X.
S Process terms without any occurrence of parallel composition.
P Process terms without any occurrence of sequential composition.
G Arbitrary process terms possibly with sequential or parallel compositions.
By 1(Σ), S(Σ), P(Σ), respectively G(Σ) we denote the set 1, S, P, respectively G
restricted to process constants from Σ, for each finite subset Σ ⊆ X.
5

A process rewrite system (PRS) is a tuple P = (Σ, A, ∆), where Σ ⊆ X is a
finite set of process constants, A ⊆ Act is a finite set of action labels, and ∆ is a
finite set of rewrite rules of the form t1 7→a t2 , where t1 ∈ G(Σ) \ {0}, t2 ∈ G(Σ)
and a ∈ A. Other models in PRS hierarchy are Finite Systems (FIN), Basic Process
Algebra (BPA), Basic Parallel Processes (BPP), Pushdown Systems (PDS), Petri Nets
(PN), PA-processes (PA), PAD-processes (PAD), and PAN-processes (PAN). They canbe defined by restricting the terms that are allowed on the left/right hand side of the
PRS rewrite rules as specified in the following tables.
Model L.H.S. R.H.S
FIN 1(Σ) 1(Σ)
BPA 1(Σ) S(Σ)
BPP 1(Σ) P(Σ)

Model L.H.S. R.H.S
PDS S(Σ) S(Σ)PN
P(Σ) P(Σ)

Model L.H.S. R.H.S
PAD S(Σ) G(Σ)
PAN P(Σ) G(Σ)

We follow the approach of [16, 6] to define the semantics of PRS. While Mayr [18] directly works on the equivalence classes of terms (induced by some equivalence relation≡ defined by some axioms including associativity and commutativity of k) to define thedynamics of PRS, we shall initially work on term level. More precisely, given a PRSa
P = (Σ, A, ∆), we write T0 (P) to denote the transition system (G(Σ), A, {−→| a ∈aA}) where −→ is defined by the following rules:
t1 −→ t′1at2 −→ t′2at1 −→ t′1aaa

t1 kt2 −→ t′1 kt2a

t1 kt2 −→ t1 kt′2

t1 .t2 −→ t′1 .t2au −→ t(u 7→a t) ∈ ∆We now define Mayr’s semantics of PRS in terms of T0 (P). First of all, let us define
the equivalence relation ≡ on terms using the following proof rules:A.

t.0 ≡ tR0.

t1 .(t2 .t3 ) ≡ (t1 .t2 ).t3

0.t ≡ tL0.

t1 k(t2 kt3 ) ≡ (t1 kt2 )kt3

tk0 ≡ t0kt ≡ tR0k
L0k

t1 kt2 ≡ t2 kt1AkCku ≡ u Ref

t1 ≡ u1t2 ≡ u2Con.
t1 .t2 ≡ u1 .u2
t1 ≡ u1t2 ≡ u2Conk
t1 kt2 ≡ u1 ku2u ≡ u′u′ ≡ u′′Transu ≡ u′′
t≡u
Sym
u≡t

Here, u, t, ti , ui range over all terms in G. Intuitively, the axioms defining ≡ say that 0 is
identity, while the operator . (resp. k) is associative (resp. associative and commutative).
The rules (Con.) and (Conk) are standard context rules in process algebra saying thatterm equivalence is preserved under substitutions of equivalent subterms. Finally, Trans,
Sym, and Ref state that ≡ is an equivalence relation. In the sequel, we also use thesymbol ≡1 to denote the equivalence relation on process terms that allows all the above
axioms except for (Ak) and (Ck). Obviously, ≡1 ⊆≡. Given a term t ∈ G, we denote by[t]≡ (resp. [t]≡1 ) the ≡-class (resp. ≡1 -class) containing t.
aMayr’s semantics on a PRS P = (Σ, A, ∆) such that T0 (P) = (G(Σ), A, {−→| a ∈A}) is a transition system T (P) = (S, A, {Ea | a ∈ A}), where S = {[t]≡ | t ∈ G(Σ)}
aand where (C, C ′ ) ∈ Ea iff there exist t ∈ C and t′ ∈ C ′ such that t −→ t′ . An
important result by Mayr [18] is that the PRS hierarchy is strict with respect to strong
bisimulation.
6

3.2 (Regular) ground tree rewrite systems and prefix-recognizable systems
A regular ground tree rewrite system (RGTRS) is a tuple R = (A, A, R), where A isa ranked alphabet, A ⊆ Act is a finite set of action labels and where R is finite set ofarewrite rules L ֒→ L′ , where L and L′ are regular tree languages over A given as NTA.
a
The transition system defined by R is T (R) = (TreesA , A, {−→| a ∈ A}), where foraeach a ∈ A, we have t −→ t′ if and only if there is some x ∈ Dt and some rulea
L ֒→ L′ ∈ R such that t↓x = s and t′ = t[x/s′ ] for some s ∈ L and some s′ ∈ L′ .
A ground tree rewrite system (GTRS) is an RGTRS R = (A, A, R), where for eacha
L ֒→ L′ ∈ R we have that both L = {t} and L′ = {t′ } is a singleton; we also writeat ֒→ t′ ∈ R for this.
A prefix-recognizable system (PREF) is an RGTRS R = (A, A, R), where only A0
and A1 may be non-empty. We note that analogously pushdown systems can be defined
as GTRS R = (A, A, R), where only A0 and A1 may be non-empty.

4 Containment results
In this section, we prove the following containment results: PAD ≤≃ GTRS (Section4.1), BPP ≤∼ GTRS and GTRS ≤∼ PRS, and finally RGTRS =≃ GTRS (Section
4.2).
4.1 PAD ≤≃ GTRS
Theorem 1 (PAD ≤≃ GTRS). Given a PAD P = (Σ, A, ∆) and a term t0 ∈ G(Σ),
there exists a GTRS R = (A, Aτ , R) and a tree t′0 ∈ TreesA such that (T (P), [t0 ]≡ )is branching bisimilar to (T (R), t′0 ). Furthermore, R and t′0 may be computed in timepolynomial in |P| + |t0 |.
Before proving this theorem, we shall first present the general proof strategy. The maindifficulty of the proof is that the domain S ′ of T (P) consists of ≡-classes of process
terms, while the domain of T (R) consists of ranked trees. On the other hand, observethat the other semantics T0 (P) is more close to a GTRS since the domain S of T0 (P)consists of process terms (not equivalence classes thereof). Therefore, the first hurdle
in the proof is to establish a connection between T (P) and T0 (P). To this end, we will
require that t0 and all process terms in P have a minimum number of zeros and have noright-associative occurrence of the sequential composition operator. We will then picka small subset of the axioms of ≡ as τ -transitions, which we will add to T0 (P). Theseaxioms include those that reduce the occurrences of 0 from terms, and the rule thatturns a right-associative occurrence of the sequential composition operator into a leftassociative occurrence. The resulting pointed transition system (T0 (P), t0 ) will becomebranching bisimilar to (T (P), [t0 ]≡ ). In fact, fixing t0 as the initial configuration, we
will see that further restrictions to the axioms for ≡ (e.g. associativity of .) may be maderesulting in a pointed transition system that can be easily captured in the framework of
GTRS.
7

τ

Adding the τ -transitions to T0 (P): We define the relation −→ on arbitrary process
terms given by the following proof rules:τ

t1 −→ t′1τ

tk0 −→ tτt1 .(t2 .t3 ) −→ (t1 .t2 ).t3τ
t1 −→ t′1τ

t1 kt2 −→ t′1 kt2

0.t −→ t
t.0 −→ t
0kt −→ tττ

t1 .t2 −→ t′1 .t2
τ
t2 −→ t′2ττ

t1 kt2 −→ t1 kt′2τt2 −→ t′2ττ

t1 .t2 −→ t1 .t′2

Here, t is allowed to be any process term. Observe that these τ -transitions remove
redundant occurrences of 0 and turns a right-associative occurrence of the sequential composition into a left-associative one. Observe that we do not allow associativτ
τ
ity/commutativity axioms for k in our definition of −→. It is easy to see that −→⊆≡1 ⊆τ
≡. We now note a few simple facts about −→ in the following lemmas.
τ ∗τLemma 2. For all terms t, there exists a unique term t↓ such that t −→ t↓ and t↓ −→.
6
Furthermore, all paths from t to t↓ are of length at most O(|t|2 ), and moreover t↓ iscomputable from t in polynomial time.
Lemma 3. The following statements hold: (1) If t ≡1 t′ , then t↓ = t′↓ , (2) If 0 ≡ v,
τ ∗

τ ∗

then v −→ 0, and (3) If X1 .X2 . . . Xn ≡ v, then v −→ X1 .X2 . . . Xn .
Lemma 2 is a basic property of a rewrite system commonly known as confluence andtermination (e.g. see [1]). In fact, it does not take long to terminate. Lemma 3 gives theτform of the unique “minimal” term with respect to −→ given various different initialstarting points. The proofs of these lemmas are standard. For the rest of the proof of
Theorem 1, we assume the following conventions:τConvention 4 The term t0 and all process terms in P are minimal with respect to −→.
That is, each of such terms t satisfies t = t↓ .
a

We now add these τ -transitions into T0 (P). So, we will write T0 (P) = (G(Σ), Aτ , {−→:a ∈ Aτ }). Our first technical result is that the equivalence relation ≡ is indeed a branching bisimulation on T0 (P).
Lemma 5. ≡ is a branching bisimulation on T0 (P).
The proof of this lemma is not difficult but tedious. As an immediate corollary, we
obtain that (T0 (P), t0 ) is equivalent to (T (P), [t0 ]≡ ) up to branching bisimulation.
Corollary 6. The relation R = {(C, t) ⊆ S ′ × S : t ∈ C} is a branching bisimulation
between T (P) and T0 (P).
Removing complex τ -transitions: Corollary 6 implies that we may restrict ourselvesto the transition system T0 (P). At this stage, our τ -transitions still contain some rulesthat cannot easily be captured in the framework of GTRS, e.g., left-associativity ruleof the sequential composition. We will now show that fixing an initial configuration t0
allows us to remove these τ -transitions from our systems.
8

Recall that our initial configuration t0 satisfies t0 = (t0 )↓ . Denote by W the set of
all subtrees (either of t0 or of a left/right side of a rule in P) rooted at a node that isa right child of a .-labeled node. It is easy to see that Convention 4 implies that eacht ∈ W satisfies t = t↓ . Consequently, each t ∈ W cannot be of the form t1 .t2 or 0
since t is a right child of the sequential composition. Furthermore, |W | is linear in thesize of P.
Lemma 7. Fix a term t ∈ post∗ (t0 ) with respect to T0 (P). Then, any subtree of t which
is a right child of a .-labeled node is in W .
This lemma can be easily proved by induction on the length of the witnessing path thatt ∈ post∗ (t0 ) and that this invariant is always satisfied. This lemma implies that someτof the rules for defining −→ may be restricted when only considering post∗ (t0 ) as thedomain of our system, resulting in the following simplified definition:ττ

0.t −→ tτ

0kt −→ tt∈Wt1 −→ t′1ττ

t1 .t2 −→ t′1 .t2

tk0 −→ tt2 ∈ Wτ

t2 −→ t′2τ

t1 −→ t′1τ

t1 kt2 −→ t′1 kt2τ

t1 kt2 −→ t1 kt′2
τObserve that the rule t.0 −→ t may be omitted since no subtree of t ∈ post∗ (t0 ) of theτform u.0 exists. Moreover, the rule t1 .(t2 .t3 ) −→ (t1 .t2 ).t3 is never applicable since no∗subtree of t ∈ post (t0 ) of the form t1 .(t2 .t3 ) exists. Other rules are omitted because
any subtree of t of the form t1 .t2 must satisfy t2 ∈ W , and that each u ∈ W satisfies
τu = u↓ (which implies u −→).
6
Finally, in order to cast the system into GTRS framework, we will further restrictττ
rules of the form tk0 −→ t or 0kt −→ t. Let l-prefix(P) be the set of all prefixes
of words w appearing on the left hand side of the rules in P treated as left-associative
terms. More formally, l-prefix(P) contains 0 (a term representation of the empty word)
and all subterms u of a term appearing on the left hand side of a rule in P rooted at aτnode location of the form 1∗ . We define τ to be the restriction of −→, where rules ofττ
the form 0kt −→ t and tk0 −→ t are restricted to t ∈ l-prefix(P). We let T0′ (P) to beτT0 (P) with −→ replaced by τ .
Lemma 8. (T0′ (P), t) is branching bisimilar to (T0 (P), t).
Constructions of the GTRS: It is now not difficult to cast T0′ (P) into GTRS framework. To construct the GTRS, we let A be the ranked alphabet containing: (i) a nullarysymbol for each process variable occuring in P, (ii) a binary symbol for the binary operator k, and (iii) a unary symbol t̂ for each term t ∈ W . Since each subtree u of a treet ∈ post∗ (t0 ) of the form t1 .t2 satisfies t2 ∈ W , we may simply substitute u with thetree tˆ2 (t1 ) and perform this substitution recursively on t1 . Denote by λ(t) the resulting
tree over the new alphabet A after this substitution is performed on a process term t. The
desired GTRS is R = (A, Aτ , R), where R is defined as follows. For each rule t 7→a t′
ain P, where a ∈ A, we add the rule λ(t) ֒→ λ(t′ ) to R. For each t ∈ l-prefix(P),τττwe add 0kt ֒→ t and tk0 ֒→ t to R. Finally, we add the transition rule t̂(0) −→ t for′each t ∈ W . It is now not difficult to show that (T0 (P), t) ≃ (T (R), λ(t)), which
immediately implies Theorem 1.
94.2 Further containment results
Theorem 9. BPP ≤∼ GTRS.
Proof (sketch). The idea is to construct from some BPP a GTRS, where each leaf corresponds to a process constant. A leaf is either marked or unmarked. An unmarked
leaf X can become marked with the fresh symbol $ via the action a in case the rule
X 7→a 0 is present in the BPP. Rules of the kind X 7→a Y1 k . . . kYn are realized viaaX ֒→ •(Y1 , . . . , Yn ) in the GTRS. Moreover the GTRS does not contain any rules,
where a marked leaf is on the left-hand side of a rule.
⊓⊔
Theorem 10. GTRS ≤∼ PRS.
Proof (sketch). Let k be the maximal rank of the alphabet of some GTRS. Althoughparallel composition is interpreted commutatively we can simulate order by using k
additional symbols in a PRS.
⊓⊔
Theorem 11. RGTRS ≃ GTRS.
Proof (sketch). A GTRS can simulate via τ -transitions the bottom-up computation ofan NTA. In addition, one provides τ -transitions that allow to undo these transitions. ⊓⊔In analogy to Theorem 11 one can prove the following.
Corollary 12. PDS ≃ PREF.

5 Separation results
In this section, we provide the separation results in the two refined hierarchies. We firstnote two known separation results: (1) BPA 6≤≈ PN (e.g. see [10]), and (2) BPP 6≤≈
PDS since there is a BPP trace language that is not context-free (e.g. see references in[4]) and trace equivalence is coarser than weak bisimulation equivalence.
5.1 PA 6≤∼ GTRS
Some properties of GTRS: We introduce some notions that were also used in [15].
Let R = (A, A, R) be an arbitrary GTRS. For each t ∈ TreesA , we define height(t) =max{|x| : x ∈ Dt }. We define the number hR = max{height(t) | ∃t′ ∈ TreesA ∃σ ∈Pσσσ
A : t ֒→ t′ ∈ R or t′ ֒→ t ∈ R} and |R| = |A| + |A| + t֒→t|t| + |t′ |.
′ ∈RLemma 13. Let Λ ⊆ A. For every t0 ∈ TreesA there is some N = exp(|R| +
Λ N

Λ n

→ for infinitely many n ∈ N.
→ implies t0 −height(t0 )) such that t0 −The separating PA: Consider the PA P = (Σ, A, ∆) with Σ = {A, B, C, D}, A ={a, b, c, d} and where ∆ consists of the following rewrite rules:
A 7→a 0

B 7→b 0C 7→c 010

D 7→d 0

A 7→a A||B||C

For the rest of this section, we wish to provethat the state α = A.D in T (P) is not strongly
bisimilar to any pointed GTRS. So for the sakeof contradiction, let us assume some GTRS R =(A, A, R) and some tα ∈ TreesA (R) with tα ∼x
α. We note that e.g. by [15] it is known that theU
set of maximal sequences executable from α (thelanguage of α when P is interpreted as a languageyacceptor) are recognizable by some GTRS [15].
V
We call U [x] a context if U ∈ TreesA and x ∈tB
DU is a leaf of U . Given a tree t ∈ TreesA and acontext U [x], we write U [t] for U [x/t]. We define
U n [t] inductively as follows: U 0 [t] = t and U n =U [U n−1 [t]] for each n > 0.
Fig. 2. The tree T 1 = U [V [tB ]].
∗Let us consider post{a} (tα ). First, there issome NTA A with L(A) = {tα }. A folklore result states that there is some NTA B
with L(B) = post∗{a} (L(A)) = post∗{a} (tα ), see e.g. [15]. Note that L(B) is infinite
since α can reach infinitely many pairwise non-bisimilar states and tα ∼ α by assumption. By applying the Pumping Lemma for regular tree languages, there is some treetB ∈ TreesA and there are contexts U [x], V [y] ∈ TreesA such that (i) U [V [tB ]] ∈ L(B),(ii) height(U [V [tB ]]) ≤ 2 · |B|, (iii) height(V [tB ]) ≤ |B|, (iv) |y| > 0, i.e. V is not asingleton tree, and (v) U [V n [tB ]] ∈ L(B) for each n ≥ 0.
The tree U [V [tB ]] is displayed in Figure 2. We define the tree T n = U [V n [tB ]]for each n ≥ 0. Moreover we define the consant γ = ℓ · (hR + 1) with ℓ =2|{t∈TreesA |height(t)≤hR }| , i.e. ℓ denotes the number of different subsets of the set of alltrees in TreesA of height at most hR .
The following lemma states that if V γ [tB ] can reach some tree of height at most hR
by only executing the action σ, then there is already some tree tσ of height at most hσ
σ ∗such that for all i ≥ 0 we have V θ+i·δ [tB ] −→ tσ .
R

σ ∗Lemma 14. There exist θ, δ ≥ 1 such that if V γ [tB ] −→ t for some t ∈ TreesA with
σ ∗
θ+i·δ
height(t) ≤ hR , then V[tB ] −→ tσ for all i ≥ 0 for some tσ ∈ TreesA .
R

For the rest of this section, we fix θ and δ from Lemma 14. Note that due to tα ∼ α wea k→ t. Thus,
have that for every t ∈ post∗{a} (tα ) there is some unique k ∈ N with tα −a kfor each tree t ∈ post∗{a} (tα ) we define k(t) to be the unique k with tα −→ t.
Lemma 15. {k(T n ) | n ∈ N} is an infinite set.
Let us immediately apply Lemma 15. Let us fix some residue class r modulo δ suchthat there are infinitely many n with n ≡ r mod δ all having pairwise distinct k(T n )values. Among these infinitely many n we will choose a sufficiently large N ≥ θ forthe following arguments to work. The tree TN is depicted in Figure 3. Recall that bydefinition T N ∈ post∗{a} (tα ).
The following lemma states that one can never shrink the subtree V γ [tB ] of T N tosome tree of height at most hR by only executing b’s or only executing c’s.
11

σ ∗

Lemma 16. If V γ [tB ] −→ t, then we have height(t) > hR for each t ∈ TreesA andeach σ ∈ {b, c}.
Let yN denote the unique node of T N where the subtree tB is rooted at. We call anode z ∈ DT N of T N off-path
if z 6 yNo. For each tree t ∈ TreesA and each σ ∈ A,
n
σ j
→ .
we define supσ (t) = sup j ∈ N | t −Intuitively speaking, the following lemma states thatfrom the subtree V γ [tB ] of T N and subtrees of T N thatare rooted at off-path nodes one only execute a constantly
long sequences from b∗ c∗ or from c∗ b∗ (unless tα ∼ α isviolated). Let us define b = c and c = b. We note that γ
and B only depend on R and on tα but not on N .

..

Lemma 17. Let σ ∈ {b, c}. Then there is some constant
J = J(R, tα ) such that supσ (t) ≤ J whenever eitherγt = V [tB ] or T∗
N ↓z σ−→ t for some off-path z.

We can now prove the main result of this section.
Theorem 18. PA 6≤∼ GTRS.

Dγ (tB )Proof. We give a simple winning strategy for Attacker that
a k(T

N

)

→
T N.
contradicts tα ∼ α. First Attacker plays tα −We remark since N is chosen sufficiently large, it follows
that k(TN ) is sufficiently large for the following arguments
to work. It has to hold for some s ∈ {0, 1}


T

N

∼

 1−s

A k BkB · · · kB k CkC · · · kC  .D
|
{z
} |
{z
}
k(T N )−s



































..

yN

Fig. 3. The tree T N .
(⋆)

k(T N )−s

We only treat the case s = 1 (the case s = 0 can be proven analogously). Recall that
γ is a constant that only depends on R and tα . On the one hand we cannot modify thesubtree V γ [tB ] of T N to any tree of height at most hR by executing b’s only by Lemma
16. On the other hand we cannot execute more than J many b’s from the subtree V γ [tB ],
b k(T

N

)−1

where J is the constant of Lemma 17. Thus, since T N −→holds, Attacker canplay k(T N ) − 1 − J many b’s outside the subtree V γ [tB ]. We recall that k(T N ) − J canbe arbitrarily large since J is a constant that only depends on R and tα . By definition
of T N all of these k(T N ) − 1 − J many b’s can be played on subtrees initially rooted at
off-path nodes of T N outside the subtree V γ [tB ]. However from each of these subtreesthat are initially rooted at off-path nodes outside the subtree V γ [tB ], we can execute at
most J many b’s.
Analogously Attacker can execute k(T N )− 1 − J many c’s from T N all on subtrees
initially rooted at off-path nodes of TN outside the subtree V γ [tB ].
Attacker now has the following winning strategy. First he plays k(T N )−1−J manyb’s on subtrees rooted at off-path nodes of T N outside V γ [tB ]. After playing these b’s
12the height each of these subtrees is bounded by a constant that only depends on R andtα by Lemma 17. Next, Attacker plays k(T N ) − 1 − J many c’s at positions outside
the subtree V γ [tB ] and still, by Lemma 17, the height of all subtrees rooted at off-path
nodes outside V γ [tB ] have a height bounded by a constant that only depends on R andbJ cJ dtα . Let us call the resulting tree T ′ . We note that T ′ −−−−→, i.e. from T ′ the sequencebJ cJ is executable thus reaching a tree where a d-labeled rule is executable. But thiswd
implies that T N −−→ for some w ∈ {b, c}∗ where |w| is bounded by a constant that
only depends on R and tα , clearly contradicting (⋆).
⊓⊔
5.2 GTRS 6≤≈ PAD
By Theorem 11 it suffices to prove that there is some RGTRS that is not weakly bisimilar to any PAD.
Consider the RGTRS R = (A, A, R), with A0 = {X0 , Y0 , Z0 }, A1 = {X1 , Y1 },A2 = {•}, and A = {a, b, c, d, e, f }. First, we add to R the following singleton rewrite
a

b

c

d

rules: (i) X0 ֒→ X1 (X0 ), (ii) X1 (X0 ) ֒→ X0 , (iii) Y1 ֒→ Y1 (Y0 ), (iv) Y1 (Y0 ) ֒→ Y0 ,eand (v) •(X0 , Y0 ) ֒→ Z0 .
..
.
We note that so far all rewrite rulest(0, 2)are standard ground tree rewrite rules.
Also note that the singleton tree Z0 is adead-end. It is easy to see that for evc..
ery tree in t ∈ TreesA that is reachdb.
able from •(X0 , Y0 ) we have t = Z0 ort(0, 1)t(1, 1) · · ·t is of the form t = •(tX , tY ), whereatX = X1m [X0 ] and tY = Y1n [Y0 ] for fccdsome m, n ≥ 0. In the latter case we de..
dbb.
note t by t(m, n). Finally, we add to Rft(0, 0)t(1, 0)t(2, 0)
the regular tree rewrite rule {t(m, n) |faan ≥ 1 or m ≥ 1} ֒→ Z0 . The transie
ftion system T (R) is depicted in Figure
f
Z0
4.
f
It is easy to see that the set of maximal sequences executable from t(0, 0)
Fig. 4. The transition system T (R).
is not a context-free language. We claimthat there is no PAD that is weakly bisimilar to t(0, 0) = •(X0 , Y0 ).
Let us assume by contradiction thatfor some PAD P = (Σ, Aτ , ∆) and for some term α0 ∈ G(Σ) we have α0 ≈ t(0, 0).
στ
We call a term α ∈ G(Σ) inactive if α =⇒6
for all σ ∈ A. We note that α =⇒ might bepossible even though α is inactive.

Lemma 19. Assume some term α with α ≈ t(m, n) for some m, n ∈ N and α contains
an enabled subterm β1 kβ2 . Then β1 or β2 is inactive.
Theorem 20. GTRS 6≤≈ PAD.
13

Proof (sketch). The proof idea is to show that any PAD that satisfies the property ofLemma 19 is already weakly bisimilar to a pushdown process.
5.3 PDS 6≤≈ PAN and PN 6≤≈ GTRS
Theorem 21. PDS 6≤≈ PAN.
Proof (sketch). The proof idea is an adaption of an idea from [18] separating PAN
from PDS with respect to strong bisimulation, but is technically more involved. The
separating pushdown process behaves as follows: First, it executes a sequence of actions
w = {a, b}∗ and then executes either of the following: (1) The action c, then the reverseof w and finally an e. (2) The action d, then the reverse of w and finally an f .
⊓⊔Theorem 22. PN 6≤≈ GTRS
The proof can be done by observing that {an bn cn | n ∈ N} is a PN language (e.g. see[22]), while this language is not a trace language of GTRS (e.g. see [15]).

6 Applications
In this section, we provide applications of the connections that we establish between
GTRS and the PRS hierarchy. Instead of attempting to exhaust all possible applications,
we shall only highlight a few of the key applications. In particular, Theorem 1 allows
us to transfer decidability/complexity upper bounds on model checking over GTRS tomodel checking over PA/PAD-processes.
The first application is the decidability of EF-logic over PAD. The logic EF (e.g. see[13, 23]) is the extension of Hennessy-Milner logic with reachability operators (possibly parameterized over subsets of all possible actions). The decidability of EF model
checking over GTRS has been known for a long time, e.g., it follows from the results of[8, 12]. Together with Theorem 1, this easily gives another proof of the following resultof Mayr.
Theorem 23 ([19]). Model checking EF-logic over PAD is decidable.
The second application is the decidability/complexity of model checking the common fragments LTLdet (called deterministic LTL) and LTL(Fs , Gs ) [7, 17] of LTL over
PAD. These fragments are suffciently powerful for expressing interesting properties
like safety, fairness, liveness, and also some simple stuttering-invariant LTL properties.
The following two theorems follow from the results for GTRS [23, 24]; decidability
with no upper bounds was initially proven in [7].
Theorem 24. Model checking LTLdet over PAD is decidable in exponential time in thesize of the formula and polynomial in the size of the system. Model checking LTL(Fs , Gs )over PAD is decidable in time double exponential in the size of the formula and polynomial in the size of the system.
Acknowledgment: We thank Taolue Chen, Matthew Hague, Jean Christoph Jung,
Richard Mayr, Colin Stirling, and anonymous reviewers for their comments. Anthony
W. Lin is supported by EPSRC (EP/H026878/1).
14

References
1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
2. J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Decidability of bisimulation equivalence
for processes generating context-free languages. In J. W. de Bakker, A. J. Nijman, and P. C.
Treleaven, editors, PARLE (2), volume 259 of Lecture Notes in Computer Science, pages
94–111. Springer, 1987.
3. J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theor.
Comput. Sci., 37:77–121, 1985.
4. A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregularproperties for nonregular processes. In LICS, pages 123–133. IEEE Computer Society, 1995.
5. A. Bouajjani, M. Müller-Olm, and T. Touili. Regular symbolic analysis of dynamic networksof pushdown systems. In M. Abadi and L. de Alfaro, editors, CONCUR, volume 3653 of
Lecture Notes in Computer Science, pages 473–487. Springer, 2005.
6. A. Bouajjani and T. Touili. Reachability analysis of process rewrite systems. In P. K. Pandya
and J. Radhakrishnan, editors, FSTTCS, volume 2914 of Lecture Notes in Computer Science,
pages 74–87. Springer, 2003.
7. L. Bozzelli, M. Kretı́nský, V. Rehák, and J. Strejcek. On decidability of LTL model checking
for process rewrite systems. Acta Inf., 46(1):1–28, 2009.
8. W. S. Brainerd. Tree generating regular systems. Information and Control, 14(2):217–231,
1969.
9. O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In
Handbook of process algebra, pages 545–623. Elsevier, North-Holland, 2001. Chapter 9.
10. S. Christensen. Decidability and Decomposition in Process Algebras. PhD thesis, Department of Computer Science, The University of Edinburgh, 1993.
11. 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.
12. M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In LICS, pages
242–248. IEEE Computer Society, 1990.
13. S. Göller and A. W. Lin. The Complexity of Verifying Ground Tree Rewrite Systems. In
LICS. IEEE Computer Society, 2011. to appear.
14. M. H. T. Hack. Decidability Questions for Petri Nets. PhD thesis, MIT, 1976.
15. C. Löding. Infinite Graphs Generated by Tree Rewriting. PhD thesis, RWTH Aachen, 2003.
16. D. Lugiez and P. Schnoebelen. The regular viewpoint on pa-processes. Theor. Comput. Sci.,
274(1-2):89–115, 2002.
17. M. Maidl. The common fragment of CTL and LTL. In FOCS, pages 643–652, 2000.
18. R. Mayr. Process rewrite systems. Inf. Comput., 156(1-2):264–286, 2000.
19. R. Mayr. Decidability of model checking with the temporal logic ef. Theor. Comput. Sci.,
256(1-2):31–62, 2001.
20. R. Milner. Communication and Concurrency. Prentice Hall, 1989.
21. D. E. Muller and P. E. Schupp. The theory of ends, pushdown automata, and second-orderlogic. Theor. Comput. Sci., 37:51–75, 1985.
22. W. Thomas. Applied automata theory. Course Notes (RWTH Aachen), 2005.
23. A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD
thesis, LFCS, School of Informatics, University of Edinburgh, 2010.
24. A. W. To and L. Libkin. Algorithmic metatheorems for decidable LTL model checking
over infinite systems. In C.-H. L. Ong, editor, FOSSACS, volume 6014 of Lecture Notes in
Computer Science, pages 221–236. Springer, 2010.
25. R. J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation
semantics. J. ACM, 43(3):555–600, 1996.

15