Bisimulation Equivalence of First-Order Grammars

A decidability proof for bisimulation equivalence of first-order grammars (finite sets of labelled rules for rewriting roots of first-order terms) is presented. The equivalence generalizes the DPDA (deterministic pushdown automata) equivalence, and the result corresponds to the result achieved by Senizergues (1998, 2005) in the framework of equational graphs, or of PDA with restricted epsilon-steps. The framework of classical first-order terms seems particularly useful for providing a proof that should be understandable for a wider audience. We also discuss an extension to branching bisimilarity, announced by Fu and Yin (2014).


Introduction
Decision problems for semantic equivalences have been a frequent topic in computer science. E.g., for pushdown automata (PDA) language equivalence was quickly shown undecidable, while the decidability in the case of deterministic PDA (DPDA) is a famous result by Sénizergues [15]. A finer equivalence, called bisimulation equivalence or bisimilarity, has emerged as another fundamental behavioural equivalence ; for deterministic systems it essentially coincides with language equivalence. We name [1] to exemplify the first decidability results for infinite-state systems, and refer to [18] for a survey of a specific area.
One of the most involved results in the area [17] shows the decidability of bisimilarity of equational graphs with finite out-degree (or of PDA with deterministic popping ε-steps); this generalizes the result for DPDA. The recent nonelementary lower bound [2] for the problem is, in fact, TOWER-hardness in the terminology of [14], and it holds even for real-time PDA, i.e. PDA with no ε-steps. For the full above mentioned PDA the problem is even not primitive recursive, since it is Ackermann-hard [12]. In the deterministic case, the equivalence problem is known to be PTIME-hard, and has a primitive recursive upper bound shown by Stirling [20]; a finer analysis places the problem in TOWER [12]. This complexity gap is just one indication that the respective fundamental equivalence problems are far from being fully understood. Another such indication might be the length and the technical nature of the so far published proofs (including the unpublished [21]).

Preliminaries and Result
In this section we define the basic notions and state the result. Some standard definitions are restricted when we do not need the full generality.
By N we denote the set {0, 1, 2, . . . } of nonnegative integers; we use [i, j] to denote the set {i, i+1, . . . , j}. For a set A, by A * we denote the set of finite sequences of elements of A, which are also called words (over A). By |w| we denote the length of w ∈ A * . By ε we denote the empty sequence (hence |ε| = 0).

