A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata
| Authors | |
|---|---|
| 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 | |
| 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: |