Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete

TL;DR

This paper establishes that the problem of checking bisimulation equivalence for first-order grammars is ACKERMANN-complete, providing the first complexity bounds and showing fixed-state cases are primitive-recursive.

Contribution

It introduces the first known complexity upper bound for bisimulation equivalence of first-order grammars, proving ACKERMANN-completeness and analyzing fixed-state cases.

Findings

Bisimulation equivalence for first-order grammars is ACKERMANN-complete.

Strong bisimilarity is primitive-recursive with fixed number of states.

Provides the first complexity bounds for this problem.

Abstract

Checking whether two pushdown automata with restricted silent actions are weakly bisimilar was shown decidable by S\'enizergues (1998, 2005). We provide the first known complexity upper bound for this famous problem, in the equivalent setting of first-order grammars. This ACKERMANN upper bound is optimal, and we also show that strong bisimilarity is primitive-recursive when the number of states of the automata is fixed.

Tables

Table 1. Table 1. The complexity of equivalence problems over pushdown processes.

Problem	Lower bound	Upper bound
DPDA lang. equ.​​​​	¶	\ComplexityFontTOWER [37, 18]
strong bisim.	​​\ComplexityFontTOWER [1]​​	​​ \ComplexityFontACKERMANN [this paper]
weak bisim.$a$	​​\ComplexityFontACKERMANN [18]​​	​​ \ComplexityFontACKERMANN [this paper]

Table 2. Table 2. Grammatical constants defined in  [ 20 ] .

Constant		Ref. in [20]	Ref. here	Growth in $\left|𝒢\right|$
$m$$=$	${\max }_{A\in 𝒩}r\left(A\right)$	(7)	(2)	linear
hinc$=$	${\max }_{E\in \text{rhs}}0ptE-1$	(4)	(3)	linear
sinc$=$	${\max }_{E\in \text{rhs}}\text{ntsize}\left(E\right)$	(5)	(4)	linear
$d_0$$=$	$1+{\max }_{A\in 𝒩,1\le i\le r\left(A\right)}\left|w_{[A,i]}\right|$	(6)	(5)	exponential
$d_1$$=$	$2\left|𝒩\right|{\left(\max \{d_0,{\left|ℛ\right|}^{d_0}\}\right)}^{m+2}$	(13)		doubly exponential
$d_2$$=$	$d_0+\left(1+d_0\text{hinc}\right)\left(d_0-1\right)$	(19)		exponential
$d_3$$=$	${\left(\max \{d_0,{\left|ℛ\right|}^{d_0}\}\right)}^2$	(21)		doubly exponential
$n$$=$	$m^{d_0}$	(24)	(6)	doubly exponential
$s$$=$	$m^{d_0+1}+\left(m+2\right)d_0\text{sinc}+\left(d_2+d_0-1\right)\text{sinc}$	(25)		doubly exponential
$g$$=$	$\left(d_2+d_0-1\right)\text{sinc}$	(26)		exponential
$d_4$$=$	$d_1{\left(1+{\sum }_{E\in \text{rhs}}\text{ntsize}\left(E\right)\right)}^{d_2+d_0-1}$	(23)		doubly exponential
$d_5$$=$	$\left(d_2+d_0-1\right)\left(1+\left(d_0-1\right)\text{hinc}\right)$	(31)		doubly exponential
$c$$=$	$\max \{d_3,2d_4{d}_5\}$	(38)		doubly exponential

Equations

$$x\sigma$$

$${\mathcal{L}}_{\mathcal{G}}\stackrel{\text{scalebox}0.5def}{=}(\text{textsc}{Terms}_{\mathcal{N}},\Sigma ,(\stackrel{a}{\to }{)}_{a\in \Sigma })$$

$$A(x_1,\dots ,x_{r(A)})\sigma \stackrel{a}{\to }E\sigma$$

$$|\mathcal{G}|$$

$$m$$

$$\stackrel{\text{scalebox}0.5def}{=}\underset{E\in \text{textsc}rhs}{\max }0ptE-1,$$

$$\stackrel{\text{scalebox}0.5def}{=}\underset{E\in \text{textsc}rhs}{\max }\text{textsc}ntsize(E)$$

$$d_0\stackrel{\text{scalebox}0.5def}{=}1+\underset{A\in \mathcal{N},1\le i\le r(A)}{\max }|w_{[A,i]}|\le 1+(2+\text{textsc}hinc{)}^{|\mathcal{N}|m};$$

$$n\stackrel{\text{scalebox}0.5def}{=}{m}^{d_0};$$

$$\mathcal{L}=(\mathcal{S},\Sigma ,(\stackrel{a}{\to }{)}_{a\in \Sigma })$$

$${\sim }_0\supseteq {\sim }_1\supseteq \cdots \supseteq \sim$$

$$\text{textsc}el(s,t)\stackrel{\text{scalebox}0.5def}{=}\sup \{k\in \mathbb{N}\mid s{\sim }_{k}t\}.$$

$$e_i$$

$$s_{i-1}$$

$${\mathcal{E}}_{\mathcal{B}}\stackrel{\text{scalebox}0.5def}{=}n+1+\sum _{i=0}^n{e}_i.$$

$$\text{textsc}{Pairs}_i\stackrel{\text{scalebox}0.5def}{=}\{(E,F)\mid \exists j\le i.\text{textsc}var(E,F)=\{x_1,\dots ,x_j\}\wedge \text{textsc}size(E,F)\le s_i\}.$$

$$\textsc{el}(E,F)\leq c\cdot\big{(}\mathcal{E}_{\mathcal{B}_{n,s,g}}\cdot\textsc{size}(E,F)+\textsc{size}(E,F)^{2}\big{)}\;.$$

$$\textsc{el}(E,F)\leq c\cdot\big{(}\mathcal{E}_{\mathcal{B}}\cdot\textsc{size}(E,F)+\textsc{size}(E,F)^{2}\big{)}\;.$$

$$\alpha \stackrel{\text{scalebox}0.5def}{=}{\omega }^n\cdot |{\mathcal{P}}_n|+\cdots +{\omega }^0\cdot |{\mathcal{P}}_0|.$$

$${\alpha }_0>{\alpha }_1>\cdots$$

$$\alpha ={\omega }^n\cdot c_n+\cdots +{\omega }^0\cdot c_0$$

$$\Vert \alpha \Vert \stackrel{\text{scalebox}0.5def}{=}\max \{n,\underset{0\le i\le n}{\max }{c}_i\}.$$

$$\Vert {\alpha }_{\ell }\Vert \le h^{\ell }(N_0),$$

$${\omega }^{\omega }(x)$$

$$h^0(x)$$

$$h^{\alpha +1}(x)$$

$$h^{\lambda }(x)$$

$$h^{\alpha }\circ h^{\beta }(x)=h^{\alpha +\beta }(x),$$

$$\text{if x≤y, then }x\le h^{\alpha }(x)\le h^{\alpha }(y).$$

$$h^{h_{\alpha }(x)}(x)=h^{\alpha }(x).$$

$$N$$

$$N_{\ell }$$

$$L$$

$${\mathcal{E}}_{\mathcal{B}}$$

$$|\textsc{Pairs}_{i}|\leq\big{(}(|\mathcal{N}|+i)\cdot s_{i}^{m}\big{)}^{s_{i}}\cdot s_{i}^{2}\leq 2^{3s_{i}|\mathcal{G}|\log n\log s_{i}}\;.$$

Full text

1. Introduction

Bisimulation equivalence plays a central role among the many notions of semantic equivalence studied in verification and concurrency theory [11]. Indeed, two bisimilar processes always satisfy exactly the same specifications written in modal logics [2] or in the modal $\mu$-calculus [14], allowing one to replace for instance a naive implementation with a highly optimised one without breaking the conformance. As a toy example, the two recursive Erlang functions below implement the same stateful message relaying service, that either receives {upd, M1} and updates its internal message from M to M1, or receives {rel,C} and sends the message M to the client C.

⬇

1serverA(M) $\rightarrow{}$ serverB(M) $\rightarrow{}$

2 receive M2 = receive

3 {upd, M1} $\rightarrow{}$ serverA(M1); {upd, M1} $\rightarrow{}$ M1;

4 {rel, C } $\rightarrow{}$ C!M, {rel, C } $\rightarrow{}$ C!M, M;

5 serverA(M); end,

6 end.    serverB(M2).

The two programs are weakly bisimilar if we only observe the input (receive) and output (C!M) actions, but the one on the left is not tail-recursive and might perform poorly compared to the one on the right.

In a landmark 1998 paper, Sénizergues [32, 34] proved the decidability of bisimulation equivalence for rooted equational graphs of finite out-degree. The proof extends his previous seminal result [31, 33], which is the decidability of language equivalence for deterministic pushdown automata (DPDA), and entails that weak bisimilarity of pushdown processes where silent actions are deterministic is decidable; a silent action (also called an $\varepsilon$-step) is deterministic if it has no alternative when enabled. Because the control flow of a first-order recursive program is readily modelled by a pushdown process, one can view this result as showing that the equivalence of recursive programs (like the two Erlang functions above) is decidable as far as their observable behaviours are concerned, provided silent moves are deterministic. Regarding decidability, Sénizergues’ result is optimal in the sense that bisimilarity becomes undecidable if we consider either nondeterministic (popping) $\varepsilon$-steps [21], or second-order pushdown processes with no $\varepsilon$-steps [4]. Note that the decidability border was also refined in [39] by considering branching bisimilarity, a stronger version of weak bisimilarity.

