The Bisimulation Problem for Equational Graphs of Finite Out-Degree
Géraud Sénizergues · SIAM Journal on Computing · 2005
The bisimulation problem for equational graphs of finite out-degree is shown to be decidable. We reduce this problem to the $\eta$-bisimulation problem for deterministic rational (vectors of) boolean series on the alphabet of a deterministic pushdown automaton ${\cal M}$. We then exhibit a complete formal system for deducing equivalent pairs of such vectors.