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: |