Technical Reports
The report FIMU-RS-2004-01
A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata
by
Antonín Kučera,
Richard Mayr,
A full version of the paper presented at IFIP TCS 2004. April 2004, 38 pages.
FIMU-RS-2004-01.
Available as Postscript,
PDF.
Abstract:
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.
