@inbook{doi:10.1137/1.9781611977554.ch105,
    Abstract = {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.},
    Author = {G{\"o}ller, Stefan and Parys, Pawel},
    BookTitle = {Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)},
    EPrint = {https://epubs.siam.org/doi/pdf/10.1137/1.9781611977554.ch105},
    File = {Weak Bisimulation Finiteness of Pushdown Systems With Deterministic ε-Transitions Is 2-ExpTime-Complete - 1.9781611977554.ch105 - a.pdf},
    Pages = {2777-2815},
    Title = {{Weak Bisimulation Finiteness of Pushdown Systems With Deterministic $\varepsilon$-Transitions Is 2-EXPTIME-Complete}},
    URL = {https://epubs.siam.org/doi/abs/10.1137/1.9781611977554.ch105},
    Year = {2023},
    bdsk-url-1 = {https://epubs.siam.org/doi/abs/10.1137/1.9781611977554.ch105},
    bdsk-url-2 = {https://doi.org/10.1137/1.9781611977554.ch105},
    date-added = {2023-03-11 23:09:43 +0100},
    date-modified = {2023-03-11 23:10:28 +0100},
    doi = {10.1137/1.9781611977554.ch105}
}

@inbook{doi:10.1137/1.9781611977554.ch105, Abstract = {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.}, Author = {G{\"o}ller, Stefan and Parys, Pawel}, BookTitle = {Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)}, EPrint = {https://epubs.siam.org/doi/pdf/10.1137/1.9781611977554.ch105}, File = {Weak Bisimulation Finiteness of Pushdown Systems With Deterministic ε-Transitions Is 2-ExpTime-Complete - 1.9781611977554.ch105 - a.pdf}, Pages = {2777-2815}, Title = {{Weak Bisimulation Finiteness of Pushdown Systems With Deterministic $\varepsilon$-Transitions Is 2-EXPTIME-Complete}}, URL = {https://epubs.siam.org/doi/abs/10.1137/1.9781611977554.ch105}, Year = {2023}, bdsk-url-1 = {https://epubs.siam.org/doi/abs/10.1137/1.9781611977554.ch105}, bdsk-url-2 = {https://doi.org/10.1137/1.9781611977554.ch105}, date-added = {2023-03-11 23:09:43 +0100}, date-modified = {2023-03-11 23:10:28 +0100}, doi = {10.1137/1.9781611977554.ch105} }