Complexity of deciding bisimilarity between normed BPA and normed BPP

We present a polynomial-time algorithm deciding bisimilarity between a normed BPA process and a normed BPP process, with running time O(n7). This improves the previously known exponential upper bound. We first suggest an O(n3) transformation of the BPP process into “prime form”. Our algorithm then relies on a polynomial bound for a “finite-state core” of the transition system generated by the (transformed) BPP process.