LTSs. A labelled transition system (an LTS) is a tuple
where S is a finite or countable set of states, Σ is a finite set of actions (or letters), and a −→⊆ S × S is a set of a-transitions (for each a ∈ Σ). In fact, we only deal with image-finite LTSs, where L = (S, Σ, ( a −→) a∈Σ ) is image-finite if the set {s ′ | s a −→ s ′ } is finite for each pair s ∈ S, a ∈ Σ. We say that L is a deterministic LTS if for each pair s ∈ S, a ∈ Σ there is at most one s ′ such that s a −→ s ′ .
By s w −→ s ′ , where w = a 1 a 2 . . . a n ∈ Σ * , we denote that there is a path s = s 0 a1 −→ s 1 a2 −→ · · · an −→ s n = s ′ ; if s w −→ s ′ , then s ′ is reachable from s, within |w| steps. By s w −→ we denote that w is enabled by s, i.e., s w −→ s ′ for some s ′ . A state s is dead if there is no a ∈ Σ such that s a −→. If L is deterministic, then by s w −→ s ′ or s w −→ we also denote the respective unique path.
(Stratified) bisimilarity. Let L = (S, Σ, ( a −→) a∈Σ ) be a given LTS. We say that a set B ⊆ S × S covers (s, t) ∈ S × S if -for any a ∈ Σ and s ′ ∈ S such that s a −→ s ′ there is t ′ ∈ S such that t a −→ t ′ and (s ′ , t ′ ) ∈ B, and for any a ∈ Σ and t ′ ∈ S such that t a −→ t ′ there is s ′ ∈ S such that s a −→ s ′ and (s ′ , t ′ ) ∈ B.
We note that if s, t are dead states, then (s, t) is covered by any B ⊆ S × S, in particular by ∅. If there is an action a ∈ Σ that is enabled by precisely one of s, t, then (s, t) is not covered by any B.
For B, B ′ ⊆ S × S we say that B ′ covers B if B ′ covers each (s, t) ∈ B. A set B ⊆ S × S is a bisimulation if B covers B. States s, t ∈ S are bisimilar, written s ∼ t, if there is a bisimulation B containing (s, t). We note the standard fact that ∼ ⊆ S × S is the maximal bisimulation, the union of all bisimulations.
We put ∼ 0 = S × S. For k ∈ N, ∼ k+1 ⊆ S × S is the set of all pairs covered by ∼ k . We easily verify that ∼ and ∼ k are equivalence relations, and that ∼ 0 ⊇ ∼ 1 ⊇ ∼ 2 ⊇ · · · · · · ⊇ ∼. For the (first infinite) ordinal ω we put s ∼ ω t if s ∼ k t for all k ∈ N; hence ∼ ω = ∩ k∈N ∼ k . It is a standard fact that ∩ k∈N ∼ k is a bisimulation in any image-finite LTS, where we thus have ∼ = ∼ ω .
Eq-levels. Given an image-finite LTS, we attach the equivalence level (eqlevel) to each pair of states: First-order-term LTSs informally. We focus on certain (image-finite) LTSs in which states are first-order terms ; we mean standard finite terms primarily but it will turn out convenient to consider also infinite regular terms (i.e. infinite terms with only finitely many pairwise different subterms). The terms are built from variables from a fixed countable set Var = {x 1 , x 2 , x 3 , . . . } and from function symbols, also called (ranked) nonterminals, from some specified finite set N ; each A ∈ N has arity(A) ∈ N. We use A, B, C, D for nonterminals, while E, F, . . . (possibly with subscripts etc.) are reserved for terms. An example of a (standard finite) term is E 1 = A(D(x 5 , C(x 2 , B)), x 5 , B) where the arities of A, B, C, D are 3, 0, 2, 2, respectively. The left-hand side of Fig. 1 depicts the syntactic tree of E 1 . (The right-hand side E 2 will be referred to later.) Transitions are determined by a finite set of root-rewriting rules. An example of a "non-popping" rule is A(x 1 , x 2 , x 3 ) a −→ C(D(x 3 , B), x 2 ), an example of a "popping" rule is A(x 1 , x 2 , x 3 ) b −→ x 1 . Each rule induces the transitions arising by applying the same substitution σ to both the left-hand side (lhs) and the right-hand side (rhs) of the rule. E.g., the rule   are terms. The small symbols x 1 , x 2 , x 3 are superfluous here, they just depict the original variables in the lhs and in the rhs of the respective rule; these variables have been replaced by applying the substitution σ. Hence x 3 and x 2 in the target-term have been replaced by the third root-successor and by the second root-successor of the source-term, respectively. In this concrete case the first root-successor of the source-term "disappears" since x 1 does not occur in the rhs of the rule.
Another example can be given by the rule −→ x 1 and the above σ, which induces the transition, or the one-step path, B)), x 5 , B) and H = D(x 5 , C(x 2 , B)). In this case our one-step path exposes a root-successor H in the source term F (the first root-successor in our case); the path has thus "sinked" to a subterm in depth 1.
The result informally. We will show that there is an algorithm that computes EqLv(T 0 , U 0 ) when given a finite set of root-rewriting rules and two terms T 0 , U 0 . In the rest of this section we formalize this statement, making also some conventions about our use of (finite and infinite) terms and substitutions.
Regular terms, presentation size. We identify terms with their syntactic trees, and denote them by E, F, . . . . Thus a term E over N (where N is a set of ranked nonterminals) is a rooted, ordered, finite or infinite tree where each node has a label from N ∪Var; if the label of a node is x i ∈ Var, then the node has no successors, and if the label is A ∈ N , then it has m (immediate) successor-nodes where m = arity(A). More precisely, a term corresponds to a set of isomorphic trees, since two isomorphic trees represent the same term. Each node is also the root of a subterm of E, i.e., of the subtree rooted in this node; more precisely, each concrete node is the root of a subterm-occurrence, since a subterm corresponds to a set of isomorphic subtrees. A subterm can thus have more (maybe infinitely many) occurrences in E. Each subterm-occurrence has its (nesting) depth in E, which is its (naturally defined) distance from the root of E; the term E itself is a subterm-occurrence with depth 0. E.g., in E 1 = A(D(x 5 , C(x 2 , B)), x 5 , B) (in Fig. 1) there is one occurrence of the term C(x 2 , B), with depth 2, and two occurrences of x 5 , with depths 1 and 2.
We also use the standard notation: a term is either , and G 1 , . . . , G m are the root-successors, i.e., the ordered subterm-occurrences with depth 1.
A term E is finite if the respective tree is finite; by Height(E) we then mean the largest depth of a subterm-occurrence in E. For E 1 = A(D(x 5 , C(x 2 , B)), x 5 , B) in Fig. 1 we thus have Height(E 1 ) = 3.
A (possibly infinite) term is regular if it has only finitely many subterms (though the subterms may be infinite and can have infinitely many occurrences). Any regular term has a natural finite-graph presentation (with possible cycles). E.g., the right-hand side of Fig. 1 presents a regular term E 2 ; here the term E 2 itself is a subterm with infinitely many occurrences (with depths 0, 3, 6, . . . ). By PrSize(E) (the presentation size of E) we mean the size of the smallest graph presentation of E.
We can be more precise, though the respective notions are standard. A finitegraph presentation of a (regular) term over N is a finite directed (multi)graph, with a designated root, where each node has a label from N ∪ Var; if the label of a node is xi ∈ Var, then the node has no outgoing arcs, and if the label is A ∈ N , then the node has arity(A) ordered outgoing arcs. The standard "tree-unfolding" of the graph is the respective term, which is infinite if there are cycles in the graph. We can obviously effectively compare if two graph presentations represent the same term. Given a presentation of a regular term E, we can thus compute the syntactic graph of E, i.e., the graph whose nodes (one-to-one) correspond to the (roots of) subterms occurring in E. (E.g., the syntactic graph of E2 in Fig. 1 arises from the given graph presentation by merging the nodes with label x5 and merging those with label B; but we note that if we replaced D with C, we could not merge the nodes with label C.) We can take the number of nodes of the syntactic graph of E as PrSize (E).
In what follows, by a "term" we mean a "regular term" if we do not say explicitly that the term is finite. (We do not consider non-regular terms.) We reserve symbols E, F, G, H, and also T, U, V, W , for denoting (regular) terms.
Substitutions, associative composition. By Terms N we denote the set of all (regular) terms over a set N of (ranked) nonterminals. A substitution σ is a mapping is finite; we reserve the symbol σ for substitutions. By range(σ) we mean the set {σ(x i ) | x i ∈ supp(σ)}. By applying a substitution σ to a term E we get the term Eσ that arises from E by replacing each occurrence of x i with σ(x i ).
First-order grammars. A first-order grammar, an FO-grammar or just a grammar for short, is a tuple G = (N , Σ, R) where N is a finite set of ranked nonterminals, viewed as function symbols with arities, Σ is a finite set of actions (or letters), and R is a finite set of rules of the form where A ∈ N , arity(A) = m, a ∈ Σ, and E is a finite term over N in which each occurring variable is from the set {x 1 , x 2 , . . . , x m }.
Rule-based and action-based LTSs generated by grammars. Given Speaking in an informal "operational" manner, we can apply a rule r of the form A(x1, . . . , xm) r −→ E to (a graph-presentation of) F iff root(F ) = A. If so, and E = xj, then the target of the j-th outgoing arc of the root of F (which might be the root itself in the case of a loop) is the root of H where F r −→ H. If E ∈ Var, we get H (for which F r −→ H) by adding (a fresh copy of) E to F where the root of E becomes the root of the arising H; to finish the construction of H, each arc in E leading to a node labelled with xj is redirected to the j-th root-successor in F . Hence the variables x1, . . . , xm in the rules serve just as "place-holders" for root-successors (in the source term of a transition); recall again Fig. 2. The LTS L r G is deterministic, since for each F and r there is at most one H such that F r −→ H. Hence F w −→, for w ∈ R * , refers to a unique path in L r G (which is later technically convenient).
We stress explicitly that transitions cannot add variables, i.e., F w −→ H implies that each variable occurring in H also occurs in F (though not vice versa in general; recall that the first root-successor "disappeared" by the transition in Fig. 2, which also caused that the subterm x2 "disappeared"). We also note that F w −→ H implies F σ w −→ Hσ for any substitution σ; this follows from the fact that xi are dead, not enabling any action. Finally we observe that our stipulation that the right-hand sides (rhs) E in the grammar-rules A(x1, . . . , xm) a −→ E are finite implies that all terms reachable from a finite term are finite. (It turns out technically convenient to have the rhs finite while including regular terms into our LTSs.) By the action-based LTS, related to a grammar G = (N , Σ, R), we mean the LTS for any substitution σ.
where act(w) is the naturally defined action-image of w: the homomorphism act : R * → Σ * is defined by putting act(r) = a for any rule r of the form A(x 1 , . . . , x m ) a −→ E. We note that L a G is image-finite, and nondeterministic in general. In fact, we still complete the definition of L a G by stipulating that We thus have that In particular we have x i ∼ 1 x j for i = j. Technically we think of each used variable x ∈ Var as being equipped with its unique action a x and with the transition x ax −→ x in L a G ; this entails that x i ∼ 1 H for H = x i without any special stipulation.
Convention. Whenever we consider F w −→ H in L a G , we tacitly assume that no special transitions x ax −→ x are involved. Hence F w −→ H implies F σ w −→ Hσ for any substitution σ. We also stipulate that ∅ covers (x i , x i ), thus avoiding superfluous technicalities. In what follows we refer to the action-based LTSs L a G , if we do not say explicitly that we have L r G in mind.

Proof of Theorem 1
We note that deciding ∼ 0 is trivial, since T ∼ 0 U holds for all T, U . When having a procedure deciding ∼ k , we can easily construct a procedure deciding ∼ k+1 ; this follows from the facts that T ∼ k+1 U iff (T, U ) is covered by ∼ k , and that for any V we can construct all (finitely many) pairs (a, V ′ ) such that V a −→ V ′ . We thus get a part of Theorem 1: There is an algorithm that, given G and T 0 , U 0 , outputs We need to modify the algorithm so that it recognizes the case T 0 ∼ U 0 in finite time. As a convenient tool we introduce a round-based game between Prover(she) and Refuter(he); the game is more involved than the standard bisimulation game. We start with a simple first version of the game, and then we enhance it stepwise. Refuter will be always able to force his win in finite time if the terms in the initial pair (T 0 , U 0 ) are non-equivalent. Prover will be always able to avoid losing if T 0 ∼ U 0 , but only in the last game-version she will be able to force her win in finite time. Since Prover's winning strategy for T 0 ∼ U 0 in the last game-version will be finitely presentable and effectively verifiable, a proof of Theorem 1 will be finished. Before the first game-version we observe some simple standard facts related to (stratified) bisimulation equivalence.

Expansions. Assume an LTS
we denote that B ′ is a minimal expansion for B, i.e., B ′ covers B and no proper subset of B ′ covers B; this also implies that for each (s ′ , t ′ ) ∈ B ′ there is (s, t) ∈ B such that s a −→ s ′ and t a −→ t ′ for some a ∈ Σ. We note that ∅ ⊳ ∅, and if s, t are dead (not enabling any action), then {(s, t)} ⊳ ∅.
Prover-Refuter game (first version). A play starts with a grammar G = (N , Σ, R) and an initial pair (T 0 , U 0 ) of terms. For i = 0, 1, 2 . . . , the (i+1)-th round of the play starts with some specified pair (T i , U i ) and proceeds as follows: 1. Prover chooses k > 0 and some B j ⊆ Terms N × Terms N for j = 1, 2 . . . , k and shows that , then Refuter wins.

