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.
|
