Weak Bisimulation Finiteness of Pushdown Systems With Deterministic ε-Transitions Is 2-EXPTIME-Complete
- Speaker(s)
- Paweł Parys
- Affiliation
- MIM UW
- Date
- Nov. 9, 2022, 2:15 p.m.
- Room
- room 5050
- Seminar
- Seminar Automata Theory
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.