Fast equivalence-checking for normed context-free processes

Abstract

Bisimulation equivalence is decidable in polynomial time over normed graphs generated by a context-free grammar. We present a new algorithm, working in time $O(n^5)$, thus improving the previously known complexity $O(n^8 * polylog(n))$. It also improves the previously known complexity $O(n^6 * polylog(n))$ of the equality problem for simple grammars.