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

Investor logo

Warning

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

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

Citation
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.