Publication details

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

Investor logo

KUČERA Antonín MAYR Richard

Year of publication 2004
Type Article in Proceedings
Conference Exploring New Frontiers of Theoretical Informatics : IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004)
MU Faculty or unit

Faculty of Informatics

Field Informatics
Keywords Formal verification; Pushdown automata; Semantic equivalences
Description We propose a generic method for deciding semantic equivalences between pushdown automata and finite-state automata. The abstract part of the method is applicable to every process equivalence which is a right PDA congruence. Practical usability of the method is demonstrated on selected equivalences which are conceptual representatives of the whole spectrum. In particular, special attention is devoted to bisimulation-like equivalences (including weak, early, delay, branching, and probabilistic bisimilarity), and it is also shown how the method applies to simulation-like and trace-like equivalences. The generality does not lead to the loss of efficiency; the algorithms obtained by applying our method are essentially time-optimal and sometimes even polynomial. The list of particular results obtained by our method includes items which are first of their kind.
Related projects:

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

More info