Termination Condition for Equivalence Checking Algorithm of PDA
Yuxi Fuaa BASICS, Department of Computer Science, Shanghai Jiao Tong University, China

Abstract
Equivalence checking of PDA processes is a hard problem. After Senizergues’ first proof, several simplifications of
the proof methodology have been given. A central issue in the proofs is the termination of the decidability algorithms.
In the paper two termination conditions are proposed. They are sufficient for converting a strong bisimulation to a
finite tree called generating tree in such a way that the former can be recovered from the latter. A simple proof of thedecidability of the strong bisimilarity of PDA is then available by guessing a tree for a pair of input PDA processes
and checking if the tree satisfies the desirable properties of generating tree.
Keywords: Pushdown automata, bisimulation, equivalence checking

1. Introduction
After the pioneering work of Baeten, Bergstra and Klop [1], algorithmic study of equivalence checking has beenan active line of research [18]. Checking equivalence for pushdown automata, PDA for short, is a very hard problem.
Early attention was paid to language equivalence of deterministic pushdown automata (DPDA) [11]. The restriction
to DPDA is not just technical; the language equivalence of general PDA is in fact undecidable [12]. The problem wasopen for a long time before Sénizergues announced that it is decidable [22]. The original proof is very long [24]. Simplified proof appeared soon afterwards [26]. Sénizergues also proved using his approach that the strong bisimilarity
of PDA is decidable [23]. The full proof is also quite long [27].
The shift from language equivalence to bisimulation equivalence opened door to process algebraic approach [13,31]. Stirling has given a decidability proof of normed PDA using tableaux method [29, 30]. Later he applied the same
method to the general PDA in an unpublished paper [32]. The tableau approach is also used to provide a simplified
proof of the DPDA problem [33, 34]. Jančar addressed the issue using Prover-Refuter game in the setting of firstorder grammar (FOG), which is a proper generalization of PDA. This has been done for the strong bisimilarity of
FOG [16, 17] and the language equivalence of deterministic FOG [14].
A key technical issue in any equivalence checking algorithm for PDA is termination. In Stirling’s tableaux approach rules must be backward sound, and a consecutive applications of rules must terminate. Starting from a pairof equivalent processes soundness in Jančar’s game theoretical framework means that Refuter should never win thegame, and termination says that Prover is able to demonstrate to Refuter in a finite number of steps that the latter will
never win the game. We will give a proof of the decidability of the strong bisimilarity of PDA in which the argument
for termination is simplified. Our contributions are twofold. Firstly we propose two new termination conditions.
One condition deals with sequences of pairs of bisimilar PDA processes of the form (qZ, H0 ), (qZ, H1 ), (qZ, H2 ), . . .
where qZ is unnormed. These bisimilar pairs need special treatment for the reason that the size of Hi may keepincreasing while i increases. The second termination condition seeks finite structure in sequences of the form
(A0 σ, B0 σ), (A1 σ, B1 σ), (A2 σ, B2 σ), . . ., where the processes share the same suffix σ and the size of the prefixes Ai
and Bi may keep increasing while i increases. Our decidability algorithm follows Stirling’s approach. But instead ofusing tableaux, we introduce bisimulation trees. Bisimulation trees have the advantage that they are easy to compose
and can be generalized to deal with silent transitions in a straightforward manner. By applying the two termination

Email address: fu-yx@cs.sjtu.edu.cn (Yuxi Fu)
Preprint submitted to Elsevier

August 6, 2018

conditions to bisimulation trees we are able to give a simpler proof of the decidability of the strong bisimilarity of
PDA. In view of the importance of PDA in equivalence checking and programming theory, especially in automatic
verification, any effort to simply the decidability proof is worthwhile. A simpler proof is what is necessary to help
expose the problem and its proof technique to a wider audience.
The rest of the paper is structured as follows: Section 2 fixes the syntax and the semantics of PDA. Section 3
introduces the important notion of bisimulation tree. Section 4 looks at algebraic structures of bisimulation trees.
Section 5 defines a nondeterministic algorithm that outputs a finite representation of a bisimulation tree when it terminates successfully. Section 6 provides a semidecidable procedure to check the strong bisimilarity of PDA processes
by enumerating possible finite representations for a bisimulation tree. Section 7 comments on related works.
2. Pushdown Automata
A pushdown automaton, PDA for short, is a tuple P = (Q, V, L, R) where• Q = {p1 , . . . , pq } is a finite set of state ranged over by o, p, q, r, s, t,• V = {X1 , . . . , Xn } is a finite set of symbol ranged over by X, Y, Z,• L = {a1 , . . . , as } is a finite set of letter ranged over by a, b, c, and• R is a finite set of transition rules.
The notation S∗ stands for the set of finite strings of elements of S, and  for the empty string. We write u, v, w forwords, the elements of L∗ , and small Greek letters for stacks, the elements of V∗ . We write αδ for the concatenationof α and δ. A P-process, or process, is denoted by pα, where p ∈ Q and α ∈ V∗ . We write the capital letters A, . . . , T
for P-processes. We use = for grammar equality. The size |pα| of pα is the same as the length |α| of α. If P = pα thenaPδ = pαδ. A transition rule in R is of the form pX −→ qα. The semantics of P is defined by the following ruleapX −→ qα ∈ R
a

.

(1)

pXσ −→ qασ
w

a1



ak

We write −→ for −→ . . . −→ if w = a1 . . . ak , and we identify −→ to =. We say that P0 is a descendant of P, and thatw
P is a ancestor of P0 , if P −→ P0 for some w. By definition P is a descendant of itself.
a

b

a

b

An example PDA is defined by P = ({p}, {X, Z}, {a, b}, {pX −→ p, pX −→ p, pZ −→ pZ, pZ −→ pZ}). It should
be clear that pX n Z and pZ have the same behaviour, where X n is the n copies of X concatenated one after another.
w
Given a number, say n, the notation [n] stands for the finite set {1, . . . , n}. Let ∂P denote the set {i | ∃w.P −→ pi }.
w
For i ∈ [q] the norm of P at i, denoted by kPki , is the size of a shortest word w such that P −→ pi . If there is no sucha word, kPki = ω. A process P is normed if ∂P , ∅; it is unnormed otherwise. An important parameter of a PDA is
the following.
m = max max {kpXki | i ∈ ∂pX} + 1.
(2)
p∈Q,X∈V i∈[q]

In fewer than m steps a sequence of transitions from pXα can expose pi α for every i ∈ ∂pX. Another parameter usedin the decidability algorithm is
r = maxp∈Q,X∈Va|α| | pX −→ qα ∈ R .

(3)

The parameter r is easy to calculate, and the parameter m can be calculated from the definition of the PDA by dynamic
programming [14].
w0w

A transition sequence pXα −→ pi α is a decreasing path if |w| = kpXki . If α = Yβ and pi α −→ pk β is a decreasing
ww0

path, we get a longer path pXα −→ pk β that is decreasing. A consecutive sequence of decreasing paths will be calledaa long decreasing path. Now suppose α = Z and pi Z is unnormed. We think of every transition pi Z −→ qδ as av
av
wav
decreasing step. If qδ −→ rγ is a long decreasing path, then both pi α −→ rγ and pXα −→ rγ are also long decreasing
au

a0 u0

a00 u00

ak uk

paths. A long decreasing path from pi Z typically takes the form pi Z −→ pi0 Z 0 −→ pi00 Z 00 −→ . . . −→ pik+1 Z (k+1) .
2

3. Bisimulation Tree
Two equivalence relations for PDA have been intensively studied. They are language equivalence and bisimulationequivalence [20, 21]. The former is undecidable in general [12]. The latter is the equivalence we study in this paper.
We fix some notations first. Suppose R, S are binary relations on processes, and {Ri }i∈I is a set of relations. We will
use the infix notation PRQ for (P, Q) ∈ R. The notation R−1 stands for {(Q, P) | (P, Q) ∈ R}, R; S for the composition
S{(P, Q) | ∃M.PRM ∧ MSQ}, and i∈I Ri for the union. The following definition is standard [29, 30, 32, 33].
Definition 1. A binary relation R on processes is a strong simulation if the following statements are valid.
aa

