Finiteness up to bisimilarity is decidable for pushdown processes
Petr Jančar · arXiv (Cornell University) · 2013
It is shown that it is decidable if a given configuration of a pushdown automaton (pda) with no epsilon-transitions is bisimulation equivalent with some unspecified finite-state process. While the semidecidability of the positive case has been long clear, it is the existence of a finite effectively verifiable witness of the negative case which is the crucial point here. The presented algorithm also uses a procedure for deciding bisimilarity between pda configurations, which is known due to Senizergues (1998, 2005). The complexity of the procedure is non-elementary, as shown by Benedikt, Goeller, Kiefer, and Murawski (2012), but the EXPTIME-hardness (Kucera and Mayr 2002, and Srba 2002) remains the only known complexity bound for the problem.