Refuter chooses a pair (T
is taken for starting the (i+2)-th round.
The reversals of u1, u2 can be found by the "bottom-up approach", starting from (T ′ i , U ′ i ) and going up to (Ti, Ui). This follows from recalling that B ⊳ B ′ implies that for each ( We also note that, e.g., for each V such that This is also depicted in Fig. 3

. When looking for Ui
We say that Refuter uses the least-eqlevel strategy, if he always chooses We easily observe the following facts.
1. If e < ω, then Refuter wins within e+1 rounds by the least-eqlevel strategy. 2. Prover can guarantee that she will not lose within e rounds.
Prover's additional tool. A challenge is to add sound possibilities for Prover to enable her to force her win in finite time if T 0 ∼ U 0 . We allow Prover to claim a win when she can (soundly) demonstrate, in some (i+1)-th round, that either Refuter has not used the least-eqlevel strategy or T 0 ∼ U 0 . This new abstract rule does not change Prop. 4 We thus further assume that Prover wins when a repeat appears, and we look at more involved options enabling her to "balance", i.e., to replace when Refuter uses the least eq-level strategy. Before formulating the second version of the game, we clarify the crucial underlying facts. First a trivial one: Congruence, the crux of balancing. We assume a given grammar G = (N , Σ, R). For substitutions σ, σ ′ and k ∈ N ∪ {ω} we put We also put EqLv(σ, We now note that ∼ k and ∼=∼ ω are congruences: . . , B ′ k with some pairs of identical terms, using the fact that The compositionality induced by the congruence properties leads naturally to considering the following modification of our game, based on decompositions. Prover is always allowed to "decompose" (Ti, Ui), i.e., to present some finite set B of pairs of terms that are in some sense smaller than (Ti, Ui), if it is guaranteed that EqLv(Ti, Ui) ≥ MinEqL(B); Refuter then chooses a pair from B for continuing. If our measure of size satisfies that there are only finitely many pairs with the size that is smaller than or equal to the size of any given (T, U ), then Refuter's least-eqlevel strategy still wins if the initial terms are non-equivalent. On the other hand, if there is a bound such that each pair T ∼ U that is bigger than the bound is decomposable via a set B ⊆∼, then we have a required algorithm: if Prover keeps decomposing large pairs via subsets of ∼, then we get a repeat eventually. This is a basis of decision algorithms for so called BPA processes, which can be viewed as being generated by FO-grammars where all nonterminals have arity 1 (or 0). We can refer, e.g., to the papers [4,3,11] for details. However, in our more general case such a straightforward approach does not seem clear.
We follow a more involved way, based on a balancing strategy that makes the component-terms in (Ti, Ui) "close to each other". We note that balancing strategies, in different frameworks, were used by Sénizergues [15,16,17] and then Stirling [19,20,21]. In fact, we will also discuss a bit of decomposition later, in Section 4.
We now illustrate how Prover can use already the simple fact captured by Prop. 5. Suppose the (i+1)-th round starts with (T i , U i ) and Refuter chooses (T ′ i , U ′ i ) in B k (we refer to the notation in the game definition, and to Fig. 3). We As we already observed, we then must also have U i v2 −→ U ′′ for some U ′′ and some v 2 ∈ R * such that Fig. 3 we would have a respective pair and Refuter uses the least-eqlevel strategy. Therefore Refuter "cannot protest" when Prover puts Refuter uses the least-eqlevel strategy. We note that U ′′ , U ′ i are close to each other in the sense that they are both reachable within k steps from one "pivot term", In the second game-version below we use the congruence properties to enable Prover to replace ( i . Prover-Refuter game (second version). The only change w.r.t. the first game-version is in the point 3: 3. Prover creates (T i+1 , U i+1 ) for the start of the (i+2)-th round: , thus making no change, or she can use one of the following options if available: i/ Left-balancing: Prover presents T ′ i as Gσ for some finite term G and some substitution σ, where for each V ∈ range(σ) she finds Informally speaking, in the second game-version Prover might replace the whole T ′ i with some U ′′ that is "shortly reachable from the pivot" (if possible), but she can also replace just "small-depth" subterms V of T ′ i with (sub)terms V ′ that are "shortly reachable from the pivot"; in the latter case some "special finite head " G of T ′ i remains. (The case of right-balancings is symmetric.) A left-balancing (with the pivot W = U i and the bal-result (Gσ ′ , U ′ i )) is also depicted in the upper part of Fig. 4. (The lower part will be discussed later.) We can easily verify that Prop. 4 holds also for the second game-version. The crucial point is that when Refuter uses the least-eqlevel strategy (this is based on Prop. 6(2) and Prop. 5).
Bal-results are close to pivots. When doing a left-balancing, replacing where we generally extend the notation from (1) as follows: the symbol L signals that we allow a special head in the left -hand component (here with the height at most d). Symmetrically we define W where R refers to the right-hand component.
Two remaining steps in the proof of Theorem 1. We first give an informal sketch, which is then formalized. We recall that a play of the Prover-Refuter game gives rise to a sequence (T 0 , U 0 ), (T 1 , U 1 ), (T 2 , U 2 ), . . . of pairs of terms that are the starting pairs for the rounds 1, 2, 3, . . . , respectively.
In the first of the remaining proof steps (captured by Lemma 7) we show that in the case T 0 ∼ U 0 Prover can force a certain potentially infinite (n, g)subsequence of (T 1 , U 1 ), (T 2 , U 2 ), . . . , by a simple balancing strategy.
In the second step (Lemma 10) we bound the lengths of eqlevel-decreasing (n, g)-sequences. It turns out that Prover can compute a respective bound ℓ n,g ∈ N on condition that she guesses correctly the pairs of equivalent terms up to a certain (large) presentation size.
In the final game-version Prover wins if the length of a created (n, g)-sequence exceeds ℓ n,g , but Refuter's least-eqlevel strategy will be still winning if Prover does not guess correctly when computing ℓ n,g .
Eqlevel-decreasing sequences, and (n, g)-sequences. A sequence In this case the sequence must be finite, and our requirement V 1 ∼ V ′ 1 implies that its length is bounded by 1+EqLv(V 1 , V ′ 1 ). Given a pair (n, g) where n ∈ N and g : N + → N + is a nondecreasing function (where N + = {1, 2, . . . }), a (finite or infinite) sequence of pairs of terms is an (n, g)-sequence if it can be presented as ) Thus the growth of the (regular) "head-terms" E j , F j is bounded by the function g, while at most n fixed "tail-subterms" (of unrestricted size) suffice for this presentation.
Prover can force an (n, g)-subsequence by a balancing strategy. We aim to prove Lemma 7; the proof is the most technical part of the paper, and we thus first explain the idea informally. Prover will use a simple balancing strategy, when starting with T 0 ∼ U 0 : -In each round Prover chooses k = M 1 (in the point 1 of the game), where M 1 is a sufficiently large constant computed from the grammar G; she also uses only B j ⊆∼, thus keeping T i ∼ U i for all i. -Prover balances (in the point 3 of the second game-version), e.g. by repla- in the case of leftbalancing, only when the respective special head G has a bounded height, bounded by some sufficiently large M ′ 0 ; the above M 1 was chosen sufficiently larger than M ′ 0 . -Obeying the above "bounded-head" condition, Prover balances in any round in which she has an opportunity, but she has still another constraint: Prover does not "switch" balancing sides in two consecutive rounds, i.e., if she does a left-balancing in the (i+1)-th round, then she cannot do a right-balancing in the (i+2)-th round, and vice versa.
To sketch the idea why this strategy enables to present an infinite subsequence of (T 1 , U 1 ), (T 2 , U 2 ), . . . as an (n, g)-sequence, we first explore the case where Prover does a left-balancing in the (i+1)-th round. Hence we have (using the notation in (2)), where W is the respective pivot and (Gσ ′ , U i+1 ) the respective bal-result; this is also illustrated in Fig. 4. We have two possibilities for the following (i+2)-th round: 1. There is a left-balancing in the (i+2)-th round. The pivot of this balancing is W ′ = U i+1 , and we have W u −→ W ′ where |u| = M 1 ; hence W ′ is "boundedly reachable" from W in this case. 2. Left-balancing (with a bounded head) is not possible in the (i+2)-th round.
Here we have "no change", i.e., (T i+2 , U i+2 ) = (T ′ i+1 , U ′ i+1 ), and we will derive that W 2M1 (T i+2 , U i+2 ) (using the notation in (1)). Now the pivot W ′ of the first next balancing in future will be again reachable from W ; maybe not boundedly reachable from W but boundedly reachable from a subterm of W .
The claims in the case 2 are based on the fact that the impossibility to do a leftbalancing in the (i+2)-th round entails that the respective path T i+1 = Gσ ′ u −→ T ′ i+1 is a shortest path from Gσ ′ to T ′ i+1 and is steadily "sinking" (or "popping"), exposing deeper and deeper subterms of Gσ ′ ; our choice of M ′ 0 and M 1 will , thus "erasing" G and exposing some x ℓ σ ′ that is reachable from W within M 1 steps; this is depicted in Fig. 4, where x ℓ σ ′ = V ′ .
A simple analysis now shows that if there is no repeat in the sequence (T 0 , U 0 ), (T 1 , U 1 ), (T 2 , U 2 ), . . . , then there must be infinitely many balancing rounds, with the respective pivots denoted W 1 , W 2 , W 3 , . . . , while each concrete pivot can repeat only boundedly many times. In the special "pivot path" −→ · · · which we touched on (recall that W j+1 is boundedly reachable from a subterm of W j ) we then must have a deepest subterm V 0 of W 1 , visited in some segment W j0 −→ · · · does not visit any subterm of V 0 . Then the sequence of bal-results related to W j0+1 , W j0+2 , W j0+3 , . . . can be presented as an (n, g)-sequence, where n, g are determined by G.
The proof of the next lemma just makes clear all relevant technical details.
Proof. We first introduce some technical notions related to a given grammar G = (N , Σ, R); in our notation we assume that arity(A) = m for all A ∈ N .
then we call w ∈ R * an (A, i)-sink word. We assume that for each pair A ∈ N , i ∈ [1, m] there is a fixed shortest (A, i)-sink word w [A,i] , and we put The words w [A,i] can be found and M 0 can be computed by a standard dynamic programming approach.
We note that |w , it can be computed in polynomial time. If we find that there are no (A, i)-sink words for some A, i, then the i-th rootsuccessor of any A(G1, . . . , Gm) plays no role (i.e., its replacing does not change the equivalence class); we can then simply omit the i-th root-successors when the root is A. We can thus decrease arity(A), and modify the grammar rules accordingly so that the LTSs L r G and L a G do not change, up to isomorphism. We can thus indeed safely assume that there are w Finally we consider a shortest path T u −→ T ′ from T to T ′ that is not sinking. To verify the claim, we first note that we cannot have T

It can be written
where |u 1 | = |u 2 | = M 1 , act(u 1 ) = act(u 2 ) (recall again Fig. 3). ii/ If T i u1 −→ T ′ i is not a shortest path from T i to T ′ i or contains a non-sink, and Prover did not do a right-balancing in the (previous) i-th round, then she makes a left-balancing, replacing ( , for some head G with the smallest possible height. (We know that Height(G) ≤ M ′ 0 .) iii/ If ii/ did not apply, and U i u2 −→ U ′ i is not shortest or contains a non-sink, and Prover did not do a left-balancing in the i-th round, then she makes a right-balancing, symmetrically to ii/. iv/ If none of ii/, iii/ applied, Prover puts (T i+1 , U i+1 ) = (T ′ i , U ′ i ). Before analysing the outcome of the strategy, we recall that each bal-result (2)), and we explore the case when Prover does a left-balancing in the (i+1)-th round, with the pivot W = U i , but she cannot do a left-balancing (and thus any balancing) in the (i+2)-th round, as depicted in Fig. 4. (We omit the case with a right-balancing, since it is symmetric.) In the mentioned case we have W round) is sinking (and shortest). But then W 2M1 (T i+2 , U i+2 ) as can be easily verified.
−→ x ℓ ); informally, the path sinks along a branch of G until a leaf On the other hand, our definitions yield that W = Ui  We now explore an infinite play from T 0 ∼ U 0 where Prover uses the above strategy. We first note that there are infinitely many balancings; otherwise from some round on we would have constant sinking on both sides, which necessarily leads to a repeat since our terms are regular.

