摘要
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 F_(d+3),which improves the best known upper bound F_(d+4) of this problem.
基金
supported by the National Natural Foundation of China(Grant Nos.62072299,61872142,61772336,61572318)
the Open Project of Shanghai Key Laboratory of Trustworthy Computing(OP202102)。
