You are here:
Publication details
A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
Authors | |
---|---|
Year of publication | 2018 |
Type | Article in Periodical |
Magazine / Source | Journal of Computer and System Sciences |
MU Faculty or unit | |
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: |