The Bisimulation Problem for equational graphs of finite out-degree
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.
cs.LO↗