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. The talk is based on a paper accepted to SODA 2023, co-authored by Stefan Göller. It is a continuation of our previous paper (LICS 2020, presented on the seminar in January 2020), where we showed an 6-EXPSPACE algorithm solving the problem in the easier case of pushdown systems without ε-transitions.