1. If P R Q −→ Q0 then P0 exists such that P −→ P0 RQ0 .
2. If Q = r then P = r.
The relation R is a strong bisimulation if both R and R−1 are strong simulations. The strong bisimilarity ∼ is thelargest strong bisimulation.
It is easy to see that the strong bisimilarity is both an equivalence and a congruence. Thus Pσ ∼ Qσ wheneverP ∼ Q. The equivalence property makes use of the fact that the composition of two strong bisimulations is a strong
bisimulation and the union of a family of strong bisimulations is a strong bisimulation [20]. Clause 2 of Definition 1
is unusual. Without it one would have p ∼ q for distinct p, q, and the congruence property would be lost.
If P is unnormed then Pσ ∼ P. We shall use the convention that A is normed whenever we write AZ. The next
lemma follows immediate from the definition of strong bisimulation.
Lemma 2. If P ∼ Q then ∂P = ∂Q and kPki = kQki for all i ∈ ∂P.
To help study our equivalence checking problem we will use a constructive version of Definition 1. Let k be anatural number and (P, Q) be a pair of processes. A k-bisimulation tree T for (P, Q) is a finite tree whose edges arelabeled by elements of L and whose nodes are labeled by pairs of process. For simplicity we shall identify a nodeawith its label. Accordingly we write (M, N) −→ (M 0 , N 0 ) for an edge labeled a from a node labeled (M, N) to a node
0 0labeled (M N ). Formally a k-bisimulation tree T for (P, Q) is defined as follows:
1. The root of T is (P, Q).
2. If P = Q, the node (P, Q) is a leaf. It is called an i-leaf. And the one-node tree is a 0-bisimulation tree for (P, Q).
3. If k > 0 and P, Q are distinct, then every child (P0 , Q0 ) is the root of a k0 -bisimulation tree for (P0 , Q0 ) for some
k0 < k, and there is at least one child that is the root of a (k−1)-bisimulation tree. Moreover the following
statements are valid.
aaa(a) If (P, Q) −→ (P0 , Q0 ), then P −→ P0 and Q −→ Q0 .
a
a
a
a
a
(b) If P −→ P0 then Q −→ Q0 for some Q0 such that (P, Q) −→ (P0 , Q0 ). If Q −→ Q0 then P −→ P0 for someaP0 such that (P, Q) −→ (P0 , Q0 ).
A k-bisimulation tree has k + 1 levels, with the root being at the 0-th level. Its height is k. A (k+1)-bisimulation tree T0
extends a k-bisimulation tree T, notation T @ T0 , if T can be obtained by cutting off the leaves of T0 at the depth k + 1.
If Ti @ Ti+1 for all i ≥ 0 and T0 is the one node tree for (P, Q), then the limit of the chain T0 @ T1 @ . . . @ Ti @ . . . iscalled an ω-bisimulation tree for (P, Q). Intuitively an ω-bisimulation tree is built up level by level. Starting from theroot (P, Q), the trivial tree T0 , one constructs the nodes at the first level. After completing T1 one constructs the nodes
at the second level. We will also say that the tree is grown level by level. The tree-like structure is meant to help one
reason about strong bisimulations. The branching version of bisimulation tree was introduced in [9].
Not every path in an ω-bisimulation tree is infinitely long. A finite path ends up in a leaf. By the definition of
k-bisimulation, an i-leaf is a pair of identical processes. It is unnecessary to grow such a node since the equality
between two identical processes is self evident. We now introduce another kind of leaf. A node is an r-leaf if its label
coincides with the label of one of its proper ancestors. There is no need to grow an r-leaf because it can be grown inprecisely the same way the ancestor has been grown.
In a k-bisimulation tree a node at k0 -th level, where k0 < k, could be either an i-leaf or an r-leaf. If all the nodes
at the k-th level are either i-leaves or r-leaves, the tree is called a complete k-bisimulation tree, or simply a complete
bisimulation tree. A bisimulation tree is either a complete bisimulation tree or an ω-bisimulation tree. By the next
lemma it is not surprising that bisimulation trees play a central role in our decidability proof.
3

Lemma 3. P ∼ Q if and only if there is a bisimulation tree for (P, Q).
Proof. For a bisimulation tree T we write e
T for the set of the pairs appearing as labels in T. Let I denote the identity
relation on processes. By the definition of bisimulation tree e
T ∪ I is a strong bisimulation. If P ∼ Q, by the definitionof strong bisimulation we can construct T0 @ T1 @ . . . @ Ti @ . . . that ends up either with a complete bisimulation
tree for (P, Q) or an ω-bisimulation tree for (P, Q).

Lemma 3 implies that P ∼ Q whenever we can grow a bisimulation tree for (P, Q) level by level so that theconstruction either ends up in a complete bisimulation tree or is non-stopping.
Due to the finite branching property there are only finitely many k-bisimulation trees for (P, Q) for every k. If
for some k no k-bisimulation tree for (P, Q) exists, then P / Q. This simple observation suggests immediately asemi-decision procedure for /.
Lemma 4. The relation / is semi-decidable.
a

The composition of two k-bisimulation trees T and T0 , denoted by T; T0 , is defined as follows: If (L, M) −→a
0(L , M 0 ) is an edge in T from the i-th level to the (i+1)-th level and (M, N) −→ (M 0 , N 0 ) is an edge in T0 from the i-thalevel to the (i+1)-th level, then (L, N) −→ (L0 , N 0 ) is an edge in T; T0 from the i-th level to the (i+1)-th level. If (L, M)
is a node in T at the i-th level and (M, M) is an i-leaf in T0 at the i-th level, then the subtree rooted at (L, M) in T; T0
is the same as the subtree rooted at (L, M) in T. If (M, M) is both an i-leaf in T at the i-th level and an i-leaf in T0 at
the i-th level, it is also an i-leaf in T; T0 . It is easy to see that the composition T; T0 is a k-bisimulation tree. Similarly
the composition of two ω-bisimulation trees is an ω-bisimulation tree.
4. Periodic Structure of Bisimulation TreeIn Section 3 we have reduced the bisimilarity of a pair of processes to the existence of a bisimulation tree for the
pair. There is however no way to assert the existence of an ω-bisimulation tree for a pair if ω-bisimulation trees do
not exhibit any periodic structure. In this section we give an account of the periodic structure discussed in literaturein terms of k-bisimulation trees. We will make use of the periodic structure to design two strategies that constain thegrowth of bisimulation trees. We will also explain the first termination condition.
Before we proceed, let’s explain the idea of saturated bisimulation tree. Suppose P ∼ Q. We can grow a bisimulation tree for (P, Q) level by level. We say that a k-bisimulation tree for (P, Q) is saturated if for every internal nodeaaa(P0 , Q0 ) of the k-bisimulation tree whenever P0 −→ P00 and Q0 −→ Q00 such that Q00 ∼ P00 then (P0 , Q0 ) −→ (P00 , Q00 )is an out-going edge from (P0 Q0 ). A saturated k-bisimulation tree for (P, Q) is the largest k-bisimulation tree for (P, Q).
For that reason we may refer to a saturated k-bisimulation tree for (P, Q) as the k-bisimulation tree for (P, Q). In therest of the paper we assume that all k-bisimulation trees for pairs of bisimilar processes are saturated.
4.1. Balance Strategy
Suppose |M| = m and |Mσ| > m + 1. Consider the equalitypXα ∼ Mσ.
a0

a1

ak−2

ak−1

(4)

For i ∈ ∂pX let pX −→ A1 −→ . . . −→ Ak−1 −→ pi  be a decreasing path. By definition there are N1 , . . . , Nk−1 , Mi
a0
ak−2
ak−1
a1
such that (pXα, Mσ) −→ (A1 α, N1 σ) −→ . . . −→ (Ak−1 α, Nk−1 σ) −→ (pi α, Mi σ) is a path in the bisimulation treefor (pXα, Mσ). Clearly |N1 | > 0, . . . , |Nk−1 | > 0 and mr > |Mi | > 0. We will call the path a left decreasing path in
the tree. The left balance strategy makes use of the minimality of left decreasing paths to reduce imbalance between
a pair of processes that descends from (4). The degree of imbalance between A and B is measured by the number
minA0 ,B0 ,σ {|A0 |, |B0 | | A = A0 σ, B = B0 σ}. Formally for every i ∈ ∂pX, there is a left decreasing path from (pXα, Mσ)to (pi α, Mi σ) for some Mi such thatpi α ∼ Mi σ.
(5)41. If (P, Q) is an i-node or an r-node, stop growing.
2. If |P| ≤ m + 1 and |Q| ≤ m + 1, produce all children of (P, Q), and then apply BT to every child.
• A pair (M, N) is small if both |M| ≤ m + 1 and |N| ≤ m + 1.

