The parametric complexity of bisimulation equivalence of normed pushdown automata

Deciding bisimulation equivalence of two normed pushdown automata is one of the most fundamental problems in formal verification. The problem is proven to be ACKER-MANN-complete recently. Both the upper bound and the lower bound results indicate that the number of control states is an important parameter. In this paper, we study the parametric complexity of this problem. We refine previous results in two aspects. First, we prove that the bisimulation equivalence of normed PDA with two states is EXPTIME-hard. Second, we prove that the bisimulation equivalence of normed PDA with d states is in Fd+3, which improves the best known upper bound Fd+4 of this problem.