  The "bisimulation problem" for equational graphs of finite out-degree is
shown to be decidable. We reduce this problem to the bisimulation problem for
deterministic rational (vectors of) boolean series on the alphabet of a dpda M.
We then exhibit a complete formal system for deducing equivalent pairs of such
vectors.