3. If P = pXα and Q = Mσ such that |M| = m, |Mσ| > m + 1 and that M does not contain any constant, grow an(m−1)-bisimulation tree for (P, Q), but suspend the growth of every sink node temporarily.
• We call a node of the form (pi α, Mi σ) in the (m−1)-bisimulation tree a sink node. Notice that a sink node may appear
in the k-bisimulation tree for some k < m − 1.
• For each i ∈ ∂pX fix a sink node (pi α, Mi ) that can be reached from (pXα, Mσ) by a left decreasing path. These sinknodes define a normed constant U.
• We call a node at the (m−1)-th level that is of the form (Lα, Nσ), where |L| > 0, a nonsink node. To every nonsink
node (Lα, Nσ) we create the u-alias (LUσ, Nσ). We will explain how to grow the u-alias (LUσ, Nσ) in Section 4.2.

After growing the (m−1)-bisimulation tree, apply BT to every sink node, and apply the construction in Fig. 2
to every nonsink node.
4. If Q = pXα and P = Mσ such that |M| = m, |Mσ| > m + 1 and that M does not contain any constant, carry out
the construction symmetric to the one in Case 3.
Figure 1: Construction BT (P, Q) of a Bisimulation Tree for (P, Q) Satisfying P ∼ Q.

We introduce a mega stack symbol U, which we call a normed constant and which is called a simple constant in [29],defined by the following grammar equality:(
Mi , if i ∈ ∂pX,
pi U =(6)pi , if i < ∂pX.
For every i ∈ [q] the process pi U is normed, hence the terminology. The role of U is to transform (4) to pXUσ ∼ Mσ
by making use of the simple fact that pXα ∼ pXUσ. Algorithmically the pair (pXUσ, Mσ) is easier to deal with thanthe pair (pXα, Mσ) because in the latter the imbalance is controlled. The number of the normed constants is finite dueto the inequalities
0 < |Mi | ≤ mr.
(7)
Consequently there are only finitely many pairs (pXU, M).
Symmetrically suppose Mσ ∼ pXα such that |M| = m and |Mσ| > m + 1. There are right decreasing paths thatallow us to introduce a normed constant U 0 such that Mσ ∼ pXU 0 σ. The right balance strategy is then available inthis symmetric situation.
We now explain how to grow a bisimulation tree for a bisimilar pair (P, Q) with the help of the normed constants.
For that purpose we extend PDA with the normed constants. Every normed constant U = (M1 , . . . , Mq ) satisfies theinequalities (7) such that M1 , . . . , Mq are normed and none of M1 , . . . , Mq contains any constant. In an extended PDA
a stack is a finite string of stack symbols and normed constants. The definition of the strong bisimilarity remains
unchanged for the extended model. Suppose P ∼ Q. The construction of the bisimulation tree for (P, Q) is defined inFig. 1, where additional definitions and comments are inserted in small fonts. The whole idea of the semi-decidable
procedure BT is to grow a bisimulation tree while controlling the imbalance. If a pair (M, N) is small, grow it for one
level. The size of its children is bounded. If N is long, grow (M, N) using left balance strategy, and if M is long but N
is not, the right balance strategy is applied. The u-aliases created by the left/right balance strategy have bounded size
prefixes. In fact if we take the size of a normed constant as one, then
|LU| < mr and |N| < mr.

(8)

The way to deal with long common suffixes is explained in Section 4.2. So the construction BT gives rise to a partial
bisimulation tree in which the growth of the nonsink nodes is suspended. A sink node (pi α, Mi σ) is smaller in thesense that the left process pi α of the pair is smaller in size than pXα. The inductive nature of BT implies that if an
infinite path contains an infinite number of sink nodes, then one of the following situations must occur:5

1. It contains infinitely many sink nodes (qY, N0 ), (qY, N1 ), . . . , (qY, Ni ), . . . for some normed qY. In this case|Ni | < m for all i ≥ 0. Repetition must occur, and the construction ends in either an i-leaf or an r-leaf.
2. It contains infinitely many sink nodes (rZ, O0 ), (rZ, O1 ), . . . , (rZ, Oi ), . . . for some unnormed rZ and {Oi }i∈ω isbounded by some number. Repetition must occur, and the construction ends in either an i-leaf or an r-leaf.
3. It contains infinitely many sink nodes (rZ, O0 ), (rZ, O1 ), . . . , (rZ, Oi ), . . . for some unnormed rZ such that |Oi | >m + 1 for all i ≥ 0 and that no repetition happens. In this case we call (rZ, Oi ) an expansion node, Z the principal
variable and |Oi | the size of (rZ, Oi ).
We will see in Section 4.3 how to harness the nontermination in the last case.
4.2. Duplication Strategy
We explain now how to grow a u-alias (LUσ, Nσ) generated by BT defined in Fig. 1. The idea is that irrespectiveof the length of σ a bisimulation tree for (LUσ, Nσ) is a replica of a bisimulation tree for some pair (LUν, Nν) withbounded size suffix ν.
Fix a pair of processes (A, B). Although there could be an infinite number of σ such thatAσ ∼ Bσ,(9)the bisimulation trees for the pairs (Aσ, Bσ) that render (9) true are essentially finite in number. The way to demonstrate this finiteness property is to isolate the growth of some nodes of the form (pσ, Nσ) or (Nσ, pσ) from the rest of
the tree whose behaviour then can be completely described without dissolving the suffix σ. We introduce two gadgets
to simplify following account. One is an equivalence relation E on a subset of [q]. We write i ∈ E if i appears in an
equivalence class of E, and i < E if otherwise. We write hii for the equivalence class containing i. Initially E is thereflexive relation on [q]. The other is a family of equalities
pi V = Gi V,(10)

one for each i ∈ [q]. Initially Gi = pi  for all i ∈ [q]. We call V the recursive constant defined by the equalities (10).
Intuitively V is a mega stack symbol recursively defined such that the process pi V is the same as the process Gi V. If
Gi = pi  we identify Gi V to pi V. If (10) holds we write V(i) for Gi .
Now suppose the pair (Aσ, Bσ) satisfies (9). We can grow level by level a modified bisimulation tree, called thecharacteristic tree for (Aσ, Bσ) over σ. Suppose we have grown the k-characteristic tree Ck . For each leaf (pi σ, Nσ)
of Ck at the k-th level, carry out one of the following.
1. If i < E then replace the label (pi σ, Nσ) by (Gi σ, Nσ). We may think of the latter as an alias of the former. This
is why the bisimulation tree is modified. In this case neither E nor {pi V = Gi V}i∈[q] is changed.
2. If i ∈ E and |N| > 0, then update the equality family by letting pk V = NV for all k ∈ hii. Remove hii from E.
3. If i ∈ E and N = p j  for some j < E, then update the equality family by letting pk V = G j V for all k ∈ hii.
Remove hii from E.
4. If i ∈ E and N = p j  for some j ∈ E, then update E by merging hii with h ji.
A leaf of Ck at the k-th level that is of the form (Nσ, pi σ) is treated likewise. After all the k-th level nodes of Ck
have been dealt with, we grow Ck into Ck+1 . The updates of E and/or the equality family can only be carried out fora finite number of times. There must exist a number h such that all changes of E have happened in the constructionof Ch . After that the characteristic tree can be grown without ever changing E. We say that the characteristic tree C isessentially bounded by h. We need to modify the equality family for the final time. For each i ∈ E and each k ∈ hii
replace the equality pk V = pk V by pk V = pminhii V. By construction for each i such that pi V = Gi V and |Gi | , 0 there
is a node (pi σ, Gi σ) in Ch . We call such a node a recursive node. If (Aσ, Bσ) is some u-alias (LUσ, Nσ), then both
|A| and |B| are bounded by mr, confer (8). It follows that there exists some constant h0 such that
|Gi | < mr + h0 r
for all i ∈ [q].
6(11)For the u-alias (LUσ, Nσ) of a nonsink node generated by BT , grow the characteristic tree for (LUσ, Nσ) for h0 -levels,
which produces a recursive constant V.
Call every node (Cσ, Dσ) at the h0 -th level that is not a recursive node a balance node. In a balance node (Cσ, Dσ) both |C| <mr + h0 r and |D| < mr + h0 r. Thus there are only finitely many balance nodes and of course finitely many v-aliases.

1. Apply BT to every recursive node.
2. For every balance node (Cσ, Dσ) create the v-alias (CV, DV), and then apply BT to grow the v-alias.
Figure 2: Growth of U-Alias.

We will take every equality in {pi V = Gi V}i∈[q] as grammar equality. We say that V is undefined at j if p j V = pi V
for some i ≤ j such that Gi = pi .
To demonstrate the power of recursive constants we extend PDA model further with recursive constants. In the
new extended model every recursive constant V 0 is defined by equalities in the form of (10). We require that forevery i ∈ [q] either Gi contains no constant or it contains a normed constant that appears as the last symbol in Gi .
A stack may contain at most one recursive constant. A recursive constant may only occur as the last symbol in astack. For PDA’s extended with normed constants and recursive constants the definition of strong bisimulations need
be strengthened by including the following clause:
3) If Q = pi V 0 and V 0 is undefined at i, then P = pi V 0 .
By definition if pi V 0 = p j V 0 and V 0 is undefined at j, then pi V 0 ∼ p j V 0 .
We are now in a position to state some properties for the recursive constant V constructed from the bisimilar
processes in (9) and defined by the equalities in (10).
Lemma 5. AV ∼ BV.
Proof. If we substitute V for σ in the characteristic tree for (Aσ, Bσ) over σ, we get a bisimulation tree for (AV, BV),
bearing in mind the grammar equality in (10). We are done by applying Lemma 3.

