Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation

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.

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 Česká republika, 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: Nizozemské království
• 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

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 VaV: Název: Verifikace nekonečně stavových systémů

Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů

• MSM 143300001, záměr: Ná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, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

• 1M0545, projekt VaV: Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky