Other formats:
BibTeX
LaTeX
RIS
@inproceedings{405198, author = {Kučera, Antonín and Mayr, Richard}, address = {Berlin}, booktitle = {Proceedings of 27th International Symposium on Mathematical Foundations of Computer Science (MFCS 2002)}, keywords = {verification; concurrency; weak bisimilarity; infinite-state systems}, language = {eng}, location = {Berlin}, isbn = {3-540-44040-2}, pages = {433-445}, publisher = {Springer}, title = {On the Complexity of Semantic Equivalences for Pushdown Automata and BPA}, year = {2002} }
TY - JOUR ID - 405198 AU - Kučera, Antonín - Mayr, Richard PY - 2002 TI - On the Complexity of Semantic Equivalences for Pushdown Automata and BPA PB - Springer CY - Berlin SN - 3540440402 KW - verification KW - concurrency KW - weak bisimilarity KW - infinite-state systems N2 - We study the complexity of comparing pushdown automata (PDA) and context-free processes (BPA) to finite-state systems, w.r.t. strong and weak simulation preorder/equivalence and strong and weak bisimulation equivalence. We present a complete picture of the complexity of all these problems. In particular, we show that strong and weak simulation preorder (and hence simulation equivalence) is EXPTIME-complete between PDA/BPA and finite-state systems in both directions. For PDA the lower bound even holds if the finite-state system is fixed, while simulation-checking between BPA and any fixed finite-state system is already polynomial. Furthermore, we show that weak (and strong) bisimilarity between PDA and finite-state systems is PSPACE-complete, while strong (and weak) bisimilarity between two PDAs is EXPTIME-hard. ER -
KUČERA, Antonín and Richard MAYR. On the Complexity of Semantic Equivalences for Pushdown Automata and BPA. K. Diks, W. Rytter (Eds.). In \textit{Proceedings of 27th International Symposium on Mathematical Foundations of Computer Science (MFCS 2002)}. Berlin: Springer, 2002, p.~433-445. ISBN~3-540-44040-2.
|