We can also carry out the reverse transformation. Let T be a bisimulation tree for (AV, BV). Let T{σ/V} denotethe tree obtained from T by substituting σ for V. The next lemma implies that T{σ/V} is the characteristic tree for(Aσ, Bσ) over σ.
Lemma 6. If pi δ ∼ Gi δ for all i ∈ [q] then for all C, D such that |C| > 0 and |D| > 0, CV ∼ DV implies Cδ ∼ Dδ.
Proof. The composition ∼; {(Cδ, Dδ) | CV ∼ DV}; ∼ is easily seen to be a strong bisimulation.



In effect Lemma 6 allows us to decompose a bisimulation tree for (Aσ, Bσ) into the bisimulation tree for (AV, BV)
and bisimulation trees for the recursive nodes. The bisimulation tree for (AV, BV) acts as a blueprint. This would not
be very interesting if there are infinitely many blueprints.
Lemma 7. For fixed A, B there are only finitely many recursive constants generated by the bisimulation trees for thefamily {(Aσ, Bσ) | Aσ ∼ Bσ}σ∈V∗ .
Proof. The initial V is defined by the family {pi V = pi V}i∈[q] , which does not depend on any σ. In any step during
the construction of V, if AV / BV then there is a least k < h such that there is no k-bisimulation tree for (AV, BV). The
crucial point is that AV / BV does not depend on any σ. By the finite branching property there are only finitely manyk-bisimulation trees for Aσ ∼ Bσ with fixed A, B and varying σ. Consequently there are only finitely many ways to
update V.
Lemma 7 implies that there is a single constant, still denoted by h0 , such that the characteristic trees for all theu-aliases are essentially bounded by h0 . So we impose the condition (11) for all the recursive constants. We are now
in a position to complete the definition of BT . The growth of u-aliases is defined in Fig. 2.
7

The growth of a v-alias (CV, DV) may expose a normed constant in V. Suppose (p0 X 0 α0 UV, D0 β0 UV) is a descendant of (CV, DV) such that |D0 | = m and a normed constant U appears in both the left and the right processes.
Notice that neither α0 nor D0 β0 may contain any normed constants by our restriction on recursive constants. If the leftbalance strategy is applicable to (p0 X 0 α0 UV, D00 β0 UV), it introduces sink nodes of the form (pα0 UV, M 0 β0 UV) andnonsink nodes of the form (L0 α0 UV, N 0 β0 UV). A new normed constant U 0 is introduced, which does not contain any
occurrence of U. The u-alias of (L0 α0 UV, N 0 β0 UV) is (L0 U 0 β0 UV, N 0 β0 UV). The common suffix of L0 U 0 β0 UV andN 0 β0 UV is β0 UV. When growing the characteristic tree for (L0 U 0 β0 UV, N 0 β0 UV) over β0 UV, a new recursive constantV 0 , defined by say {pi V 0 = G0i V 0 }i∈[q] , is introduced. It is obvious that V 0 may contain U 0 as the last symbol in some
G0j , but it definitely does not contain any occurrence of U. We conclude that the construction defined in Fig. 2 only
introduces normed constants and recursive constants that meet our constraints. This fine property depends cruciallyon the requirement |Mσ| > m + 1 in the clause 3 and the clause 4 of the definition of BT . The requirement guarantees
that M contains no constant.
The construction of the characteristic tree over σ for (Aσ, Bσ) satisfying (9) can be generalized. Instead of startingfrom the trivial recursive constant V0 defined by V0 (i) = pi  for all i ∈ [q], we may begin with a nontrivial recursive
constant V00 such that pi σ ∼ V00 (i)σ for all i ∈ [q]. The way to construct the characteristic tree remains the same. The
result of the construction is the characteristic tree for (Aσ, Bσ) over σ extending V00 . Let V 0 be the recursive constantthus defined. We write V00  V 0 to indicate the fact that V 0 is defined from V00 .
4.3. Termination Condition for Balance Strategy
We now address the issue pointed out at the end of Section 4.1. The construction BT may not terminate because
there exists an infinite path in which there are an infinite number of expansion nodes. Observe that the length of aw
decreasing path (pX, qβ) −→ (p0 X 0 , q0 β0 ) is bounded by mr. In an (infinite) long decreasing path from (pX, qβ) there
must be some expansion node (q0 Z0 , H0 ) whose size is minimum. Now consider the infinite long decreasing path
w0

w j−1

w1

wj

w j+1

(q0 Z0 , H0 ) −→ (q1 Z1 , H1 ) −→ . . . −→ (q j Z j , H j ) −→ (q j+1 Z j+1 , H j+1 ) −→ . . . .

(12)

wj

The decreasing path (q j Z j , H j ) −→ (q j+1 Z j+1 , H j+1 ) is of length no more than mr. So (12) can be written as
w0

w j−1

w1

wj

w j+1

(q0 Z0 , G0 σ0 ) −→ (q1 Z1 , G1 σ0 ) −→ . . . −→ (q j Z j , G j σ0 ) −→ (q j+1 Z j+1 , G j+1 σ0 ) −→ . . .

(13)such that |G0 | ≤ mr and |G0 | ≤ |G j | for all j. For some k1 ≤ nmr we must have |G0 | < |Gk1 | for otherwise there would bea repetition. Clearly the length of the long decreasing path from (q0 Z0 , G0 σ0 ) to (qk1 Zk1 , Gk1 σ0 ) is bounded by mrnmr ,hence |Gk1 | < mrnmr r. Inductively define size function s(x) and time function t(x) as follows:
t(0)

=

0,

s(0)

=

mr,

t(i+1) =t(i) + mr(n+1) s(i) ,s(i+1) =s(i) + mr2 (n+1) s(i) .

Assume that there are some k1 < t(1), . . . , kn < t(n) such that 0 = k0 < k1 < k2 < . . . < kn , |Gki | < s(i) for alli ∈ [n], and |G0 | = |Gk0 | < |Gk1 | < . . . < |Gkn |. Then by the definition of t(n + 1) there must exist some kn+1 such thatt(n) < kn+1 < t(n + 1) and |Gkn | < |Gkn+1 |. Let t be the computable function defined as follows:
t(0)

=

0,

t( j+1)=t( j) + ms(t( j)).