Computational Complexity

While this delineates the decidability border for equivalences of pushdown processes, the computational complexity of the bisimilarity problem is open. Sénizergues’ algorithm consists in two semi-decision procedures, with no clear means of bounding its complexity, and subsequent works like [17] have so far not proven easier to analyse. We know however that this complexity must be considerable, as the problem is \ComplexityFontTOWER-hard in the real-time case (i.e., without silent actions, hence for strong bisimilarity) [1] and \ComplexityFontACKERMANN-hard in the general case (with deterministic silent actions) [18]—we are employing here the ‘fast-growing’ complexity classes defined in [29], where $\ComplexityFont{TOWER}=\ComplexityFont{F}_{\!3}$ is the lowest non elementary class and $\ComplexityFont{ACKERMANN}=\ComplexityFont{F}_{\!\omega}$ the lowest non primitive-recursive one.

In fact, the precise complexity of deciding equivalences for pushdown automata and their restrictions is often not known—as is commonplace with infinite-state processes [35]. For instance, language equivalence of deterministic pushdown automata is ¶-hard and was shown to be in \ComplexityFontTOWER by Stirling [37] (see [18] for an explicit upper bound), and bisimilarity of BPAs (i.e., real-time pushdown processes with a single state) is \ComplexityFontEXPTIME-hard [22] and in \ComplexityFont2EXPTIME [5] (see [16] for an explicit proof). There are also a few known completeness results in restricted cases: bisimilarity of normed BPAs is ¶-complete [13] (see [10] for the best known upper bound), bisimilarity of real-time one-counter processes (i.e., of pushdown processes with a singleton stack alphabet) is \PSPACE-complete [3], and bisimilarity of visibly pushdown processes is \ComplexityFontEXPTIME-complete [36].

Contributions

In this paper, we prove that the bisimilarity problem for pushdown processes is in $\ComplexityFont{ACKERMANN}$, even the weak bisimilarity problem when silent actions are deterministic. Combined with the already mentioned lower bound from [18], this shows the problem to be \ComplexityFontACKERMANN-complete. This is the first instance of a complexity completeness result in the line of research originating from Sénizergues’ work [31, 32, 33, 34]; see Tab. 1.

Rather than working with rooted equational graphs of finite out-degree or with pushdown processes with deterministic silent actions, our proof is cast in the formalism of first-order grammars (see Sec. 2), which are term rewriting systems with a head rewriting semantics, and are known to generate the same class of graphs [7].

Our proof heavily relies on the main novelty from [17]: the bisimilarity of two arbitrary terms according to a first-order grammar essentially hinges on a finite basis of pairs of non-equivalent terms, which can be constructed from the grammar independently of the terms provided as input. The basis provides a number that allows us to compute a bound on the ‘equivalence-level’ of two non-equivalent terms; this is the substance of the decision procedure (see Sec. 3). Both in [17] and in its reworked version in [20], such a basis is obtained through a brute force argument, which yields no complexity statement. In Sec. 4 we exhibit a concrete algorithm computing the basis, and we analyse its complexity in the framework of [28, 29, 30] in Sec. 5, yielding the \ComplexityFontACKERMANN upper bound.

Finally, although our results do not match the \ComplexityFontTOWER lower bound of Benedikt et al. [1] in the case of real-time pushdown processes, we nevertheless show in Sec. 6 that bisimilarity becomes primitive-recursive in that case if additionally the number of control states of the pushdown processes is fixed.

2. First-Order Grammars

First-order grammars are labelled term rewriting systems with a head rewriting semantics. They are a natural model of first-order functional programs with a call-by-name semantics, and were shown to generate the class of rooted equational graphs of finite out-degree by Caucal [6, 7], where they are called term context-free grammars. Here we shall use the terminology and notations from [20].

2.1. Regular Terms

Let $\mathcal{N}$ be a finite ranked alphabet, i.e., where each symbol $A$ in $\mathcal{N}$ comes with an arity $r(A)$ in \mathbb{N}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\{0,1,2,\dots\}, and \textsc{Var}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\{x_{1},x_{2},\dots\} a countable set of variables, all with arity zero. We work with possibly infinite regular terms over $\mathcal{N}$ and Var, i.e., terms with finitely many distinct subterms. Let $\textsc{Terms}_{\mathcal{N}}$ denote the set of all regular terms over $\mathcal{N}$ and Var. We further use $A,B,C,D$ for nonterminals, and $E,F$ for terms, possibly primed and/or with subscripts.

Representations

Such terms can be represented by finite directed graphs as shown in Fig. 1, where each node has a label in $\mathcal{N}\cup\textsc{Var}$ and a number of ordered outgoing arcs equal to its arity. The unfolding of the graph representation is the desired term, and there is a bijection between the nodes of the least graph representation of a term $E$ and the set of subterms of $E$.

Size and Height

We define the size $\textsc{size}(E)$ of a term $E$ as its number of distinct subterms. For instance, $\textsc{size}(E_{1})=6$, $\textsc{size}(E_{2})=9$, and $\textsc{size}(E_{3})=5$ in Fig. 1. For two terms $E$ and $F$, we also denote by $\textsc{size}(E,F)$ the number of distinct subterms of $E$ and $F$; note that $\textsc{size}(E,F)$ can be smaller than $\textsc{size}(E)+\textsc{size}(F)$, as they might share some subterms. For instance, $\textsc{size}(E_{1},E_{2})=9$ in Fig. 1. We let $\textsc{ntsize}(E)$ denote the number of distinct subterms of $E$ with root labels in $\mathcal{N}$; e.g., $\textsc{ntsize}(E_{1})=4$ in Fig. 1. A term $E$ is thus finite if and only if its graph representation is acyclic, in which case it has a height $0ptE$, which is the maximal length of a path from the root to a leaf; for instance $0pt{E_{1}}=3$ in Fig. 1. Finally, we let $\textsc{var}(E)$ denote the set of variables occurring in $E$, and let \textsc{var}(E,F)\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\textsc{var}(E)\cup\textsc{var}(F); e.g., $\textsc{var}(E_{1},E_{2})=\{x_{2},x_{5}\}$ in Fig. 1.

2.2. Substitutions

A substitution $\sigma$ is a map $\textsc{Var}\to\textsc{Terms}_{\mathcal{N}}$ whose support \textsc{supp}(\sigma)\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\{x\in\textsc{Var}\mid\sigma(x)\neq x\} is finite. This map is lifted to act over terms by

[TABLE]

for all $x$ in Var, $A$ in $\mathcal{N}$, and $E_{1},\dots,E_{r(A)}$ in $\textsc{Terms}_{\mathcal{N}}$. For instance, in Fig. 1, $E_{2}=E_{1}\sigma$ if $\sigma(x_{2})=E_{1}$ and $\sigma(x_{5})=x_{5}$.

2.3. Grammars

A first-order grammar is a tuple $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$ where $\mathcal{N}$ is a finite ranked alphabet of nonterminals, $\Sigma$ a finite alphabet of actions, and $\mathcal{R}$ a finite set of labelled term rewriting rules of the form $A(x_{1},\dots,x_{r(A)})\xrightarrow{a}E$ where $A\in\mathcal{N}$, $a\in\Sigma$, and $E$ is a finite term in $\textsc{Terms}_{\mathcal{N}}$ with $\textsc{var}(E)\subseteq\{x_{1},\dots,x_{r(A)}\}$.

Head Rewriting Semantics

A first-order grammar $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$ defines an infinite labelled transition system

[TABLE]

over $\textsc{Terms}_{\mathcal{N}}$ as set of states, $\Sigma$ as set of actions, and with a transition relation ${\xrightarrow{a}}\subseteq\textsc{Terms}_{\mathcal{N}}\times\textsc{Terms}_{\mathcal{N}}$ for each $a\in\Sigma$, where each rule $A(x_{1},\dots,x_{r(A)})\xrightarrow{a}E$ of $\mathcal{R}$ induces a transition

[TABLE]

for every substitution $\sigma$. This means that rewriting steps can only occur at the root of a term, rather than inside a context. For instance, the rules $A(x_{1},x_{2},x_{3})\xrightarrow{a}C(x_{2},D(x_{2},x_{1}))$ and $A(x_{1},x_{2},x_{3})\xrightarrow{b}x_{2}$ give rise on the terms of Fig. 1 to the transitions $E_{1}\xrightarrow{a}C(x_{5},D(x_{5},D(x_{5},C(x_{2},B))))$ and $E_{1}\xrightarrow{b}x_{5}$. The transition relations $\xrightarrow{a}$ are extended to $\xrightarrow{w}$ for words $w\in\Sigma^{\ast}$ in the standard way.

