下推系统的互模拟性是初等的
Bisimulation Finiteness of Pushdown Systems Is Elementary
摘要：
我们证明了，如果一个下推系统是互模拟等价于一个有限系统，已经有一个互模拟等价的有限系统，其大小是基本上有界的下推系统的描述大小。由此我们得到，如果一个给定的下推系统与某个有限系统互模拟等价，则它是初等可判定的。这提高了以前最有名的阿克曼上限为这个问题。
英文摘要：
We show that in case a pushdown system is bisimulation equivalent to a finite system, there is already a bisimulation equivalent finite system whose size is elementarily bounded in the description size of the pushdown system. As a consequence we obtain that it is elementarily decidable if a given pushdown system is bisimulation equivalent to some finite system. This improves a previously best-known ACKERMANN upper bound for this problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