Define the sequence(r0 Y0 , K0 σ0 ), (r1 Y1 , K0 σ1 ), . . .
by letting(r j Y j , K j σ0 ) =(qt( j) Zt( j) , Gt( j) σ0 )8(14)for all j ≥ 0. The function t is so defined to ensure that for all j the length of the long decreasing path from thenode (r j Y j , K j σ0 ) to the node (r j+1 Y j+1 , K j+1 σ0 ) is longer than the length of any long decreasing path from K j σ0 that
exposes σ0 . Consider the subsequence(r0 Y0 , K0 σ0 ), (r1 Y1 , K1 σ0 ), . . . , (rqn2q Yqn2q , Kqn2q σ0 )(15)that contains the first qn2q + 1 nodes in (14). The multiplier qn guarantees that in (15) there must be two expansion
nodes (r j Y j , K j σ0 ) and (r j0 Y j0 , K j0 σ0 ), where j < j0 , such that r j Y j = r j0 Y j0 = qZ for some qZ, and the multiplier 2q
ensures that K j = Ga and K j0 = Gb for some a and b such that
∂Ga = ∂Gb

(16)

|Ga | < s(t(qn2q )) and |Gb | < s(t(qn2q )).

(17)

and
The length of the long decreasing path from (qZ, Ga ) to (qZ, Gb ) is bounded byt(qn2q ).

(18)

Now grow the expansion node (qZ, Ga σ0 ) until the long decreasing path reaches (qZ, Gb σ0 ). By the property of (15)for every h ∈ ∂Ga a node of the form (Ch , ph σ0 ) satisfying
Ch ∼ ph σ0(19)

is generated at a level above the level that (qZ, Gb σ0 ) appears. The nice thing about (19) is that
|Ch | ≤ s(t(qn2q ))mr.

(20)