Note that variables $x\in\textsc{Var}$ are ‘dead’, in that no transitions can be fired from a variable. In fact, in Sec. 3.1 we discuss that for technical reasons we could formally assume that each variable $x$ has its unique action $a_{x}$ and a transition $x\xrightarrow{a_{x}}x$.

Grammatical Constants

Let us fix a first-order grammar $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$. We define its size as

[TABLE]

bound respectively the maximal arity of its nonterminals, its maximal height increase in one transition step, and its maximal size increase in one transition step.

If $A(x_{1},\dots,x_{r(A)})\xrightarrow{w}x_{i}$ in $\mathcal{L}_{\mathcal{G}}$ for some $i$ in $\{1,\dots,r(A)\}$ and $w$ in $\Sigma^{\ast}$, then we call $w$ an $(A,i)$-sink word. Observe that $w\neq\varepsilon$, hence $w=aw^{\prime}$ with $A(x_{1},\dots,x_{r(A)})\xrightarrow{a}E$ in $\mathcal{R}$ and $E\xrightarrow{w^{\prime}}x_{i}$, where either $w^{\prime}=\varepsilon$ and $E=x_{i}$ or $E$ ‘sinks’ to $x_{i}$ when applying $w^{\prime}$. Thus, for each $A\in\mathcal{N}$ and $i\in\{1,\dots,r(A)\}$ we can compute some shortest $(A,i)$-sink word $w_{[A,i]}$ by dynamic programming; in the cases where no $(A,i)$-sink word exist, we can formally put w_{[A,i]}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\varepsilon. In turn, this entails that the maximal length of shortest sink words satisfies

[TABLE]

here and in later instances, we let \max\emptyset\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}0.

Finally, the following grammatical constant $n$ from [20] is important for us:

[TABLE]

note that $n$ is at most doubly exponential in the size of $\mathcal{G}$. This $n$ was chosen in [20] so that each $E$ can be written as $E^{\prime}\sigma$ where $0pt{E^{\prime}}\leq d_{0}$ and $\textsc{var}(E^{\prime})\subseteq\{x_{1},\dots,x_{n}\}$, and it is guaranteed that each path $E\xrightarrow{w}F$ where $|w|\leq d_{0}$ can be presented as $E^{\prime}\sigma\xrightarrow{w}F^{\prime}\sigma$ where $E^{\prime}\xrightarrow{w}F^{\prime}$. Put simply: $n$ bounds the number of depth-$d_{0}$ subterms for each term $E$.

3. Bisimulation Equivalence

Bisimulation equivalence has been introduced independently in the study of modal logics [2] and in that of concurrent processes [25, 26]. We recall here the basic notions surrounding bisimilarity before we introduce the key notion of candidate bases as defined in [20].

3.1. Equivalence Levels

Consider a labelled transition system

[TABLE]

like the one defined by a first-order grammar, with set of states $\mathcal{S}$, set of actions $\Sigma$, and a transition relation ${\xrightarrow{a}}\subseteq\mathcal{S}\times\mathcal{S}$ for each $a$ in $\Sigma$. We work in this paper with image-finite labelled transition systems, where $\{s^{\prime}\in\mathcal{S}\mid s\xrightarrow{a}s^{\prime}\}$ is finite for every $s$ in $\mathcal{S}$ and $a$ in $\Sigma$. In this setting, the coarsest (strong) bisimulation $\sim$ can be defined through a chain

[TABLE]

of equivalence relations over $\mathcal{S}\times\mathcal{S}$: let {\sim_{0}}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\mathcal{S}\times\mathcal{S} and for each $k$ in $\mathbb{N}$, let $s\sim_{k+1}t$ if $s\sim_{k}t$ and

[]

**(zig): **

if $s\xrightarrow{a}s^{\prime}$ for some $a\in\Sigma$, then there exists $t^{\prime}$ such that $t\xrightarrow{a}t^{\prime}$ and $s^{\prime}\sim_{k}t^{\prime}$, and

**(zag): **

if $t\xrightarrow{a}t^{\prime}$ for some $a\in\Sigma$, then there exists $s^{\prime}$ such that $s\xrightarrow{a}s^{\prime}$ and $s^{\prime}\sim_{k}t^{\prime}$.

We put \sim_{\omega}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\bigcap_{k\in\mathbb{N}}{\sim_{k}}; hence ${\sim}={\sim_{\omega}}$.

For each pair $s,t$ of states in $\mathcal{S}$, we may then define its equivalence level $\textsc{el}(s,t)$ in $\omega+1=\mathbb{N}\uplus\{\omega\}$ as

[TABLE]

Here we should add that—to be consistent with [20]—we stipulate that $\textsc{el}(x,E)=0$ when $E\neq x$; in particular $\textsc{el}(x_{i},x_{j})=0$ when $i\neq j$. This would automatically hold if we equipped each $x\in\textsc{Var}$ with a special transition $x\xrightarrow{a_{x}}x$ in $\mathcal{L}_{\mathcal{G}}$, as we already mentioned. This stipulation guarantees that $\textsc{el}(E,F)\leq\textsc{el}(E\sigma,F\sigma)$.

Two states $s,t$ are (strongly) bisimilar if $s\sim t$, which is if and only if $\textsc{el}(s,t)=\omega$. We will later show an algorithm computing the equivalence level of two given terms in the labelled transition system defined by a given first-order grammar. The main decision problem in which we are interested is the following.

Problem** (Bisimulation).**

[]

**input: **

A first-order grammar $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$ and two terms $E,F$ in $\textsc{Terms}_{\mathcal{N}}$.

**question: **

Is $\textsc{el}(E,F)=\omega$ in the labelled transition system $\mathcal{L}_{\mathcal{G}}$?

3.2. Bisimulation Game

Observe that the following variant of the bisimulation problem is decidable.

Problem** (Bounded Equivalence Level).**

[]

**input: **

A first-order grammar $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$, two terms $E,F$ in $\textsc{Terms}_{\mathcal{N}}$, and $e$ in $\mathbb{N}$.

**question: **

Is $\textsc{el}(E,F)\leq e$ in the labelled transition system $\mathcal{L}_{\mathcal{G}}$?

Indeed, as is well-known, the zig-zag condition can be recast as a bisimulation game between two players called Spoiler and Duplicator. A position of the game is a pair $(s_{1},s_{2})\in\mathcal{S}\times\mathcal{S}$. Spoiler wants to prove that the two states are not bisimilar, while Duplicator wants to prove that they are bisimilar. The game proceeds in rounds; in each round,

• •

Spoiler chooses $i\in\{1,2\}$ and a transition $s_{i}\xrightarrow{a}s^{\prime}_{i}$ (if no such transition exists, Spoiler loses), then

• •

Duplicator chooses a transition $s_{3-i}\xrightarrow{a}s^{\prime}_{3-i}$ with the same label $a$ (if no such transition exists, Duplicator loses);

the game then proceeds to the next round from position $(s^{\prime}_{1},s^{\prime}_{2})$. Then $\textsc{el}(s_{1},s_{2})\leq k$ if and only if Spoiler has a strategy to win in the $(k{+}1)$th round at the latest when starting the game from $(s_{1},s_{2})$. Note that this game is determined and memoryless strategies suffice.

Thus, the bounded equivalence level problem can be solved by an alternating Turing machine that first writes the representation of $E$ and $F$ on its tape, and then plays at most $e$ rounds of the bisimulation game, where each round requires at most a polynomial number of computational steps in the size of the grammar (assuming a somewhat reasonable tape encoding of the terms).

Fact 1**.**

*The bounded equivalence level problem is in

\ComplexityFont{ATIME}\big{(}\textsc{size}(E,F)+\poly(|\mathcal{G}|)\cdot e\big{)}.*

3.3. Candidate Bases

Consider some fixed first-order grammar $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$. Given three numbers $n$, $s$, and $g$ in $\mathbb{N}$—which will depend on $\mathcal{G}$—, an $(n,s,g)$-candidate basis for non-equivalence is a set of pairs of terms $\mathcal{B}\subseteq\textsc{Terms}_{\mathcal{N}}\times\textsc{Terms}_{\mathcal{N}}$ associated with two sequences of numbers $(s_{i})_{0\leq i\leq n}$ and $(e_{i})_{0\leq i\leq n}$ such that

1. (1)

$\mathcal{B}\subseteq{\nsim}$, 2. (2)

for each $(E,F)\in\mathcal{B}$ there is $i\in\{0,\dots,n\}$ such that $\textsc{var}(E,F)=\{x_{1},\dots,x_{i}\}$ and $\textsc{size}(E,F)\leq s_{i}$, 3. (3)

s_{n}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}s, and the remaining numbers are defined inductively by

[TABLE]

Note that the numbers $(s_{i})_{0\leq i\leq n}$ and $(e_{i})_{0\leq i\leq n}$ are entirely determined by $\mathcal{B}$ and $n$, $s$, and $g$. An $(n,s,g)$-candidate basis $\mathcal{B}$ yields a bound $\mathcal{E}_{\mathcal{B}}$ defined by

[TABLE]

Full Bases

For $0\leq i\leq n$, let

[TABLE]

An $(n,s,g)$-candidate basis $\mathcal{B}$ is full below some equivalence level $e\in\omega+1$ if, for all $0\leq i\leq n$ and all $(E,F)\in\textsc{Pairs}_{i}$ such that $\textsc{el}(E,F)<e$ we have $(E,F)\in\mathcal{B}$. We say that $\mathcal{B}$ is full if it is full below $\omega$. In other words and because $\mathcal{B}\subseteq{\nsim}$, $\mathcal{B}$ is full if and only if, for all $0\leq i\leq n$, $\textsc{Pairs}_{i}\setminus\mathcal{B}\subseteq{\sim}$.

Proposition 2** ([20, Prop. 9]).**

For any $n,s,g$, there is a unique full $(n,s,g)$-candidate basis, denoted by $\mathcal{B}_{n,s,g}$.

Proof.

The full candidate basis $\mathcal{B}_{n,s,g}$ is constructed by induction over $n$. Let s_{n}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}s and consider the finite set S_{n}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\{(E,F)\in\textsc{Terms}_{\mathcal{N}}\times\textsc{Terms}_{\mathcal{N}}\mid E\nsim F\wedge\exists j\leq n\mathbin{.}\textsc{var}(E,F)=\{x_{1},\dots,x_{j}\}\wedge\textsc{size}(E,F)\leq s_{n}\}; $S_{n}$ has a maximal equivalence level e_{n}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\max_{(E,F)\in S_{n}}\textsc{el}(E,F). If $n=0$, we define \mathcal{B}_{0,s,g}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}S_{0}. Otherwise, we let s_{n-1}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}2s_{n}+g+e_{n}(\textsc{sinc}+g) as in (9); by induction hypothesis there is a unique full $(n-1,s_{n-1},g)$-candidate basis $\mathcal{B}_{n-1,s_{n-1},g}$ and we set \mathcal{B}_{n,s,g}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}S_{n}\cup\mathcal{B}_{n-1,s_{n-1},g}. ∎

The main result from [20] can now be stated.

Theorem 3** ([20, Thm. 7]).**

Let $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$ be a first-order grammar. Then one can compute a grammatical constant $g$ exponential in $|\mathcal{G}|$ and grammatical constants $n$, $s$, and $c$ doubly exponential in $|\mathcal{G}|$ such that, for all terms $E,F$ in $\textsc{Terms}_{\mathcal{N}}$ with $E\nsim F$,

[TABLE]

Theorem 3 therefore shows that the bisimulation problem can be reduced to the bounded equivalence level problem, provided one can compute the full $(n,s,g)$-candidate basis for suitable $n$, $s$, and $g$—see Tab. 2 in the appendix for details on how the grammatical constants $n$, $s$, $c$, and $g$ are defined in [20]. Our goal in Sec. 4 will thus be to exhibit a concrete algorithm computing the full candidate basis $\mathcal{B}_{n,s,g}$, in order to derive an upper bound on $\mathcal{E}_{\mathcal{B}_{n,s,g}}$.

The proof of [20, Thm. 7] relies on the following insight, which we will also need in order to prove the correctness of our algorithm.

Lemma 4** ([20, Eq. 39]).**

Let $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$ be a first-order grammar, $g,n,s,c$ be defined as in Thm. 3, $E,F$ be two terms in $\textsc{Terms}_{\mathcal{N}}$ with $E\not\sim F$, and $\mathcal{B}$ be an $(n,s,g)$-candidate basis full below $\textsc{el}(E,F)$. Then

[TABLE]

4. Computing Candidate Bases

Theorem 3 shows that, in order to solve the bisimulation problem, it suffices to compute $c$ and $\mathcal{E}_{\mathcal{B}_{n,s,g}}$ and then solve the bounded equivalence problem, for which Fact 1 provides a complexity upper bound. In this section, we show how to compute $\mathcal{E}_{\mathcal{B}_{n,s,g}}$ for an input first-order grammar $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$. Note that this grammatical constant was shown computable in [17, 20] through a brute-force argument, but here we want a concrete algorithm, whose complexity will be analysed in Sec. 5. We proceed in two steps, by first considering a non effective version in Sec. 4.1, whose correctness is straightforward, and then the actual algorithm in Sec. 4.2.

4.1. Non Effective Version

Throughout this section, we consider $n$ as a fixed parameter. We first assume that we have an oracle $\textsc{EqLevel}(\mathcal{G},\mathcal{E}_{\mathcal{B}},c,E,F)$ at our disposal, that returns the equivalence level $\textsc{el}(E,F)$ in $\mathcal{L}_{\mathcal{G}}$; the parameters $\mathcal{E}_{\mathcal{B}},c$ will be used in the effective version in Sec. 4.2. The following procedure then constructs full $(n,s,g)$-candidate basis $\mathcal{B}_{n,s,g}$ and its associated bound $\mathcal{E}_{\mathcal{B}_{n,s,g}}$, by progressively adding pairs from the sets $\textsc{Pairs}_{i}$ until the candidate basis is full. In order not to clutter the presentation too much, we assume implicitly that the equivalence level $e$ of each pair $(E,F)$ added to $\mathcal{B}$ on line 14 is implicitly stored, thus it does not need to be recomputed on line 19.

1 procedure CandidateBoundn($\mathcal{G}$, $s$, $g$, $c$)

2      \mathcal{B}\leftarrow\emptyset$$\triangleright Initialisation

3      for $i\leftarrow 0,\dots,n$ do

4          $e_{i}\leftarrow 0$      

5      $s_{n}\leftarrow s$

6      for $i\leftarrow n-1,\dots,0$ do

7          $s_{i}\leftarrow 2s_{i+1}+g$      

8      $\mathcal{E}_{\mathcal{B}}\leftarrow n+1$

9      for $i\leftarrow n,\dots,0$ do

10          $\mathcal{P}_{i}\leftarrow\textsc{Pairs}_{i}\setminus\bigcup_{i<j\leq n}\mathcal{P}_{j}$      

11      while $\exists i\in\{0,1,\dots,n\}\mathbin{,}\exists(E,F)\in\mathcal{P}_{i}:$ $\textsc{EqLevel}(\mathcal{G},\mathcal{E}_{\mathcal{B}},c,E,F)<\omega$ do

12          e\leftarrow\textsc{EqLevel}(\mathcal{G},\mathcal{E}_{\mathcal{B}},c,E,F)$$\triangleright Main loop

13          $\mathcal{P}_{i}\leftarrow\mathcal{P}_{i}\setminus\{(E,F)\}$

14          $\mathcal{B}\leftarrow\mathcal{B}\cup\{(E,F)\}$

15          if $e>e_{i}$ **then$\triangleright$ If so, then update **

16               $e_{i}\leftarrow e$

17               for $j\leftarrow i-1,\dots,0$ do

18                   $s_{j}\leftarrow 2s_{j+1}+g+e_{j+1}(\textsc{sinc}+g)$

19                   $e_{j}\leftarrow\max_{(E,F)\in\mathcal{B}\mid\textsc{size}(E,F)\leq s_{j}}\textsc{el}(E,F)$

20                   $\mathcal{P}_{j}\leftarrow\textsc{Pairs}_{j}\setminus(\mathcal{B}\cup\bigcup_{i<k\leq n}\mathcal{P}_{k})$               

21               $\mathcal{E}_{\mathcal{B}}\leftarrow n+1+\sum_{0\leq j\leq n}e_{j}$               

22      return $\mathcal{E}_{\mathcal{B}}$

Invariant

The procedure $\textsc{CandidateBound}_{n}$ maintains as an invariant of its main loop on lines 11–21 that $\mathcal{B}$ is an $(n,s,g)$-candidate basis associated with the numbers $(s_{i})_{0\leq i\leq n}$ and $(e_{i})_{0\leq i\leq n}$, and that $\mathcal{E}_{\mathcal{B}}$ is its associated bound. This holds indeed after the initialisation phase on lines 2–8, and is then enforced in the main loop by the update instructions on lines 15–21.

Correctness

Let us check that, if it terminates, this non effective version does indeed return the bound $\mathcal{E}_{\mathcal{B}_{n,s,g}}$ associated with the unique full $(n,s,g)$-candidate basis $\mathcal{B}_{n,s,g}$. By the previous invariant, it suffices to show that $\mathcal{B}$ is full when the procedure terminates. Consider for this some index $0\leq i\leq n$ and a pair $(E,F)\in\textsc{Pairs}_{i}$ with $\textsc{el}(E,F)=e$ for some $e<\omega$. By definition of the sets $(\mathcal{P}_{i})_{0\leq i\leq n}$ on lines 9–10 and their updates on lines 13 and 20 in the main loop, the pair $(E,F)$ must have been added to some $\mathcal{P}_{j}$ for $j\geq i$. Then the pair must have been selected by the condition of the main loop on line 11, and added to $\mathcal{B}$.

Termination

Although we are still considering a non effective version of the algorithm, the proof that it always terminates is the same as the one for the effective version in Sec. 4.2. We exhibit a ranking function on the main loop, thereby showing that it must stop eventually. More precisely, each time we enter the main loop on line 11, we associate to the current state of the procedure the ordinal rank below $\omega^{n+1}$ defined by111 Note that this is equivalent to defining the rank as the tuple $(|\mathcal{P}_{n}|,\dots,|\mathcal{P}_{0}|)$ in $\mathbb{N}^{n+1}$, ordered lexicographically, but ordinal notations are more convenient for our analysis in Sec. 5.

[TABLE]

This defines a descending sequence of ordinals

[TABLE]

of ordinals, where $\alpha_{\ell}$ is the rank after $\ell$ iterations of the main loop. Indeed, each time we enter the loop, the cardinal $|\mathcal{P}_{i}|$ of the set under consideration strictly decreases on line 13, and is not modified by the updates on line 20, which only touch the sets $\mathcal{P}_{j}$ for $j<i$. Hence $\textsc{CandidateBound}_{n}$ terminates.

4.2. Effective Version

In order to render $\textsc{CandidateBound}_{n}$ effective, we provide an implementation of EqLevel that does not require an oracle for the bisimulation problem, but relies instead on Lem. 4 and the bounded equivalence level problem, which as we saw in Sec. 3.2 is decidable.

1 procedure EqLevel($\mathcal{G}$, $\mathcal{E}_{\mathcal{B}}$, $c$, $E$, $F$)

2      if \textsc{el}(E,F)\leq c\cdot\big{(}\mathcal{E}_{\mathcal{B}}\cdot\textsc{size}(E,F)+\textsc{size}(E,F)^{2}\big{)} then

3          return $\textsc{el}(E,F)$

4      else

5          return $\omega$

We establish the correctness of this effective variant in the following theorem, which uses the same reasoning as the proof of [20, Thm. 7].

Theorem 5**.**

The effective version of procedure $\textsc{CandidateBound}_{n}(\mathcal{G},s,g,c)$ terminates and, provided $n$, $s$, $c$, and $g$ are defined as in Thm. 3, returns the bound $\mathcal{E}_{\mathcal{B}_{n,s,g}}$.

Proof.

Termination is guaranteed by the ranking function defined by (12). Regarding correctness, assume the provided $g$, $n$, $s$, and $c$ are defined as in Thm. 3, and let us define a (reflexive and symmetric) relation $\dot{\sim}_{k}$ on $\textsc{Terms}_{\mathcal{N}}$ by $E\mathrel{\dot{\sim}_{k}}F$ if and only if \textsc{el}(E,F)>c\cdot\big{(}k\cdot\textsc{size}(E,F)+\textsc{size}(E,F)^{2}\big{)}. Clearly, ${\sim}\subseteq{\dot{\sim}_{k}}$ for all $k$ in $\mathbb{N}$. We say that an $(n,s,g)$-candidate basis is $k$-complete if, for all $0\leq i\leq n$, $\textsc{Pairs}_{i}\setminus\mathcal{B}\subseteq{\dot{\sim}_{k}}$. We call $\mathcal{B}$ complete if it is $\mathcal{E}_{\mathcal{B}}$-complete. By the reasoning we used for showing the correctness of the non effective version, when the effective version of $\textsc{CandidateBound}_{n}$ terminates, $\mathcal{B}$ is complete.

It remains to show that $\mathcal{B}$ is complete if and only if it is full. First observe that, if $\mathcal{B}$ is full, then it is complete: indeed, $\mathcal{B}$ being full entails that, for all $E\nsim F$ in $\textsc{Pairs}_{i}$, $(E,F)$ is in $\mathcal{B}\subseteq{\nsim}$, hence $\textsc{Pairs}_{i}\setminus\mathcal{B}\subseteq{\sim}\subseteq{\dot{\sim}_{\mathcal{E}_{\mathcal{B}}}}$.

Conversely, assume that $\mathcal{B}$ is complete, and let us show that it is full; it suffices to show that, in that case, ${\dot{\sim}_{\mathcal{E}_{\mathcal{B}}}}\subseteq{\sim}$. By contradiction, consider a pair $E\nsim F$ with $E\mathrel{\dot{\sim}_{\mathcal{E}_{\mathcal{B}}}}F$; without loss of generality, $\textsc{el}(E,F)$ can be assumed minimal among all such pairs. Then $\mathcal{B}$ is full below $\textsc{el}(E,F)$: indeed, if $(E^{\prime},F^{\prime})\in\textsc{Pairs}_{i}$ and $\textsc{el}(E^{\prime},F^{\prime})<\textsc{el}(E,F)$, since $\textsc{el}(E,F)$ was taken minimal, $E^{\prime}\mathrel{\dot{\nsim}_{\mathcal{E}_{\mathcal{B}}}}F^{\prime}$ and therefore $(E^{\prime},F^{\prime})$ belongs to $\mathcal{B}$ since $\mathcal{B}$ is complete. Thus Lem. 4 applies and shows that $E\mathrel{\dot{\nsim}_{\mathcal{E}_{\mathcal{B}}}}F$, a contradiction. ∎

5. Complexity Upper Bounds

In this section, we analyse the procedure $\textsc{CandidateBound}_{n}$ to derive an upper bound on the computed $\mathcal{E}_{\mathcal{B}}$. In turn, by facts 1 and 3, this bound will allow us to bound the complexity of the bisimulation problem. The idea is to analyse the ranking function defined by (12) in order to bound how many times the main loop of $\textsc{CandidateBound}_{n}$ can be executed. We rely for this on a so-called ‘length function theorem’ from [28] to bound the length of descending sequences of ordinals like (13). Finally, we classify the final upper bound using the ‘fast-growing’ complexity classes defined in [29]. A general introduction to these techniques can be found in [30]. Throughout this section, we assume that the values of $g$, $n$, $s$, and $c$ are the ones needed for Thm. 3 to hold.

5.1. Controlled Descending Sequences

Though all descending sequences of ordinals are finite, we cannot bound their lengths in general; e.g., $K+1>K>K-1>\cdots>0$ and $\omega>K>K-1>\cdots>0$ are descending sequences of length $K+2$ for all $K$ in $\mathbb{N}$. Nevertheless, the sequence (13) produced by $\textsc{CandidateBound}_{n}$ is not arbitrary, because the successive ranks are either determined by the input and the initialisation phase, or the result of some computation, hence one cannot use an arbitrary $K$ as in these examples.

This intuition is captured by the notion of controlled sequences. For an ordinal $\alpha<\omega^{\omega}$ (like the ranks defined by (12)), let us write $\alpha$ in Cantor normal form as

[TABLE]

with $c_{0},\dots,c_{n}$ and $n$ in $\mathbb{N}$, and define its size as

[TABLE]

Let $N_{0}$ be a natural number in $\mathbb{N}$ and $h{:}\,\mathbb{N}\to\mathbb{N}$ a monotone inflationary function, i.e., $x\leq y$ implies $h(x)\leq h(y)$, and $x\leq h(x)$. A sequence $\alpha_{0},\alpha_{1},\dots$ of ordinals below $\omega^{\omega}$ is $(N_{0},h)$-controlled if, for all $\ell$ in $\mathbb{N}$,

[TABLE]

i.e., the size of the $\ell$th ordinal $\alpha_{\ell}$ is bounded by the $\ell$th iterate of $h$ applied to $N_{0}$; in particular, $\|\alpha_{0}\|\leq N_{0}$. Because for each $N\in\mathbb{N}$, there are only finitely many ordinals below $\omega^{\omega}$ of size at most $N$, the length of controlled descending sequences is bounded [see, e.g., 28]. One can actually give a precise bound on this length in terms of subrecursive functions, whose definition we are about to recall.

5.2. Subrecursive Functions

Algorithms shown to terminate via an ordinal ranking function can have a very high worst-case complexity. In order to express such large bounds, a convenient tool is found in subrecursive hierarchies, which employ recursion over ordinal indices to define faster and faster growing functions. We define here two such hierarchies.

Fundamental Sequences

A fundamental sequence for a limit ordinal $\lambda$ is a strictly ascending sequence $(\lambda(x))_{x<\omega}$ of ordinals $\lambda(x)<\lambda$ with supremum $\lambda$. We use the standard assignment of fundamental sequences to limit ordinals $\lambda\leq\omega^{\omega}$, defined inductively by

[TABLE]

where $\beta+\omega^{k+1}$ is in Cantor normal form. This particular assignment satisfies, e.g., $0<\lambda(x)<\lambda(y)$ for all $x<y$. For instance, $\omega(x)=x+1$ and $(\omega^{3}+\omega^{3}+\omega)(x)=\omega^{3}+\omega^{3}+x+1$.

Hardy and Cichoń Hierarchies

In the context of controlled sequences, the hierarchies of Hardy and Cichoń turn out to be especially well-suited [8]. Let $h{:}\,\mathbb{N}\to\mathbb{N}$ be a function. For each such $h$, the Hardy hierarchy $(h^{\alpha})_{\alpha\leq\omega^{\omega}}$ and the Cichoń hierarchy $(h_{\alpha})_{\alpha\leq\omega^{\omega}}$ relative to $h$ are two families of functions $h^{\alpha},h_{\alpha}{:}\,\mathbb{N}\to\mathbb{N}$ defined by induction over $\alpha$ by

[TABLE]

The Hardy functions are well-suited for expressing a large number of iterations of the provided function $h$. For instance, $h^{k}$ for some finite $k$ is simply the $k$th iterate of $h$. This intuition carries over: $h^{\alpha}$ is a ‘transfinite’ iteration of the function $h$, using a kind of diagonalisation in the fundamental sequences to handle limit ordinals. For instance, if we use the successor function $H(x)=x+1$ as our function $h$, we see that a first diagonalisation yields $H^{\omega}(x)=H^{x+1}(x)=2x+1$. The next diagonalisation occurs at $H^{\omega\cdot 2}(x)=H^{\omega+x+1}(x)=H^{\omega}(2x+1)=4x+3$. Fast-forwarding a bit, we get for instance a function of exponential growth $H^{\omega^{2}}(x)=2^{x+1}(x+1)-1$, and later a non-elementary function $H^{\omega^{3}}$ akin to a tower of exponentials, and a non primitive-recursive function $H^{\omega^{\omega}}$ of Ackermannian growth.

In the following, we will use the following property of Hardy functions [38, 8], which can be checked by induction provided $\alpha+\beta$ is in Cantor normal form (and justifies the use of superscripts):

[TABLE]

Regarding the Cichoń functions, an easy induction on $\alpha$ shows that $H^{\alpha}(x)=H_{\alpha}(x)+x$ for the hierarchy relative to H(x)\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}x+1. But the main interest of Cichoń functions is that they capture how many iterations are performed by Hardy functions [8]:

[TABLE]

Length Function Theorem

We can now state a ‘length function theorem’ for controlled descending sequences of ordinals.

Theorem 6** ([28, Thm. 3.3]).**

Let $N_{0}\geq n+1$. The maximal length of $(N_{0},h)$-controlled descending sequences of ordinals in $\omega^{n+1}$ is $h_{\omega^{n+1}}(N_{0})$.

5.3. Controlling the Candidate Computation

General Approach

Consider an execution of $\textsc{CandidateBound}_{n}$ entering the main loop at line 11 and let us define

[TABLE]

Controlling one Loop Execution

As a preliminary, let us observe that, for all $0\leq i\leq n$, the number of elements of $\textsc{Pairs}_{i}$ (defined in (11)) can be bounded by

[TABLE]

Indeed, the graph representation of some pair $(E,F)$ in $\textsc{Pairs}_{i}$ has at most $s_{i}$ vertices, each labelled by a nonterminal symbol from $\mathcal{N}$ or a variable from $\{x_{1},\dots,x_{i}\}$ and with at most $m$ outgoing edges; finally the two roots must be distinguished.

Let us turn our attention to the contents of the main loop.

Lemma 7**.**

For all $\ell$ in $\mathbb{N}$ we have $N_{\ell+1}\leq G_{\mathcal{G}}(N_{\ell})$ where

[TABLE]

Proof.

Assume we enter the main loop for the $\ell$th time with $N_{\ell}$ as defined in (19). On line 12, a new equivalence level $e$ is introduced, with $e\leq 2cN_{\ell}^{2}$ since $\mathcal{E}_{\mathcal{B}}\leq N_{\ell}$ and $\textsc{size}(E,F)\leq N_{\ell}$, thus in case of an update on line 16, we have $e_{i}\leq 2cN_{\ell}^{2}$. Consider now the for loop on lines 17–20. Regarding line 19, observe that $\max_{(E,F)\in\mathcal{B}}\textsc{el}(E,F)\leq\max\{e,\mathcal{E}_{\mathcal{B}}\}\leq 2cN_{\ell}^{2}$, thus

[TABLE]

Finally, regarding line 21, by (24), $\mathcal{E}_{\mathcal{B}}\leq 2(n+1)cN_{\ell}^{2}$. ∎

Final Bound

Let us finally express (22) in terms of $n$ and $|\mathcal{G}|$. First observe that, at the end of the initialisation phase of lines 2–8, $e_{i}=0$, $s_{i}\leq 2^{n+1}g$, $|\mathcal{P}_{i}|\leq 2^{2^{2n+5}s^{2}g^{2}\log|\mathcal{G}|}$, and $\mathcal{E}_{\mathcal{B}}=n+1$, thus

[TABLE]

Then, because the bounds in lemmata 7 and 27 are in terms of $|\mathcal{G}|$ (recall that the grammatical constant $g$ is exponential and $n$, $s$, and $c$ are doubly exponential in terms of $|\mathcal{G}|$), there exists a constant $d$ independent from $\mathcal{G}$ such that $|\mathcal{G}|\leq N_{0}\leq H^{\omega^{2}\cdot d}(|\mathcal{G}|)$ and $G_{\mathcal{G}}(x)\leq H^{\omega^{2}\cdot d}(\max\{x,|\mathcal{G}|\})$ for all $\mathcal{G}$ and $x$, where according to (16) $H^{\omega^{2}\cdot d}$ is the $d$th iterate of $H^{\omega^{2}}(x)=2^{x+1}(x+1)-1$. Then by (17), h(x)\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}H^{\omega^{2}\cdot d}(x) is a suitable control function that satisfies (20) and therefore (22).

Finally, because $n\leq N_{0}\leq h(|\mathcal{G}|)$ and by (17), $h^{\omega^{n+1}}(N_{0})\leq h^{\omega^{\omega}}(h(|\mathcal{G}|))$. We have just shown the following upper bound.

Lemma 8**.**

Let $\mathcal{G}$ be a first-order grammar and $n$, $s$, and $g$ be defined as in Thm. 3. Then $\mathcal{E}_{\mathcal{B}_{n,s,g}}\leq h^{\omega^{\omega}}(h(|\mathcal{G}|))$ where h(x)\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}H^{\omega^{2}\cdot d}(x) for some constant $d$.

5.4. Fast-Growing Complexity

It remains to combine Fact 1 with Lem. 8 in order to provide an upper bound for the bisimilarity problem. We will employ for this the fast-growing complexity classes defined in [29]. This is an ordinal-indexed hierarchy of complexity classes $(\ComplexityFont{F}_{\!\alpha})_{\alpha<\varepsilon_{0}}$, that uses the Hardy functions $(H^{\alpha})_{\alpha}$ relative to H(x)\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}x+1 as a standard against which we can measure high complexities.

Fast-Growing Complexity Classes

Let us first define

[TABLE]

denote the class of decision problems solved by deterministic Turing machines in time O\big{(}H^{\omega^{\alpha}}\!(p(n))\big{)} for some function $p\in\mathscr{F}_{\!<\alpha}$. The intuition behind this quantification over $p$ is that, just like e.g. \ComplexityFont{EXPTIME}=\bigcup_{p\in\poly}\ComplexityFont{DTIME}\big{(}2^{p(n)}\big{)} quantifies over polynomial functions to provide enough ‘wiggle room’ to account for polynomial reductions, $\ComplexityFont{F}_{\!\alpha}$ is closed under $\mathscr{F}_{\!<\alpha}$ reductions [29, Thms. 4.7 and 4.8].

For instance, \ComplexityFont{TOWER}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\ComplexityFont{F}_{\!3} defines the class of problems that can be solved using computational resources bounded by a tower of exponentials of elementary height in the size of the input, $\bigcup_{k\in\mathbb{N}}\ComplexityFont{F}_{\!k}$ is the class of primitive-recursive decision problems, and \ComplexityFont{ACKERMANN}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}\ComplexityFont{F}_{\!\omega} is the class of problems that can be solved using computational resources bounded by the Ackermann function applied to some primitive-recursive function of the input size—here it does not matter for $\alpha>2$ whether we are considering deterministic, nondeterministic, alternating, time, or space bounds [29, Sec. 4.2.1]. See Fig. 2 for a depiction.

Theorem 9**.**

The bisimulation problem for first-order grammars is in \ComplexityFontACKERMANN, and in $\ComplexityFont{F}_{\!n+4}$ if $n$ is fixed.

Proof.

This is a consequence of Fact 1 combined with theorems 3 and 8; the various overheads on top of the bound on $\mathcal{E}_{\mathcal{B}_{n,s,g}}$ are of course negligible for such high complexities [29, Lem. 4.6]. We rely here on [29, Thm. 4.2] to translate from $h^{\omega^{n+1}}$ with $h=H^{\omega^{2}\cdot d}\in\mathscr{F}_{\!<3}$ into a bound in terms of $H^{\omega^{n+4}}$. ∎

6. Pushdown Processes

The complexity upper bounds obtained in Sec. 5 are stated in terms of first-order grammars. In this section, we revisit the known reduction from pushdown systems to first-order grammars (as given in [15, 19]), and we also give a direct reduction from first-order grammars to pushdown systems (instead of giving just a general reference to [9, 7]). We do this first to make clear that the reductions are primitive recursive (in fact, they are polynomial-time reductions), and second to show that, in the real-time case, Thm. 9 provides primitive-recursive bounds for pushdown systems with a fixed number of states.

Pushdown Systems

Let us first recall that a pushdown system (PDS) is a tuple $M=(Q,\Sigma,\Gamma,\Delta)$ of finite sets where the elements of $Q,\Sigma,\Gamma$ are called control states, actions (or terminal letters), and stack symbols, respectively; $\Delta$ contains transition rules of the form $pY\xrightarrow{a}q\gamma$ where $p,q\in Q$, $Y\in\Gamma$, $a\in\Sigma\uplus\{\varepsilon\}$, and $\gamma\in\Gamma^{\ast}$. A pushdown system is called real-time if $a$ is restricted to be in $\Sigma$, i.e., if no $\varepsilon$ transition rules appear in $\Delta$.

A PDS $M=(Q,\Sigma,\Gamma,\Delta)$ generates the labelled transition system

[TABLE]

where each rule $pY\xrightarrow{a}q\gamma$ induces transitions $pY\gamma^{\prime}\xrightarrow{a}q\gamma\gamma^{\prime}$ for all $\gamma^{\prime}\in\Gamma^{\ast}$. Note that $\mathcal{L}_{M}$ might feature $\varepsilon$-transitions (also called $\varepsilon$-steps) $pY\gamma^{\prime}\xrightarrow{\varepsilon}q\gamma\gamma^{\prime}$ if the PDS is not real-time.

6.1. From PDS to First-Order Grammars

We recall a construction already presented in the appendix of the extended version of [19]. The idea is that, although first-order grammars lack the notion of control state, the behaviour of a pushdown system can nevertheless be captured by a first-order grammar that uses $m$-ary terms where $m$ is the number of control states.

Figure 3 (left) presents a configuration of a PDS—i.e., a state in $\mathcal{L}_{M}$—as a term; here we assume that $Q=\{q_{1},q_{2},q_{3}\}$. The string $pACB$, depicted on the left in a convenient vertical form, is translated into a term presented by an acyclic graph in the figure. On the right in Fig. 3 we can see the translation of the PDS transition rule $pA\xrightarrow{a}qCA$ into a rule of a first-order grammar.

6.1.1. Real-Time Case

Let us first assume that $M$ is a real-time PDS, i.e., that each PDS transition rule $pY\xrightarrow{a}q\gamma$ is such that $a$ is in $\Sigma$. We are interested in the following decision problem.

Problem** (Strong Bisimulation).**

[]

**input: **

A real-time pushdown system $M=(Q,\Sigma,\Gamma,\Delta)$ and two configurations $pY,qZ$ in $Q\times\Gamma$.

**question: **

Is $pY\sim qZ$ in the labelled transition system $\mathcal{L}_{M}$?

Formally, for a real-time PDS $M=(Q,\Sigma,\Gamma,\Delta)$, where $Q=\{q_{1},q_{2},\dots,q_{m}\}$, we can define the first-order grammar

[TABLE]

where \mathcal{N}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}Q\cup(Q\times\Gamma), with r(q)\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}0 and r((q,X))\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}m for all $q$ in $Q$ and $X$ in $\Gamma$; the set $\mathcal{R}$ is defined below. We write $[q]$ and $[qY]$ for nonterminals $q$ and $(q,Y)$, respectively, and we map each configuration $p\gamma$ to a (finite) term $\mathcal{T}(p\gamma)$ in $\textsc{Terms}_{\mathcal{N}}$ defined by structural induction:

[TABLE]

for all $i\in\{1,\dots,m\}$.

A PDS transition rule $pY\xrightarrow{a}q\gamma$ in $\Delta$ with $a$ in $\Sigma$ is then translated into the first-order grammar rule

[TABLE]

It should be obvious that the labelled transition system $\mathcal{L}_{M}$ is isomorphic with the restriction of the labelled transition system $\mathcal{L}_{\mathcal{G}_{M}}$ to the states $\mathcal{T}(p\gamma)$ where $p\gamma$ are configurations of $M$; moreover, the set $\{\mathcal{T}(p\gamma)\mid p\in Q,\gamma\in\Gamma^{\ast}\}$ is closed w.r.t. reachability in $\mathcal{L}_{\mathcal{G}_{M}}$: if $\mathcal{T}(p\gamma)\xrightarrow{a}F$ in $\mathcal{L}_{\mathcal{G}_{M}}$, then $F=\mathcal{T}(q\gamma^{\prime})$ where $p\gamma\xrightarrow{a}q\gamma^{\prime}$ in $\mathcal{L}_{M}$.

Corollary 10**.**

The strong bisimulation problem for real-time pushdown systems is in \ComplexityFontACKERMANN, and in $\ComplexityFont{F}_{\!|Q|+4}$ if the number $|Q|$ of states is fixed.

Proof.

What we have sketched above is a polynomial-time (in fact, \ComplexityFontlogspace) reduction from the strong bisimulation problem in (real-time) pushdown systems to the bisimulation problem in first-order grammars, for which we can apply Thm. 9. Observe that, in this translation and according to the discussion after (6), we may bound $n$ by the number $|Q|$ of states of the given pushdown system, which justifies the primitive-recursive $\ComplexityFont{F}_{\!|Q|+4}$ upper bound when the number of states is fixed. (Figure 3 makes clear that all branches in $\mathcal{T}(p\gamma)$ have the same lengths, and there are precisely $|Q|$ depth-$d$ subterms of $\mathcal{T}(p\gamma)$, for each $d\leq 0pt{\mathcal{T}(p\gamma)}$.) ∎

6.1.2. General Case

In the case of labelled transition systems $\mathcal{L}=(\mathcal{S},\Sigma,({\xrightarrow{a}})_{a\in\Sigma\uplus\{\varepsilon\}})$ with a silent action $\varepsilon$, by $s\xRightarrow{w}t$, for $w\in\Sigma^{\ast}$, we denote that there are $s_{0},s_{1},\dots,s_{\ell}\in\mathcal{S}$ and $a_{1},\dots,a_{\ell}\in\Sigma\uplus\{\varepsilon\}$ such that $s_{0}=s$, $s_{\ell}=t$, $s_{i-1}\xrightarrow{a_{i}}s_{i}$ for all $i\in\{1,\dots,\ell\}$, and $w=a_{1}\cdots a_{\ell}$. Thus $s\xRightarrow{\varepsilon}t$ denotes an arbitrary sequence of silent steps, and $s\xRightarrow{a}t$ for $a\in\Sigma$ denotes that there are $s^{\prime},t^{\prime}$ such that $s\xRightarrow{\varepsilon}s^{\prime}\xrightarrow{a}t^{\prime}\xRightarrow{\varepsilon}t$.

A relation $R\subseteq\mathcal{S}\times\mathcal{S}$ is a weak bisimulation if the following two conditions hold:

[]

**(zig): **

if $s\mathbin{R}t$ and $s\xrightarrow{a}s^{\prime}$ for some $a\in\Sigma\uplus\{\varepsilon\}$, then there exists $t^{\prime}$ such that $t\xRightarrow{a}t^{\prime}$ and $s^{\prime}\mathbin{R}t^{\prime}$;

**(zag): **

if $s\mathbin{R}t$ and $t\xrightarrow{a}t^{\prime}$ for some $a\in\Sigma\uplus\{\varepsilon\}$, then there exists $s^{\prime}$ such that $s\xRightarrow{a}s^{\prime}$ and $s^{\prime}\mathbin{R}t^{\prime}$.

By $\approx$ we denote weak bisimilarity, i.e., the largest weak bisimulation (the union of all weak bisimulations), which is an equivalence relation.

We are now interested in the following problem.

Problem** (Weak Bisimulation).**

[]

**input: **

A pushdown system $M=(Q,\Sigma,\Gamma,\Delta)$ and two configurations $pY,qZ$ in $Q\times\Gamma^{\ast}$.

**question: **

Is $pY\approx qZ$ in the labelled transition system $\mathcal{L}_{M}$?

Unfortunately, in general the weak bisimulation problem for PDS is undecidable, already for one-counter systems [24]; we can also refer, e.g., to [21] for further discussion. As already mentioned in the introduction, we thus consider PDS with (very) restricted silent actions: each rule $pY\xrightarrow{\varepsilon}q\gamma$ in $\Delta$ is deterministic (i.e., alternative-free), which means that there is no other rule with the left-hand side $pY$. From now on, by restricted PDS we mean PDS whose $\varepsilon$-rules are deterministic.

We aim to show that the weak bisimulation problem for restricted PDS reduces to the (strong) bisimulation problem for first-order grammars (where silent actions are not allowed by our definition). For this it is convenient to make a standard transformation [see, e.g., 12, Sec. 5.6] of our restricted PDS that removes non-popping $\varepsilon$-rules; an $\varepsilon$-rule $pY\xrightarrow{\varepsilon}q\gamma$ is called popping if $\gamma=\varepsilon$. This is captured by the next proposition. (When comparing two states from different LTSs, we implicitly refer to the disjoint union of these LTSs.)

Proposition 11**.**

There is a polynomial-time transformation of a restricted PDS $M=(Q,\Sigma,\Gamma,\Delta)$ to $M^{\prime}=(Q,\Sigma,\Gamma,\Delta^{\prime})$ in which each $\varepsilon$-rule is deterministic and popping, and $pY$ in $\mathcal{L}_{M}$ is weakly bisimilar with $pY$ in $\mathcal{L}_{M^{\prime}}$.

Proof.

Given a restricted PDS $M=(Q,\Sigma,\Gamma,\Delta)$, we proceed as follows. First we find all $pY$ such that

[TABLE]

and each rule $qB\xrightarrow{a}q^{\prime}\gamma^{\prime}$ with $a\in\Sigma$ we add the rule $pY\xrightarrow{a}q^{\prime}\gamma^{\prime}\gamma$. Finally we remove all the non-popping $\varepsilon$-rules. Thus $M^{\prime}=(Q,\Sigma,\Gamma,\Delta^{\prime})$ arises. Identifying the configurations that satisfy conditions (34–36) can be performed in polynomial time through a saturation algorithm. The claim on the relation of $\mathcal{L}_{M}$ and $\mathcal{L}_{M^{\prime}}$ is straightforward. ∎

A stable configuration is either a configuration $p\varepsilon$, or a configuration $pY\gamma$ where there is no $\varepsilon$-rule of the form $pY\xrightarrow{\varepsilon}q\gamma^{\prime}$. In a restricted PDS with only popping $\varepsilon$-rules, any unstable configuration $p\gamma$ only allows to perform a finite sequence of silent popping steps until it reaches a stable configuration. It is natural to restrict our attention to the transitions $p\gamma\xrightarrow{a}q\gamma^{\prime}$ with $a\in\Sigma$ between stable configurations; such transitions might encompass sequences of popping $\varepsilon$-steps.

When defining the grammar $\mathcal{G}_{M}$, we can avoid the explicit use of deterministic popping silent steps, by ‘preprocessing’ them: we apply the inductive definition of the translation operator $\mathcal{T}$ from (30–32) to stable configurations, while if $pY$ is unstable, then there is exactly one applicable rule, $pY\xrightarrow{\varepsilon}q$, and in this case we let

[TABLE]

Figure 4 (right) shows the grammar-rule

[TABLE]

(arising from the PDS-rule $pA\xrightarrow{a}qCA$), when $Q=\{q_{1},q_{2},q_{3}\}$ and there is a PDS-rule $q_{2}A\xrightarrow{\varepsilon}q_{3}$, while $q_{1}A$, $q_{3}A$ are stable.

Corollary 12**.**

The weak bisimulation problem for restricted pushdown systems (i.e., where $\varepsilon$-rules are deterministic) is in $\ComplexityFont{ACKERMANN}$.

Proof.

By Proposition 11 it suffices to consider a PDS $M=(Q,\Sigma,\Gamma,\Delta)$ where each $\varepsilon$-rule is deterministic and popping. Since it is clear that $pY\approx qZ$ in $\mathcal{L}_{M}$ iff $\mathcal{T}(pY)\sim\mathcal{T}(qZ)$ in $\mathcal{L}_{\mathcal{G}_{M}}$, the claim follows from Thm. 9. ∎

Note that, due to our preprocessing, the terms $\mathcal{T}(p\gamma)$ may have branches of varying lengths, which is why $n$ as defined in (6) might not be bounded by the number of states as in Cor. 10.

6.2. From First-Order Grammars to PDS

We have shown the $\ComplexityFont{ACKERMANN}$-membership for bisimilarity of first-order grammars (Thm. 9), and thus also for weak bisimilarity of pushdown processes with deterministic $\varepsilon$-steps (Cor. 12). By adding the lower bound from [18], we get the $\ComplexityFont{ACKERMANN}$-completeness for both problems.

In fact, the $\ComplexityFont{ACKERMANN}$-hardness in [18] was shown in the framework of first-order grammars. The case of pushdown processes was handled by a general reference to the equivalences that are known, e.g., from [9] and the works referred there; another relevant reference for such equivalences is [7]. Nevertheless, in our context it seems more appropriate to show a direct transformation from first-order grammars to pushdown processes (with deterministic $\varepsilon$-steps), which can be argued to be primitive-recursive; in fact, it is a \ComplexityFontlogspace reduction.

Let $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$ be a first-order grammar. For a term $F\in\textsc{Terms}_{\mathcal{N}}$ such that $F\not\in\textsc{Var}$ (hence the root of $F$ is a nonterminal $A$) we define its root-substitution to be the substitution $\sigma$ where $F=A(x_{1},\dots,x_{r(A)})\sigma$ and $x\sigma=x$ for all $x\not\in\{x_{1},\dots,x_{r(A)}\}$. A substitution $\sigma$ is an rhs-substitution for $\mathcal{G}$ if it is the root-substitution of a subterm $F$ of the right-hand side $E$ of a rule $A(x_{1},\dots,x_{r(A)})\xrightarrow{a}E$ in $\mathcal{R}$ (where $F\not\in\textsc{Var}$); we let $\textsc{RSubs}_{\mathcal{G}}$ denote the set of rhs-substitutions for $\mathcal{G}$.

We define the PDS M_{\mathcal{G}}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.5}{{def}}}}}{{=}}}}(Q,\Sigma,\Gamma,\Delta) where

[TABLE]

See Fig. 5 for an example. Note that the $\varepsilon$-rules are indeed deterministic; moreover, any non-popping $\varepsilon$-step, hence of the form $q_{i}\sigma\gamma\xrightarrow{\varepsilon}q_{1}C\sigma^{\prime}\gamma$, cannot be followed by another $\varepsilon$-step.

It should be obvious that a state $A(x_{1},\dots,x_{r(A)})$ in $\mathcal{L}_{\mathcal{G}}$ is weakly bisimilar with the state $q_{1}A$ in $\mathcal{L}_{M_{\mathcal{G}}}$. In particular we note that $q_{1}A\xRightarrow{w}q_{i}\gamma$ in $\mathcal{L}_{M_{\mathcal{G}}}$ (where also $\varepsilon$-steps might be comprised) entails that $\gamma=\sigma_{0}\sigma_{1}\dots\sigma_{\ell}$ (in which case $q_{i}\gamma$ represents the term $x_{i}\sigma_{0}\sigma_{1},\dots\sigma_{\ell}$), or $\gamma=B\sigma_{1}\dots\sigma_{\ell}$ when $i=1$ (in which case $q_{1}\gamma$ represents the term $B(x_{1},\dots,x_{r(B)})\sigma_{1},\dots\sigma_{\ell}$).

We could add a technical discussion about how to represent all the terms from $\textsc{Terms}_{\mathcal{N}}$ (including the infinite regular terms) in an enhanced version of $\mathcal{L}_{M_{\mathcal{G}}}$, but this is not necessary since the lower bound construction in [18] uses only the states of $\mathcal{L}_{\mathcal{G}}$ that are reachable from ‘initial’ terms of the form $A(x_{1},\dots,x_{r(A)})$ (more precisely, of the form $A(\bot,\dots,\bot)$ for a nullary nonterminal $\bot$).

Corollary 13**.**

The weak bisimulation problem for pushdown systems whose $\varepsilon$-rules are deterministic and popping is $\ComplexityFont{ACKERMANN}$-hard.

Proof.

In [18], the \ComplexityFontACKERMANN-hardness of the control-state reachability problem for reset counter machines is recalled [27], and its polynomial-time (in fact, \ComplexityFontlogspace) reduction to the bisimulation problem for first-order grammars is shown. The reduction guarantees that a given control state is reachable from the initial configuration of a given reset counter machine $R$ iff $A(\bot,\dots,\bot)\not\sim B(\bot,\dots,\bot)$ in $\mathcal{L}_{\mathcal{G}_{R}}$ for the constructed grammar $\mathcal{G}_{R}$. As shown above, the question whether $A(\bot,\dots,\bot)\sim B(\bot,\dots,\bot)$ in $\mathcal{L}_{\mathcal{G}_{R}}$ can be further reduced to an instance of the weak bisimulation problem for the pushdown system $M_{\mathcal{G}_{R}}$. ∎

7. Concluding Remarks

Theorems 9 and 12 provide the first known worst-case upper bounds, in \ComplexityFontACKERMANN, for the strong bisimulation equivalence of first-order grammars and the weak bisimulation equivalence of pushdown processes restricted to deterministic silent steps. By the lower bound shown in [18] and Cor. 13, this is moreover optimal. An obvious remaining problem is to close the complexity gap in the case of strong bisimulation for real-time pushdown processes, which is only known to be \ComplexityFontTOWER-hard [1], and for which we do not expect Cor. 10 to provide tight upper bounds.

Appendix A Grammatical Constants

The proof of Thm. 3 in [20, Thm. 7] relies on the definition of several grammatical constants, which depend solely on the given first-order grammar $\mathcal{G}=(\mathcal{N},\Sigma,\mathcal{R})$. In Tab. 2 we summarise their definitions as a reference for the reader.

Acknowledgements

P. Jančar acknowledges the support of the Grant Agency of Czech Rep., GAČR 18-11193S; part of this research was conducted while he held an invited professorship at ENS Paris-Saclay. S. Schmitz is partially funded by ANR-17-CE40-0028 Bra​VAS.