A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
| Autor: | Richard Mayr, Antonín Kučera |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Bisimulation
Discrete mathematics Theoretical computer science Finite-state machine Logical equivalence Computer Networks and Communications Applied Mathematics Formal equivalence checking Pushdown automaton 0102 computer and information sciences 02 engineering and technology 16. Peace & justice 01 natural sciences Theoretical Computer Science Automaton Computational Theory and Mathematics 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Equivalence (measure theory) Formal verification Computer Science::Formal Languages and Automata Theory Pushdown automata semantic equivalences bisimulation Mathematics |
| Zdroj: | Kučera, A & Mayr, R 2018, ' A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata ', Journal of Computer and System Sciences, vol. 91, pp. 82-103 . https://doi.org/10.1016/j.jcss.2017.09.004 |
| ISSN: | 0022-0000 |
| DOI: | 10.1016/j.jcss.2017.09.004 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect