# 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.

## Key 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.