Beyond Language Equivalence on Visibly Pushdown Automata

摘要

We study (bi)simulation-like preorder/equivalence checking on the class ofvisibly pushdown automata and its natural subclasses visibly BPA (Basic ProcessAlgebra) and visibly one-counter automata. We describe generic methods forproving complexity upper and lower bounds for a number of studied preorders andequivalences like simulation, completed simulation, ready simulation, 2-nestedsimulation preorders/equivalences and bisimulation equivalence. Our mainresults are that all the mentioned equivalences and preorders areEXPTIME-complete on visibly pushdown automata, PSPACE-complete on visiblyone-counter automata and P-complete on visibly BPA. Our PSPACE lower bound forvisibly one-counter automata improves also the previously known DP-hardnessresults for ordinary one-counter automata and one-counter nets. Finally, westudy regularity checking problems for visibly pushdown automata and show thatthey can be decided in polynomial time.