Weak Bisimulation Finiteness of Pushdown Systems With Deterministic ε-Transitions Is 2-EXPTIME-Complete

We consider the problem of deciding whether a given pushdown system all of whose ε-transitions are deterministic is weakly bisimulation finite, that is, whether it is weakly bisimulation equivalent to a finite system. We prove that this problem is 2-EXPTIME-complete. This consists of three elements: First, we prove that the smallest finite system that is weakly bisimulation equivalent to a fixed pushdown system, if exists, has size at most doubly exponential in the description size of the pushdown system. Second, we propose a fast algorithm deciding whether a given pushdown system is weakly bisimulation equivalent to a finite system of a given size. Third, we prove 2-EXPTIME-hardness of the problem. The problem was known to be decidable, but the previous algorithm had Ackermannian complexity (6-EXPSPACE in the easier case of pushdown systems without ε-transitions); concerning lower bounds, only EXPTIME-hardness was known.