SRBA, Jiří. Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation. LNCS, Annual Conference on Computer Science Logic (CSL'06), Netherlands: Springer-Verlag, 2006, roč. 2006, č. 4207, s. 89-103.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
Název česky Viditelne Zasobnikove Automaty: Od Jazykove Ekvivalence k Simulaci a Bisimulaci
Autoři SRBA, Jiří (203 Česko, garant).
Vydání LNCS, Annual Conference on Computer Science Logic (CSL'06), Netherlands, Springer-Verlag, 2006.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Nizozemsko
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/06:00015980
Organizační jednotka Fakulta informatiky
UT WoS 000241587300006
Klíčová slova anglicky visibly pushdown automata; bisimilarity; decidability
Štítky bisimilarity, decidability, visibly pushdown automata
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. JUDr. Vladimír Šmíd, CSc., učo 1084. Změněno: 6. 7. 2007 09:02.
Anotace
We investigate the possibility of (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses visibly BPA (Basic Process Algebra) and visibly one-counter automata. We describe generic methods for proving complexity upper and lower bounds for a number of studied preorders and equivalences like simulation, completed simulation, ready simulation, 2-nested simulation preorders/equivalences and bisimulation equivalence. Our main results are that all the mentioned equivalences and preorders are EXPTIME-complete on visibly pushdown automata, PSPACE-complete on visibly one-counter automata and P-complete on visibly BPA. Our PSPACE lower bound for visibly one-counter automata improves also the previously known DP-hardness results for ordinary one-counter automata and one-counter nets. Finally, we study regularity checking problems for visibly pushdown automata and show that they can be decided in polynomial time.
Anotace česky
We investigate the possibility of (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses visibly BPA (Basic Process Algebra) and visibly one-counter automata. We describe generic methods for proving complexity upper and lower bounds for a number of studied preorders and equivalences like simulation, completed simulation, ready simulation, 2-nested simulation preorders/equivalences and bisimulation equivalence. Our main results are that all the mentioned equivalences and preorders are EXPTIME-complete on visibly pushdown automata, PSPACE-complete on visibly one-counter automata and P-complete on visibly BPA. Our PSPACE lower bound for visibly one-counter automata improves also the previously known DP-hardness results for ordinary one-counter automata and one-counter nets. Finally, we study regularity checking problems for visibly pushdown automata and show that they can be decided in polynomial time.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Standardní projekty
MSM 143300001, záměrNázev: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 3. 7. 2020 23:19