# Equivalence of pushdown automata via first-order grammars

## TL;DR

This paper presents a simpler, explicit algorithm for deciding bisimulation equivalence of first-order grammars, which subsumes previous results for deterministic pushdown automata and may allow for complexity analysis.

## Contribution

It offers a new, more straightforward proof of decidability for bisimulation equivalence, providing an explicit algorithm rather than semidecision procedures.

## Key findings

- Decidability of bisimulation equivalence for first-order grammars established
- Provides an explicit algorithm potentially suitable for complexity analysis
- Simplifies previous proofs by Sénizergues for deterministic pushdown automata

## Abstract

A decidability proof for bisimulation equivalence of first-order grammars is given. It is an alternative proof for a result by S\'enizergues (1998, 2005) that subsumes his affirmative solution of the famous decidability question for deterministic pushdown automata. The presented proof is conceptually simpler, and a particular novelty is that it is not given as two semidecision procedures but it provides an explicit algorithm that might be amenable to a complexity analysis.