A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata

Antonin Kučera, Richard Mayr

Research output: Contribution to journalArticlepeer-review

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.
Original languageEnglish
Pages (from-to)82-103
Number of pages22
JournalJournal of Computer and System Sciences
Volume91
Early online date19 Sep 2017
DOIs
Publication statusPublished - Feb 2018

Keywords

  • Pushdown automata, semantic equivalences, bisimulation

Fingerprint

Dive into the research topics of 'A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata'. Together they form a unique fingerprint.

Cite this