Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete
Autor: | Petr Jancar, Sylvain Schmitz |
---|---|
Přispěvatelé: | Department of Computer Science [Univ Palacký], Faculty of Science [Univ Palacký], Palacky University Olomouc-Palacky University Olomouc, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Institut Universitaire de France (IUF), Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (M.E.N.E.S.R.), ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017) |
Jazyk: | angličtina |
Rok vydání: | 2019 |
Předmět: |
FOS: Computer and information sciences
Discrete mathematics Computer Science - Logic in Computer Science Grammar Formal Languages and Automata Theory (cs.FL) Semantics (computer science) media_common.quotation_subject bisimilarity Pushdown automaton [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Computer Science - Formal Languages and Automata Theory 16. Peace & justice fast-growing complexity Upper and lower bounds Ackermann function Logic in Computer Science (cs.LO) Automaton Decidability Rule-based machine translation first-order grammar Computer Science::Logic in Computer Science Computer Science::Formal Languages and Automata Theory media_common Mathematics pushdown system |
Zdroj: | LICS 2019, 34th Annual ACM/IEEE Symposium on Logic in Computer Science LICS 2019, 34th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2019, Vancouver, Canada. pp.1--12, ⟨10.1109/LICS.2019.8785848⟩ LICS |
DOI: | 10.1109/LICS.2019.8785848⟩ |
Popis: | International audience; Checking whether two pushdown automata with restricted silent actions are weakly bisimilar was shown decidable by Sénizergues (1998, 2005). We provide the first known complexity upper bound for this famous problem, in the equivalent setting of first-order grammars. This ACKERMANN upper bound is optimal, and we also show that strong bisimilarity is primitive-recursive when the number of states of the automata is fixed. |
Databáze: | OpenAIRE |
Externí odkaz: |