The parametric complexity of bisimulation equivalence of normed pushdown automata  

作　　者：Wenbo Zhang 

机构地区：[1]College of Information Technology,Shanghai Ocean University,Shanghai,201306,China [2]BASICS Lab,School of Electronic Information and Electrical Engineering,Shanghai Jiao Tong University,Shanghai,200240,China

出　　处：《Frontiers of Computer Science》2022年第4期111-117,共7页中国计算机科学前沿（英文版）

基　　金：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)。

摘　　要：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.

关 键 词：PDA BISIMULATION equivalence checking 

分 类 号：TP39[自动化与计算机技术—计算机应用技术]