Weak Bisimulation Finiteness of Pushdown Systems With Deterministic $\varepsilon$-Transitions Is 2-ExpTime-Complete

We consider the problem of deciding whether a given pushdown system all of whose $\varepsilon$-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 $\varepsilon$-transitions); concerning lower bounds, only ExpTime-hardness was known.