On the Complexity of Semantic Equivalences for Pushdown Automata and BPA
| Autoři | |
|---|---|
| Rok publikování | 2002 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of 27th International Symposium on Mathematical Foundations of Computer Science (MFCS 2002) |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Počítačový hardware a software |
| Klíčová slova | verification; concurrency; weak bisimilarity; infinite-state systems |
| Popis | 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. |
| Související projekty: |