Suppose we have Ti
−→ · · · where all paths Ti+j −→ Ti+2 first sinks along a branch of G until exposing a subterm of Ti; hence Ti+2 is also reachable from a subterm of Ti in less than M0 steps. Inductively we thus derive that each Ti+j is reachable from a subterm of Ti in less than M0 steps, hence all Ti, Ti+1, Ti+2, . . . range over a finite set. (Similarly Ui, Ui+1, Ui+2, . . . would range over a finite set when there were only finitely many balancings.) We denote the pivots of our infinitely many balancings by W 1 , W 2 , W 3 , . . . , and we easily verify that for each j we have a path W j where |v 1 |, |v 3 | are bounded (surely by 2M 1 ) and V ′′ is a subterm of V ′ ; though v 2 can be sometimes long (and sometimes empty), we can assume the path V ′ v2 −→ V ′′ to be sinking.
In the case of balancings in two consecutive rounds (which are then both left-balancings, or both right-balancings), with pivots Wj and Wj+1, we have Wj u −→ Wj+1 where |u| = M1. Suppose now two consecutive balancings, with pivots Wj ∈ {Ti 1 , Ui 1 } and Wj+1 ∈ {Ti 2 , Ui 2 } that did not happen in two consecutive rounds, hence i2 ≥ i1+2. By our above analysis we have Wj 2M 1 (Ti 1 +2, Ui 1 +2), and the strategy implies that we have either has length M1 and is sinking. Similarly as previously, we derive that Wj+1 is reachable in less than M0 steps from a subterm of either Ti 1 +2 or Ui 1 +2.
Suppose now that the "pivot path" visits subterms of W 1 infinitely often. Then the pivots W j are infinitely often boundedly reachable from a subterm of W 1 , as follows from the form (3) of paths W j wj −→ W j+1 . In this case one pivot reappears infinitely often; but there are boundedly many bal-results for one pivot, and we would thus have a repeat.
Recall that the bal-result (T, U ) related to pivot W satisfies W (2)); hence we have boundedly many possible (T, U ) for one W .
By the form of the paths (3), we know that G ℓ+1 is boundedly reachable from a subterm of G ℓ ; to be more precise, G ℓ+1 is reachable within M0 steps from a subterm of a term that is reachable within 2M1 steps from G ℓ . Hence we surely have We are interested in the bal-results related to W j0+1 , W j0+2 , W j0+3 , . . . , i.e., to G 1 σ ′ , G 2 σ ′ , G 3 σ ′ , . . . . Since the bal-result (T, U ) related to G ℓ σ ′ satisfies , it is built from some finite bounded "head-terms", and some "tail-terms" that are subterms of G ℓ σ ′ in depth at most M 1 .
A path W v −→ V obviously cannot "expose", i.e. "sink to", a subterm of W that is deeper than |v|.
It is useful to rather write for a finite term F in which each branch has length M 1 if it is not a complete branch of V 0 , and where range(σ) consists of the subterms of V 0 with depth M 1 .
To get F and σ, for each particular occurrence of a subterm U of V0 that has depth M1 in V0 we do the following: we replace this occurrence of U with a fresh variable xi and we put σ(xi) = U . The resulting term F is a finite term with Height(F ) ≤ M1, and supp(σ) consists of at most m M 1 variables, where m is the maximum arity of noterminals of the grammar G. Putting Recalling (4) and (5), we have for finite terms E ℓ , F ℓ whose height, and thus also size, can only boundedly grow with growing ℓ (since Height(H ℓ ) can only boundedly grow with growing ℓ).
since the subterm-occurrences with depth at least M1 in H ℓ σ need at least M1 steps for being exposed. Moreover, Height(H ′ ) ≤ Height(H ℓ )+M1 ·MaxRH (where MaxRH bounds the height-increase in one step).
⊓ ⊔ The lengths of eqlevel-decreasing (n, g)-sequences are bounded. Before proving Lemma 10 we show some useful facts and convenient notions, assuming a grammar G = (N , Σ, R). We first recall that EqLv(E, F ) ≤ EqLv(Eσ, F σ), and note: ) When trying to mimic this sequence by replacing σ with the empty-support substitution and aiming to create H)}σ is the substitution σ ′ satisfying x i σ ′ = Hσ and x j σ ′ = x j σ for all j = i. We note that the ("limit" regular) term  Fig. 1 we we denote the substitution arising from σ by removing x i from the support (if it is there), i.e., If H = x i , then x i does not occur in H ′ defined by (6); we then have H ′ σ = H ′ σ [−xi] , and this enables an inductive argument in the proof of Lemma 10, based on stepwise decreasing the substitution support (i.e., the number n in eqlevel-decreasing (n, g)-sequences).
Recalling that σ ∼ k σ ′ iff x j σ ∼ k x j σ ′ for all x j ∈ Var, and referring to H ′ in (6), we also note the following fact (which follows from the congruence properties, by a repeated use of Prop. 6(2)): Proof. Assume H = x i ; hence x i does not occur in H ′ , and we also recall that For j = i we obviously have Let EqLv(Hσ, H ′ σ) = e; this can be also written EqLv(Hσ, H{(x i , H ′ )}σ) = e. If e = ω, then (7) is clear. If e < ω, then (where the inequality ">" follows from Prop. 6(2)). Thus EqLv(Hσ, H ′ σ) > EqLv(x i σ, H ′ σ), and (7) follows by Prop. 5. ⊓ ⊔ Remark. We discussed a possible decomposition approach after noting the congruence properties (Prop. 6). Now Propositions 8 and 9 also suggest a certain decomposition approach, as we now sketch. Suppose we have T ∼ U . We can present (T, U ) as (Eσ, F σ) in many ways. 1. either E ∼ F , in which case Eσ ′ ∼ F σ ′ for any σ ′ , 2. or EqLv(E, F ) = k < ω. In the case 2 we must have xi ∈ supp(σ) and Prop. 8 and 9), and thus We can even bound the size of H, and thus of H ′ , as follows: PrSize(H ′ ) ≤ PrSize(E, F ) + k · StepInc, where StepInc is defined in (8). We also note that for any E, F, σ, xi, H where H = xi (and maybe Eσ ∼ F σ), we have which can lead to a decomposition if the pairs (xiσ, we can continue in the same way as above: In the latter case we get some xj ∈ supp(σ [−x i ] ) and some G such that Continuing this reasoning, we must come to the case 1 after at most n iterations where n = |supp(σ)|, maybe with the empty-support substitution in the end. A problem is to define an adequate size of the pairs, to transform the above observations into a sound algorithm based on the respective decompositions. In the algorithm based on our Prover-Refuter game we circumvent this problem; we use the above observations for a (conditional, nondeterministic) computation of a bound on eqlevel-decreasing (n, g)-sequences.
We still add a few technical notions, useful for proving Lemma 10. For our assumed grammar G = (N , Σ, R) we put We note that F w −→ G implies PrSize(G) ≤ PrSize(F ) + |w| · StepInc. For any set B ⊆ Terms N × Terms N we put stipulating max ∅ = 0. (MinEqL(B) has been already defined.) For any b ∈ N, we put We note that MEL b is always a finite number. For any n ∈ N and g : N + → N + we define ℓ n,g ∈ N by the following recursive definition: Lemma 10. Any eqlevel-decreasing (n, g)-sequence has length at most ℓ n,g .
⊓ ⊔ If T 0 ∼ U 0 , then Prover can force a potentially infinite (n 0 , g 0 )-sequence for certain n 0 , g 0 determined by G (by Lemma 7). She could claim a win after creating an (n 0 , g 0 )-sequence longer than ℓ n0,g0 , if she could demonstrate the value ℓ n0,g0 . (By Lemma 10 it would be then clear that Refuter does not use the least-eqlevel strategy or T 0 ∼ U 0 .) Inspecting the above, we can verify that for computing ℓ n,g for concrete n, g it suffices to know SIZE ≤B ∩ ∼ for a sufficiently large B ∈ N, and the values g(j) for j from a sufficiently large initial segment [1, m] of N. We can capture this by the following inductive definition: -We say that B ∈ N is a sufficient size-bound for n ∈ N and g : N + → N + (i.e., for computing ℓ n,g ) if g(1) ≤ B and in the case n > 0 we also have that B is a sufficient size-bound for n−1, g ′ where g ′ is defined by (9). -We say that m ∈ N is a sufficient segment-bound for n ∈ N and g : N + → N + (i.e., for computing ℓ n,g ) if m ≥ 1 and in the case n > 0 we have that m ≥ 1 + MEL g(1) + m ′ where m ′ is a sufficient segment-bound for n−1, g ′ where g ′ is defined by (9).
Finally we note that Prover can, when given a grammar G, present some n 0 ∈ N and g 0 : N + → N + (or just the values g 0 (1), g 0 (2), . . . , g 0 (m) for some m ∈ N) and perform the above recursive computation for ℓ n0,g0 , while guessing a set C ⊆ (SIZE ≤B ∩ ∼) for some B ∈ N that is sufficient for this computation. We note that Prover can demonstrate that C ⊆ ∼, and also compute the eq-level for each pair in C (recall Prop. 2). For Rest = SIZE ≤B C Prover just claims that it is a subset of ∼, in which case her computation of ℓ n0,g0 would be indeed correct; in reality she computes a value ℓ C n0,g0 that is dependent on her choice of C. We let Refuter to challenge the assumption Rest ⊆∼, by choosing a pair from Rest, so that his least-eqlevel strategy will still be winning if Prover does not guess C correctly. This idea will be now formalized and embodied in the final game-version.
For C ⊆ ∼ and b ∈ N we put For triples (C, n, g) where C ⊆ ∼, n ∈ N, g : N + → N + we define ℓ C n,g by the following recursive definition: (1) , and ℓ C n+1,g = 1 + MEL C g(1) + ℓ n,g ′ where -We say that B ∈ N is a sufficient size-bound for a triple (C, n, g) as above if C ⊆ SIZE ≤B , g(1) ≤ B, and in the case n > 0 we also have that B is a sufficient size-bound for (C, n−1, g ′ ) where g ′ is defined by (10). -We say that m ∈ N is a sufficient segment-bound for (C, n, g) if m ≥ 1, and in the case n > 0 we have that m ≥ 1 + MEL C g(1) + m ′ where m ′ is a sufficient segment-bound for (C, n−1, g ′ ) where g ′ is defined by (10).
We now derive an analogy of Lemma 10: Lemma 11. Let B be a sufficient size-bound for (C, n, g), where C ⊆ ∼, n ∈ N, g : N + → N + , and let Rest = SIZE B C. Then any eqlevel-decreasing (n, g)sequence starting with a pair whose eq-level is less than MinEqL(Rest) has length at most ℓ C n,g .
, and by using Prop. 5 we also derive ) is an eqlevel-decreasing (n−1, g ′ )-sequence, and B is sufficient for (C, n−1, g ′ ) (since B is assumed sufficient for (C, n, g)). The induction hypothesis thus implies that ℓ−s ≤ ℓ C n−1,g ′ , and thus ℓ ≤ 1 + MEL C g(1) + ℓ C n−1,g ′ = ℓ C n,g . ⊓ ⊔ Prover-Refuter game (third version). We separate G from the initial pair, now denoted (E 0 , F 0 ), to stress that the initial phase depends on G only. i) A grammar G = (N , Σ, R) is given. ii) Prover provides some finite set C ⊆ Terms N × Terms N , some n 0 ∈ N, a sequence of increasing values denoted g 0 (1), g 0 (2), . . . , g 0 (m) for some m ∈ N, and some B ∈ N such that C ⊆ SIZE ≤B . For each pair (E, F ) ∈ C Prover provides e ∈ N and demonstrates that EqLv(E, F ) = e (recall Prop. 2); thus C ⊆ ∼. Prover now computes ℓ C n0,g0 , using the recursive definition given before (10); this fails when B or m are not sufficiently large. iii) An initial pair (E 0 (with the least eq-level when using the least-eqlevel strategy). v) Now a play of the second game-version starts with (T 0 , U 0 ). A new feature is that Prover can claim her win when she shows that (T 1 , U 1 ), (T 2 , U 2 ), . . . contains an (n, g)-subsequence that is longer than ℓ C n0,g0 .
The least-eqlevel strategy still guarantees Refuter's win for E 0 ∼ F 0 ; Prover can never win by the new game-rule (i.e., by exceeding ℓ C n0,g0 ), due to Lemma 11. On the other hand, Prover can correctly guess C = SIZE ≤B ∩ ∼ for B that is sufficient for computing (the real) ℓ n0,g0 (related to n 0 , g 0 that are guaranteed for G by Lemma 7), and she can force her win when E 0 ∼ F 0 .
Since a winning strategy of Prover (for any G, E 0 , F 0 where E 0 ∼ F 0 ) is finitely presentable and effectively verifiable (which easily follows from the fact that Refuter always has only finitely many options when it is his turn), a proof of Theorem 1 is now clear.

