@article{KUCERA201882,
    Abstract = {For a given process equivalence, we say that a process g is fully equivalent to a process f of a transition system T if g is equivalent to f and every reachable state of g is equivalent to some state of T. We propose a generic method for deciding full equivalence between pushdown processes and finite-state processes applicable to every process equivalence satisfying certain abstract conditions. Then, we show that these conditions are satisfied by bisimulation-like equivalences (including weak and branching bisimilarity), weak simulation equivalence, and weak trace equivalence, which are the main conceptual representatives of the linear/branching time spectrum. The list of particular results obtained by applying our method includes items which are first of their kind, and the associated upper complexity bounds are essentially optimal.},
    Author = {Ku{\v c}era, Anton{\'\i}n and Mayr, Richard},
    File = {1-s2.0-S0022000017301368-main (0) - a - a - t.pdf},
    ISSN = {0022-0000},
    Journal = {Journal of Computer and System Sciences},
    Keywords = {Pushdown automata, Semantic equivalences, Bisimulation},
    Pages = {82 - 103},
    Title = {A generic framework for checking semantic equivalences between pushdown automata and finite-state automata},
    URL = {http://www.sciencedirect.com/science/article/pii/S0022000017301368},
    Volume = {91},
    Year = {2018},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0022000017301368},
    bdsk-url-2 = {https://doi.org/10.1016/j.jcss.2017.09.004},
    bdsk-url-3 = {http://drops.dagstuhl.de/opus/volltexte/2018/9943},
    date-added = {2019-01-21 15:22:45 +0100},
    date-modified = {2019-01-21 15:22:45 +0100},
    doi = {10.1016/j.jcss.2017.09.004}
}

@article{KUCERA201882, Abstract = {For a given process equivalence, we say that a process g is fully equivalent to a process f of a transition system T if g is equivalent to f and every reachable state of g is equivalent to some state of T. We propose a generic method for deciding full equivalence between pushdown processes and finite-state processes applicable to every process equivalence satisfying certain abstract conditions. Then, we show that these conditions are satisfied by bisimulation-like equivalences (including weak and branching bisimilarity), weak simulation equivalence, and weak trace equivalence, which are the main conceptual representatives of the linear/branching time spectrum. The list of particular results obtained by applying our method includes items which are first of their kind, and the associated upper complexity bounds are essentially optimal.}, Author = {Ku{\v c}era, Anton{\'\i}n and Mayr, Richard}, File = {1-s2.0-S0022000017301368-main (0) - a - a - t.pdf}, ISSN = {0022-0000}, Journal = {Journal of Computer and System Sciences}, Keywords = {Pushdown automata, Semantic equivalences, Bisimulation}, Pages = {82 - 103}, Title = {A generic framework for checking semantic equivalences between pushdown automata and finite-state automata}, URL = {http://www.sciencedirect.com/science/article/pii/S0022000017301368}, Volume = {91}, Year = {2018}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0022000017301368}, bdsk-url-2 = {https://doi.org/10.1016/j.jcss.2017.09.004}, bdsk-url-3 = {http://drops.dagstuhl.de/opus/volltexte/2018/9943}, date-added = {2019-01-21 15:22:45 +0100}, date-modified = {2019-01-21 15:22:45 +0100}, doi = {10.1016/j.jcss.2017.09.004} }