A generic framework for checking semantic equivalences between pushdown automata and finite-state automata

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

KUČERA Antonín MAYR Richard

Year of publication 2018
Type Article in Periodical
Magazine / Source Journal of Computer and System Sciences
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1016/j.jcss.2017.09.004
Doi http://dx.doi.org/10.1016/j.jcss.2017.09.004
Keywords pushdown automata; equivalence-checking
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.