Additional Remarks
Theorem 1 just states the existence of an algorithm deciding bisimulation equivalence of first-order grammars, or, in more detail, computing the respective eq-levels. But the proof can be surely adapted to more general statements. It would be a technical exercise to phrase the proof in some more general terms, not referring to bisimilarity. E.g., we could speak about some more general (stratified) equivalence with a related notion of covering B ⊳ B ′ with some properties like those captured in Prop. 3, etc. As usual, a question in such cases is to what extent it makes good sense. E.g., do we get new worthwhile decidability results in such a way?
If we look at a (straightforward) transformation from pushdown automata (PDA) to FO-grammars (given here in Appendix for completeness), we note how FO-grammars "swallow" deterministic popping ε-steps in PDA. (If there is no other rule for A than A(x 1 , . . . , x m ) ε −→ x i , then any (sub)term A(G 1 , . . . , G m ) can be immediately replaced with G i .) A question posed by Stirling was if bisimilarity of PDA with just popping ε-steps (where some nondeterminism is allowed) is still decidable. This was answered negatively in [9].
In our term-framework we extend the action set in G = (N , Σ, R) with a silent action, denoted ε, and we also allow ε-rules A(x 1 , . . . , x m ) ε −→ E. The associated LTS is then L a G = (Terms N , Σ ∪ {ε}, ( a −→) a∈Σ∪{ε} ) that naturally extends the LTS L a G defined for the case with no ε-rules. The collapsed LTS L a−col G arises from L a G by "swallowing" the ε-transitions, i.e., we have no ε- A construction in [9] shows that bisimilarity in L a−col G is undecidable, even when all ε-rules are popping, i.e. of the form A(x 1 , . . . , x m ) ε −→ x i . As also noted in [9], the same proof construction also shows that weak bisimilarity (for PDA or for L a G of FO-grammars where silent popping moves are allowed) is undecidable.
In fact, the construction for undecidability in [9] works also when we do not include the silent "post-transitions", i.e., if we require k2 = 0 in (11); thus the undecidability also holds for the respective equivalence that is finer than weak bisimilarity.
The undecidability results have been recently refined, using branching bisimilarity [22].
In branching bisimilarity we also exclude the silent "post-transitions" (as mentioned above) but there is also a "semantical" constraint: the silent "pretransitions" are supposed to be not changing the equivalence-class. Formally, given G = (N , Σ, R), where rules A(x1, . . . , xm) ε −→ G are allowed, we can define a branching bisimulation in the (non-collapsed) LTS L a G as a symmetric relation B ⊆ TermsN × TermsN where for each move E a −→ E ′ in a pair (E, F ) ∈ B, for a ∈ Σ ∪ {ε}, there is a sequence, a response, Fi) ∈ B for all i ∈ [0, k], and (E ′ , F ′ ) ∈ B; if a = ε, then it suffices that (E ′ , F ) ∈ B (i.e., the response might be empty).
For "pushing" ε-rules the construction for undecidability from [9] can be again easily adapted to branching bisimilarity. But if we only allow popping ε-rules, of the form A(x 1 , . . . , x m ) ε −→ x i , then the construction from [9] cannot be used for branching bisimilarity; there the silent "pre-transitions" do not keep the same equivalence class. This was noted by Y. Fu and Q. Yin [7] who announced a result that would translate in our setting as the decidability of branching bisimilarity of FO-grammars with popping ε-rules.
In fact, [7] also announces the decidability for pushing ε-rules in the context of so called normed PDA processes. The crucial idea is that the above "responses" −→ E ′ can be bounded in this context; i.e., Prover gets again only boundedly many possibilities how to cover a given finite set B (in the adapted version of B ⊳ B ′ ), which allows us to proceed essentially in the way that we used in this paper.
Hence Y. Fu and Q. Yin have noticed that it indeed makes good sense to try to adapt the decidability proof for bisimilarity to get further results. An adaptation of an existing proof seems necessary, since the branching bisimilarity problem that they study, in particular for PDA with popping ε-steps, does not seem to be easily reducible to the known decidable (bisimilarity) problem; one has thus to delve into the existing proofs, looking for their possible adaptations.
Y. Fu and Q. Yin have chosen to build on Stirling's paper [21]. They adapt Stirling's tableau approach to a new model that they invented. In fact, when one looks at their technical model, it seems clear that it could be smoothly replaced with the first-order-term framework used here (and already in [10], i.e., in the paper of which the authors of [7] became aware only afterwards, as they say in their conclusions). Analysing their procedure and its relation to our Prover-Refuter game would require a nontrivial technical work; here we thus suggest a direct adaptation of the game that captures the announced result.
Adaptation of Prover-Refuter game. If we want to use our framework of the Prover-Refuter game directly to branching bisimilarity of FO-grammars with popping ε-rules, thus modifying the relation B ⊳ B ′ accordingly, we encounter a technical problem. Though in a pair (E, F ) each move E a −→ E ′ (a ∈ Σ ∪ {ε}) still has only finitely many possible responses F = F 0 ε −→ F 1 ε −→ · · · ε −→ F k a −→ F ′ , their number is not bounded (by a quantity determined by the underlying grammar G), since the responses might be sinking to subterms of F in unbounded depths. This causes, e.g., that the bal-result related to a pivot might not be "boundedly close" to the pivot. But we can require that Prover avoids such unbounded responses; she can always tell, whenever she presents a new (sub)term V , if V is equivalent with a root-successor V ′ in V , and she must then behave consistently with her claims; we can imagine that she colours the respective arcs (form the root of V to the root of V ′ ) as "blue".
Recall that any response F = F0 ε −→ F1 ε −→ · · · ε −→ F k a −→ F ′ should not change the equivalence class when "sinking" from F to F k ; this sinking can be done only along such blue arcs if Prover colours the arcs correctly.
Such a blue arc, i.e. a claim that V ∼ V ′ where V ′ is a root-successor in V , can be also challenged by Refuter, but it can be used (later) for replacing V with V ′ when this should not affect the current eq-level, if Refuter uses the leasteqlevel strategy. In this way the respective possible transitions V ε −→ V ′ (where V ∼ V ′ ) are also "swallowed", similarly as deterministic popping ε-steps, which are swallowed "automatically".
In the case with no ε-rules, the "machinery" of blue arcs is not needed. But it makes sense when we consider branching bisimilarity in the case of popping ε-rules. There the relation B ⊳ B ′ is modified appropriately, and we allow Prover to use only responses F = F 0 ε −→ F 1 ε −→ · · · ε −→ F k a −→ F ′ where the "pretransitions" can only sink along blue arcs, and thus always into bounded depths. The decidability proof can be then finished analogously to the case with no ε-rules.
Further remarks on related research. Further work is needed to fully understand the discussed problems. E.g., even the case of BPA processes, generated by real-time PDA with a single control-state, is not quite clear. Here the bisimilarity problem is EXPTIME-hard [13] and in 2-EXPTIME [3] (proven explicitly in [11]); for the subclass of normed BPA the problem is polynomial [8] (see [6] for the best published upper bound).