Bisimulation Equivalence of First-Order Grammars

TL;DR

This paper proves that bisimulation equivalence for first-order grammars is decidable, extending known results for automata and providing a more accessible proof framework, with discussions on branching bisimilarity.

Contribution

It introduces a decidability proof for bisimulation equivalence of first-order grammars, generalizing automata equivalence results and making the proof more understandable.

Findings

Decidability of bisimulation equivalence for first-order grammars established.

Extension to branching bisimilarity discussed.

Framework potentially applicable to broader classes of rewriting systems.

Abstract

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