Now introduce a new constant W, called unnormed constant, defined by the following grammar equality:(
Ci , if i ∈ ∂Ga ,pi W =pi , if i < ∂Ga .

(21)

It follows from (21) and (20) that |pi W| ≤ s(t(qn2q ))mr for all i ∈ [q], and that both Ga σ0 ∼ Ga W and Gb σ0 ∼ Gb W. So
we may let (Ga W, Gb W) be an alias of the expansion node (qZ, Gb σ0 ), called the W-alias of (qZ, Gb σ0 ), and continue
to grow the W-alias. There cannot be an infinite path that contains an infinite number of W-aliases because there are
only finitely many W-aliases. We have therefore removed one cause of nontermination from BT . The constant W is
unnormed because Ci is unnormed for every i ∈ ∂Ga . So we may ignore the trailing α in Wα. A long decreasing pathfrom pW is essentially a long decreasing path from some p0 Z 0 . So it does not give rise to any new nondeterminism.
The introduction of the recursive constants opens up new possibility for nontermination. Infinite long decreasing
sequence of the following form is possible, where {|H j |} j∈ω is unbounded.
w0

w1

w j−1

wj

w j+1

(q0 V, H0 ) −→ (q1 V, H1 ) −→ . . . −→ (q j V, H j ) −→ (q j+1 V, H j+1 ) −→ . . . .

(22)

It ought to be clear that the sequence (22) can be treated in completely the same way as the sequence (12) by exploring
the fact that |V(i)| < mr + h0 r for all i ∈ [q]. A W-alias introduced in this case may contain V as the last symbol in
pi W, where i ∈ [q]. Since the number of recursive constants is finite, the number of W-aliases must remain finite.
From now on we assume that an extended PDA admits normed, recursive, and unnormed constants.
4.4. Termination Condition for Duplication Strategy
Let’s take another look at the semi-decidable procedure BT defined in Fig. 1 and Fig. 2. Section 4.2 provides
a method to grow a nonsink node. Section 4.3 introduces a technique to terminate a long decreasing sequence.
Nontermination is however not completely eliminated. Suppose (L0 U0 σ0 , M0 σ0 ) is a u-alias. After growing thecharacteristic tree for the u-alias over σ0 , we get a recursive node of the form (p0 σ0 , G0 σ0 ) say. We apply the leftbalance strategy to grow (p0 σ0 , G0 σ0 ), assuming that |G0 σ0 | > m + 1. Some new u-alias (L1 U1 σ1 , M1 σ1 ) is then9generated. According to the construction either σ0 is a suffix of σ1 or σ1 is a suffix of σ0 , depending on whether|G0 | ≥ m or not. In this fashion a sequence of u-aliases(L0 U0 σ0 , M0 σ0 ), (L1 U1 σ1 , M1 σ1 ), . . . , (Li Ui σi , Mi σi ), . . . .

(23)might be produced. Generally we need to consider the situations where the i-th pair in (23) could be (Mi σi , Li Ui σi ).
The following argument however would be the same in the general case. So we shall only consider the sequence (23).
Two exclusive situations may arise. One is that for every i ≥ 0 there is some j > i such that |σ j | ≤ |σi |. In this case arepetition must occur. The other is that there is some i0 such that |σi0 | < |σ j | for all j > i0 . In the latter case we musthave a consecutive sequence of u-aliases that looks like the following.
(Li0 Ui0 σi0 , Mi0 σi0 ), (Li0 +1 Ui0 +1 δi0 +1 σi0 , Mi0 +1 δi0 +1 σi0 ), . . . , (Li0 + j Ui0 + j δi0 + j σi0 , Mi0 + j δi0 + j σi0 ), . . . ,(24)

where |δi0 + j | > 0 for all j > 0. We will call (24) a positive u-alias sequence. An alternative way to see the sequence isthat the suffix σi0 is fixed whereas the prefixes are increasing in size. If we grow the characteristic tree for every pairin (24) over σi0 , we get different recursive constants. Let Vi0 be the recursive constant defined by the h0 -characteristic
tree for (Li0 Ui0 σi0 , Mi0 σi0 ) over σi0 . We now explain the second termination condition. There are two cases.
1. Li0 +h0 Ui0 +h0 δi0 +h0 Vi0 ∼ Mi0 +h0 δi0 +h0 Vi0 . In this case (Li0 +h0 Ui0 +h0 δi0 +h0 σi0 , Mi0 +h0 δi0 +h0 σi0 ) is a deep balance node.
We can rename the node to (Li0 +h0 Ui0 +h0 δi0 +h0 Vi0 , Mi0 +h0 δi0 +h0 Vi0 ), called the d-alias of the deep balance node.
2. Li0 +h0 Ui0 +h0 δi0 +h0 Vi0 / Mi0 +h0 δi0 +h0 Vi0 . Construct the characteristic tree for (Li0 +h0 Ui0 +h0 δi0 +h0 σi0 , Mi0 +h0 δi0 +h0 σi0 )over σi0 extending Vi0 , generating a recursive constant V0 . Now |V0 (i0 )| > 0 but |Vi0 (i0 )| = 0 for some i0 ∈ [q].
Recall that |Vi0 (i0 )| < mr + h0 r for all i0 ∈ [q], hence |δi0 +1 | < mr + h0 r. It follows that |δi0 +h0 | < h0 (mr + h0 r).
In fact |Li0 +h0 Ui0 +h0 δi0 +h0 | ≤ h0 (mr + h0 r) and |Mi0 +h0 δi0 +h0 | ≤ h0 (mr + h0 r). Let h1 be a constant such that thecharacteristic trees for (P0 σ0 , Q0 σ0 ) over σ0 satisfying |P0 | ≤ h0 (mr + h0 r) and |Q0 | ≤ h0 (mr + h0 r) are essentially bounded by h1 . If Li0 +h0 +h1 Ui0 +h0 +h1 δi0 +h0 +h1 V0 ∼ Mi0 +h0 +h1 δi0 +h0 +h1 V0 , then the deep balance node is(Li0 +h0 +h1 Ui0 +h0 +h1 δi0 +h0 +h1 σi0 , Mi0 +h0 +h1 δi0 +h0 +h1 σi0 ) and (Li0 +h0 +h1 Ui0 +h0 +h1 δi0 +h0 +h1 V0 , Mi0 +h0 +h1 δi0 +h0 +h1 V0 ) is thed-alias of the deep balance node. If Li0 +h0 +h1 Ui0 +h0 +h1 δi0 +h0 +h1 V0 / Mi0 +h0 +h1 δi0 +h0 +h1 V0 , then construct the characteristic tree for (Li0 +h0 +h1 Ui0 +h0 +h1 δi0 +h0 +h1 σi0 , Mi0 +h0 +h1 δi0 +h0 +h1 σi0 ) over σi0 extending V0 , generating a recursive constant V1 . We then continue inductively. The construction must end since there are only q entries to arecursive constant.
We conclude that there are constants h0 < . . . < hq , depending only on the definition of the PDA, such that for eachpositive u-alias sequence of the form (24) there is some h < q that renders valid the following statement: There arerecursive constants V0 , V1 , . . . , Vh satisfying Vi0  V0  V1  . . .  Vh such that for each j ≤ h the recursive constantV j is defined by the h j -characteristic tree over σi0 for(Li0 +h0 +h1 +...+h j Ui0 +h0 +h1 +...+h j δi0 +h0 +h1 +...+h j σi0 , Mi0 +h0 +h1 +...+h j δi0 +h0 +h1 +...+h j σi0 );moreover Li0 +h0 +h1 +...+hh+1 Ui0 +h0 +h1 +...+hh+1 δi0 +h0 +h1 +...+hh+1 Vh ∼ Mi0 +h0 +h1 +...+hh+1 δi0 +h0 +h1 +...+hh+1 Vh . The node
(Li0 +h0 +h1 +...+hh+1 Ui0 +h0 +h1 +...+hh+1 δi0 +h0 +h1 +...+hh+1 σi0 , Mi0 +h0 +h1 +...+hh+1 δi0 +h0 +h1 +...+hh+1 σi0 )is the deep balance node and its d-alias is the node
(Li0 +h0 +h1 +...+hh+1 Ui0 +h0 +h1 +...+hh+1 δi0 +h0 +h1 +...+hh+1 Vh , Mi0 +h0 +h1 +...+hh+1 δi0 +h0 +h1 +...+hh+1 Vh ).
Without loss of generality we may assume that |Vh (i)| ≤ hh for all i ∈ [q].
5. Generating Tree
We are now in a position to turn the semantic construction BT into a nondeterministic algorithm GT by incorporating all the facts revealed so far in Section 4. We remark that an input to the construction BT is a pair such thatP ∼ Q, whereas an input to the algorithm GT is any pair of extended processes. The nondeterministic algorithm GT
is defined in Fig. 3. Again some remarks are inserted in the algorithm in small font. To check the property stated in
Step 3(b)iiA, the algorithm has to call a subroutine that upon receiving a number h generates an h-characteristic tree
for some node in the output tree of the algorithm. The subroutine will be defined in Section 6. The algorithm GT
makes many guesses. However termination is guaranteed.
10Input: A pair (P, Q) of processes, and numbers h0 , h1 , . . . , hq such that h0 < h1 < . . . < hq .
Algorithm GT :1. If (P, Q) is an i-node or an r-node, stop.
bi
2. If |P| ≤ m + 1 and |Q| ≤ m + 1, guess a finite set of transitions (P, Q) −→ (Pi , Qi ) , and verify that the set of
i∈I
 b

bi
i
edges P −→ Pi , Q −→ Qi
form a 1-bisimulation tree for (P, Q). If it does form a 1-bisimulation tree, applyi∈I

GT to every (Pi , Qi ) that is neither an i-leaf nor an r-leaf; otherwise abort.
In the recursive invocations of GT the parameters h0 , h1 , . . . , hq remain the same.

3. If P = pXα and Q = Mσ such that |M| = m, |Mσ| > m + 1, guess an (m−1)-bisimulation tree for (P, Q) but
suspend the growth of every sink node so that a normed constant U is defined. Verify that the internal nodes of
the guessed tree satisfy the strong bisimulation property. If the verification is unsuccessful, abort; otherwise do
the following.
(a) For every sink node do the following:i. If the sink node is not an expansion node, apply GT to the sink node.
ii. If the sink node is an expansion node (qZ, N), then abort if there is a long left decreasing path fromsome (qZ, N 0 ) to (qZ, N) that is longer than t(qn2q ), otherwise do (3(a)iiA) or (3(a)iiB) nondeterministically.
bi
A. Guess a finite set of transitions (qZ, N) −→ (Pi , Qi ) , and verify that the set of edges
i∈J


bi
bi
qZ −→ Pi , N −→ Qi
form a 1-bisimulation tree for (qZ, N). If it does form a 1-bisimulationi∈Jtree, apply GT to every (Pi , Qi ) that is neither an i-leaf nor an r-leaf; otherwise aborts.
B. Choose a long left decreasing path from some (qZ, N 0 ) to (qZ, N), abort if such a path does notexist or if the statement (†) cannot be validated:(†) N 0 = Ga σ0 and N = Gb σ0 for some Ga , Gb satisfying ∂Ga = ∂Gb .
For each h ∈ ∂Ga choose a long right decreasing path from (qZ, Ga σ0 ) to some (Ch , ph σ0 ). Define
an unnormed constant W as in (21); introduce the W-alias (Ga W, Gb W) of (qZ, Wb σ0 ); and apply
GT to the W-alias.
(b) For the u-alias (LUσ, Nσ) of every nonsink node, abort if there is a positive u-alias sequence that ends in(LUσ, Nσ) and is longer than h0 + h1 + . . . + hq , otherwise nondeterministically do (3(b)i) or (3(b)ii).
i. Guess a characteristic tree of height h0 for (LUσ, Nσ). If any of the internal nodes of the guessed tree
fails the strong bisimulation property, abort; otherwise do the following.
A. Apply GT to every recursive node.
B. Apply GT to the v-alias of every balance node.
ii. If (LUσ, Nσ) is (Li0 +h0 +h1 +...+hh Ui0 +h0 +h1 +...+hh δi0 +h0 +h1 +...+hh σi0 , Mi0 +h0 +h1 +...+hh δi0 +h0 +h1 +...+hh σi0 ) forsome h ∈ [q], guess a recursive constant Vh such that |Vh (i)| < hh for all i ∈ [q], and then apply GT tothe deep balance node (Li0 +h0 +h1 +...+hh Ui0 +h0 +h1 +...+hh δi0 +h0 +h1 +...+hh Vh , Mi0 +h0 +h1 +...+hh δi0 +h0 +h1 +...+hh Vh ).
In the decidability proof the guessed recursive constant Vh must be validated. Specifically it must be shown that
A. for each i satisfying |Vh (i)| > 0 there is some j < h such that (pi σi0 , Vh (i)σi0 ) or (Vh (i)σi0 , pi σi0 ) is admitted
in the h j -characteristic tree constructed from the output of GT .
We will explain how the h j -characteristic tree is constructed in the proof of Theorem 9.

4. If Q = pXα, |Q| ≤ m + 1 and P = Mσ such that |M| = m, |Mσ| > m + 1 and that M does not contain any
constant, carry out the construction symmetric to the one in Case 3.
For simplicity we have ignored the nontermination caused by sequences like (22) since it introduces no new difficulty.
Figure 3: Nondeterministic Algorithm GT .

11

Lemma 8. The algorithm GT always terminates.
Proof. Suppose an execution of GT on an input pair (P, Q) does not abort. A path cannot contain an infinite numberof small nodes, bearing in mind that there are only a finite number of constants. A long decreasing path may switch
to a long right decreasing path, but not vice versa. By definition the execution path cannot contain, starting from an
expansion node, a long left/right decreasing path longer than t(qn2q ), nor can it contain any positive u-alias sequence
longer than h0 + h1 + . . . + hq . Between any two such long decreasing paths/positive u-alias sequences there must
be other kind of nodes. If a path contains a nonsink (balance) node, it contains its u-alias (v-alias). There cannot be
any path that contains infinitely many u-aliases/v-aliases/d-aliases/w-aliases since they are all bounded in size. We
conclude by König lemma that the output tree must be finite.
We call the output of a successful execution of GT a potentially generating tree for the input pair (P, Q). It is a
generating tree for (P, Q) if statement 3(b)iiA of Fig. 3 is valid throughout the execution of the algorithm. A graphicaloutline of a generating tree is given in Fig. 4, where j0 = h0 + h1 + . . . + hh , and the nodes in boldface are leaves, anda node is separated from its alias by a horizontal line.
(pXα, M σ)(pi α, Mi σ)(Lα, N σ)(LU σ, N σ)
(Gj 0 σ, pj 0 σ)(qZ, Ga σ0 )(ph σ, pk σ)(pj σ, Gj σ)(Aσ, Bσ)(AV, BV )(qZ, Gb σ0 )(Ga W, Gb W )(rZ, rZ)(Li0 Ui0 σi0 , Mi0 σi0 )(O, O0 )(rσi0 , Mi00 σi0 )(qZ, Ga σ00 )(Li0 +1 Ui0 +1 δi0 +1 σi0 , Mi0 +1 δi0 +1 σi0 )(Aσ 0 , Bσ 0 )(AV, BV)(qZ, Gb σ00 )(Ga W, Gb W)(Li0 +j Ui0 +j δi0 +j σi0 , Mi0 +j δi0 +j σi0 )(Li0 +j 0 Ui0 +j 0 δi0 +j 0 σi0 , Mi0 +j 0 δi0 +j 0 σi0 )(Li0 +j 0 Ui0 +j 0 δi0 +j 0 Vh , Mi0 +j 0 δi0 +j 0 Vh )Figure 4: A Generating Tree.

12(O, O0 )6. Decidability
Suppose that some execution of GT on input process pair (P, Q) and input constants h0 , . . . , hh returns a generating
tree for (P, Q). Let’s explain how to grow the generating tree into a bisimulation tree for (P, Q) level by level. Equivalently we define a procedure that upon receiving a node in the generating tree construct a bisimulation tree for thenode in a coinductive manner. This is done inductively as follows.
1. Suppose (Aσ, Bσ) is a balance node and (AV, BV) is its v-alias. The growth of (Aσ, Bσ) simply duplicates thegrowth of (AV, BV).
2. Suppose (pXUσ, Mσ) is the u-alias of a nonsink node. Firstly notice that we can grow every balance node of
the characteristic tree for (pXUσ, Mσ) as described in the previous case. We then simply compose the resulting
tree level by level with the bisimulation trees for the recursive nodes (pi σ, Li σ) or (Li σ, pi σ) such that |Li | > 0.
3. If U is defined as in (6), we can grow a bisimulation tree for (pXα, pXUσ) by appending the bisimulation
tree for (pi α, Mi σ). We can then grow a bisimulation tree for (pXα, Mσ) by composing the bisimulation treefor (pXα, pXUσ) with the bisimulation tree for (pXUσ, Mσ), the construction of the latter is described in theprevious case.
4. Let’s now take a look at the expansion node (qZ, Gb σ0 ) as discussed before and after (16). We can grow abisimulation tree for the alias (Ga σ0 , Gb σ0 ) by copying the growth of (Ga W, Gb W), and whenever the suffix σ0
is exposed continuing the imitation by composing with the bisimulation trees for (Ch , ph σ0 ) or (ph σ0 , Ch ) forh ∈ [q], confer (19) and (21). We then grow a bisimulation tree for (qZ, Gb σ0 ) by composing the bisimulation
tree for (qZ, Ga σ0 ) with the bisimulation tree for (Ga σ0 , Gb σ0 ). See the left and middle diagrams in Fig. 5.
5. Let (Li0 +h0 +...+hh Ui0 +h0 +...+hh δi0 +h0 +...+hh σi0 , Mi0 +h0 +...+hh δi0 +h0 +...+hh σi0 ) be a deep balance node as in (24). A bisimulation tree for the deep balance node is obtained by duplicating the bisimulation tree for the alias(Li0 +h0 +...+hh Ui0 +h0 +...+hh δi0 +h0 +...+hh Vh , Mi0 +h0 +...+hh δi0 +h0 +...+hh Vh ),(25)

where Vh is the recursive constant guessed in Step 3(b)ii of GT and checked in Step 3(b)iiA. By definition thebisimulation tree for (25) is grown after the h j -characteristic tree for(Li0 +h0 +...+h j Ui0 +h0 +...+h j δi0 +h0 +...+h j σi0 , Mi0 +h0 +...+h j δi0 +h0 +...+h j σi0 )(26)

has been produced by GT for all j < h. So there is no circularity. See the right diagram in Fig. 5, where the small
triangles are (m−1)-bisimulation trees that define normed constants. The point is that when the characteristic
tree generating Vi0 +h0 starts to grow, the growth of the h0 -characteristic tree generating Vi0 is already completed.
We conclude that if GT (P, Q, h0 , . . . , hh ) returns a generating tree then P ∼ Q. Decidability proof is now a formality.
Theorem 9. The strong bisimilarity for PDA is decidable.
Proof. We only have to give a semidecidable procedure for ∼. Given a pair (P, Q), guess numbers h0 , . . . , hq suchthat 0 < h0 < . . . < hq . Apply GT to construct a generating tree for (P, Q) nondeterministically. If the construction
successfully outputs a potential generating tree and the output is in fact a generating tree, return ‘yes’.
Checking if a successful output is a generating tree is equivalent to checking if statement 3(b)iiA can be validated.
Referring to (24) we can firstly construct for each j ≤ h an h j+1 -bisimulation tree B j for (26) as described in the
beginning of the section, and this can be done before GT processes the deep balance node. Secondly we can constructfrom B0 and Vi0 an h1 -characteristic tree C0 for (Li0 +1 Ui0 +1 δi0 +1 σi0 , Mi0 +1 δi0 +1 σi0 ) over σi0 extending Vi0 . This canbe done by the construction defined on page 6. The difference between the construction on page 6 and the present
construction is that the former is semantic whereas the latter is algorithmic. Imagine we are growing B0 level by level,
and at the same time we define a recursive constant V 0 . Initially V 0 is Vi0 . Whenever we come across a node of the form(pk σi0 , Mk0 σi0 ), we check if V 0 is defined at k. If it is not defined at k we extend the definition of V 0 by V 0 (k) = Mk0 .
Otherwise we compose the bisimulation tree for (V 0 (k)σi0 , pk σi0 ) with the subtree of B0 rooted at (pk σi0 , Mk0 σi0 ). Now
either (V 0 (k)σi0 , pk σi0 ) and/or (pk σi0 , V 0 (k)σi0 ) is a node of Bi0 or B0 . So the bisimulation tree for (V 0 (k)σi0 , pk σi0 )is essentially a subtree of Bi0 or B0 . In this way we get the h0 -characteristic tree C0 by composition. Let V 0 be therecursive constant induced by C0 . Thirdly we can construct from Bh and V h−1 an hh+1 -characteristic tree Ch for the
deep balance node over σi0 extending V h−1 , inducing a recursive constant V h . The validation of statement 3(b)iiA isdone by comparing V h against Vh gussed by the algorithm.

13

(pZ, Gb σ0 )(pZ, Ga σ0 ) (Ga σ0 , Gb σ0 )(Ga W, Gb W )Vi0(ph σ0 , Oσ0 )(Ch , OW )(ph σ0 , Ch )(Ch , Oσ0 )Vi0 +0Vi0 +h0

Figure 5: Bisimulation Trees from Generating Trees.

7. Conclusion
All proofs of the decidability of equivalence checking problem for (D)PDA are based on Senizergues’ fundamental
observation on the recurrent behaviours of processes [22, 23, 24, 26, 27]. A pair of equivalent processes can be turned
into an equivalent pair of prefix bounded processes using the balance strategy. The latter pair has finite behaviours
by the duplication technique. By applying the two strategies in an orderly manner, using weights, conditional rules,
etc., one hopes to construct a finite tree-like structure that witnesses the equivalence of two (D)PDA processes. The
finite structure can be a proof system, a tableau, or a game. There are two difficulties when reasoning about thefinite structures. One is to show the compositionality of them. For DPDA equivalence and strong bisimilarity of
PDA compositionality is relative easy to establish. For branching bisimilarity compositionality depends crucially ona correct definition of finite structure. The main difficulty in decidability proof is to do with termination. In the lightof König lemma termination is equivalent to the finiteness of tree-like structures. In Stirling’s approach [29, 30, 32]
the key is to argue that all tableaux are finite. In Jančar’s proof [16, 17] the main step is to demonstrate the existenceof an (n, g)-sequence convincing Refuter of the fact that he will never have any chance of winning.
Our motivation for this work is to give a simpler and more intuitive proof of the decidability of the strong bisimilarity of PDA. The endeavor is worthwhile for at least two reasons. Theoretically the strong bisimilarity of PDA poses
one of the most challenging problems in the field of equivalence checking. Decidability proofs of simpler models
and their variants in the general framework of process rewriting system [19] are a lot easier [5, 6, 7, 8, 38]. Any
improvement of a decidability proof about PDA may have implications to the decidability proofs of related problems.
For instance a more streamlined proof may help generalize the current results to models that admit far more liberalsilent transitions than DPDA. At pragmatic level algorithms about PDA are important in programme analysis. A simpler and more intuitive proof may suggest how to constrain the PDA model to obtain efficient equivalence checking
algorithms. This would be welcome in view of the fact that the general problem is highly complex [3]. It turns out
for us that the idea of the proof is most easily explained directly in terms of strong bisimulations. It is well-known
that bisimulations are closed under set union and composition. So the compositionality would not be an issue. Our
termination conditions draw inspiration from Jančar’s treatment to long prefix increasing sequence in the setting of
Defender-Refuter game. The introduction of the unnormed constants follows the commmon practice in the study of
PDA, that is to extend the basic PDA model so that the extended model enjoys better algebraic property. The structureof our decidability proof is basically Stirling’s proof using tableau system plus our termination conditions. When one
works with tableau systems one actually has in mind the bisimulation trees. Simplification is achieved by working
directly with the latter objects.
The termination conditions of this paper can be applied to richer models. They are applied in the proof that thebranching bisimilarity [36, 37, 2] is decidable for -pushing normed PDA [9] and for -popping PDA [10]. It remains
to see if the proof methodology is useful in saying anything about the branching bisimilarity of finite turn PDA [25].
Acknowledgment
We thank BASICS members for frequent discussions on issues related to PDA. We thank particularly Qiang Yin
for collaboration on the decidability of branching bisimilarity of PDA variants [9, 10], which has greatly enhanced
our understanding of the subject. We also thank Petr Jančar for discussions on related issues. The support from NSFC
(61472239, 61772336) is gratefully acknowledged.
14

References[1] J. Baeten, J. Bergstra, and J. Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-free Languages. PARLE
1987, Lecture Notes in Computer Science 259, 94-111, 1987.
[2] J. Baeten. Branching bisimilarity is an equivalence indeed. Information Processing Letters 58:141-147, 1996.
[3] M. Benedikt, S. Göller, S. Kiefer, and A. Murawski. Bisimilarity of Pushdown Automata is Nonelementary. In LICS’13, 488-498,
2013.
[4] O. Burkart, D. Caucal, F. Göller, and B. Steffen. Verification on Infinite Structures. In J. Bergstra, A. Ponse, and S. Smolka, editors,
Handbook of Process Algebra, 545-623. North-Holland, 2001.
[5] W. Czerwiński, P. Hofman, and S. Lasota. Decidability of branching bisimulation on normed commutative context-free processes. In
CONCUR’11, pages 528-542. Lecture Notes in Computer Science 6901, Springer, 2011.
[6] S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. In CONCUR’92, pages
138-147. Lecture Notes in Computer Science 630, Springer, 1992.
[7] S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation equivalence is decidable for basic parallel processes. In Prodeedings of the
4th International Conference on Concurrency Theory (CONCUR’93), pages 143-157. Springer, 1993.
[8] Y. Fu. Checking Equality and Regularity for Normed BPA with Silent Moves. ICALP’13, Lecture Notes in Computer Science 7966,
238-249, 2013.
[9] Y. Fu and Q. Yin. Decidability of Epsilon Pushing PDA, 2018.
[10] Y. Fu and Q. Yin. Decidability of Epsilon Popping PDA, 2018.
[11] S. Ginsburg and S. Greibach. Deterministic Context Free Languages. Information and Control, 9:620-648, 1966.
[12] J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley Publishing Company,
1979.
[13] H. Hüttel and C. Stirling. Actions speak louder than words: Proving bisimilarity for context-free processes. In LICS’91, pages 376-386,
1991.
[14] P. Jančar. Decidability of DPDA Language Equivalence via First-Order Grammars. In LICS’12, 415-424. IEEE Computer Society,2012.
[15] P. Jančar. Equivalences of Pushdown Systems are Hard. Foundations of Software Science and Computation, 1-28, 2014.
[16] P. Jančar. Bisimulation Equivalence of First Order Grammars. In J. Esparza, P. Fraigniaud, T. Husfeldt, and E. Koutsoupias, editors,
ICALP’14, Lecture Notes in Computer Science 8573, 232-243, 2014.
[17] P. Jančar. Bisimulation Equivalence of First Order Grammars. arXiv:1405.7923, 2014.
[18] A. Kučera and P. Jančar. Equivalence-Checking on Infinite-State Systems: Techniques and Results. Theory and Practice of Logic
Programming, 6:227-264, 2006.
[19] R. Mayr. Process Rewrite Systems. Information and Computation, 156:264-286, 2000.
[20] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[21] D. Park. Concurrency and Automata on Infinite Sequences. In TCS’81, Lecture Notes in Computer Science 104, 167-183. Springer,
1981.
[22] G. Sénizergues. The Equivalence Problem for Deterministic Pushdown Automata is Decidable. In ICALP’97, Lecture Notes in
Computer Science 1256, 671-681. Springer-Verlag, 1997.
[23] G. Sénizergues. Decidability of Bisimulation Equivalence for Equational Graphs of Finite Out-Degree. In FOCS’98, 120-129. IEEE,
1998.
[24] G. Sénizergues. L(a)=L(b)? Decidability Results from Complete Formal Systems. Theoretical Computer Science, 251(1-2):1-166,
2001.
[25] G. Sénizergues. The Equivalence Problem for t-Turn DPDA is co-NP. ICALP 2003, Lecture Notes in Computer Science 2719, 478-489,
2003.
[26] G. Sénizergues. L(a)=L(b)? A Simplified Decidability Proof. Theoretical Computer Science, 281(1):555-608, 2002.
[27] G. Sénizergues. Decidability of Bisimulation Equivalence for Equational Graphs of Finite Out-Degree. SIAM Journal of Computing,34(5):1025-1106, 2005.
[28] J. Srba. Undecidability of Weak Bisimilarity for Pushdown Processes. In CONCUR’02, Lecture Notes in Computer Science 2421,
579–593. Springer-Verlag, 2002.
[29] C. Stirling. Decidability of Bisimulation Equivalence for Normed Pushdown Processes. In CONCUR’96, Lecture Notes in Computer
Science, 217-232. Springer-Verlag, 1996.
[30] C. Stirling. Decidability of Bisimulation Equivalence for Normed Pushdown Processes. Theoretical Computer Science, 195(2):113131, 1998.
[31] C. Stirling. The Joy of Bisimulation. In MFCS’98, Lecture Notes in Computer Science 1450, 142-151. Springer, 1998.
[32] C. Stirling. Decidability of Bisimulation Equivalence for Pushdown Processes. 2000.
[33] C. Stirling. Decidability of DPDA Equivalence. Theoretical Computer Science, 255(1-2):1-31, 2001.
[34] Stirling. An Introduction to Decidability of DPDA Equivalence. In FSTTCS’01, Lecture Notes in Computer Science 2245, 42-56.
Springer, 2001.
[35] Stirling. Deciding DPDA Equivalence is Primitive Recursive. In ICALP’02, Lecture Notes in Computer Science 2380, 821-832.
Springer, 2002.
[36] R. van Glabbeek and W. Weijland. Branching Time and Abstraction in Bisimulation Semantics. In Information Processing’89, 613-618.
North-Holland, 1989.
[37] R. van Glabbeek and W. Weijland. Branching Time and Abstraction in Bisimulation Semantics. Journal of ACM, 3:555-600, 1996.
[38] Q. Yin, Y. Fu, C. He, M. Huang, and X. Tao. Branching Bisimilarity Checking for PRS. In J. Esparza, P. Fraigniaud, T. Husfeldt, andE. Koutsoupias, editors, ICALP’14, Lecture Notes in Computer Science 8573, 363-374, 2014.

15