On the complexity of checking semantic equivalences between pushdown processes and finite-state processes

Simulation preorder/equivalence and bisimulation equivalence are the most commonly used equivalences in concurrency theory. Their standard definitions are often called strong simulation/bisimulation, while weak simulation/bisimulation abstracts from internal τ-actions. We study the computational complexity of checking these strong and weak semantic preorders/equivalences between pushdown processes and finite-state processes. We present a complete picture of the computational complexity of these problems and also study fixed-parameter tractability in two important input parameters: x, the size of the finite control of the pushdown process, and y, the size of the finite-state process. All simulation problems are generally EXPTIME-complete and only become polynomial if both parameters x and y are fixed. Weak bisimulation equivalence is PSPACE-complete, but becomes polynomial if and only if parameter x is fixed. Strong bisimulation equivalence is PSPACE-complete, but becomes polyn...

• Type: Journal
• Year: 2010
• Where: IANDC
• Authors: Antonín Kucera, Richard Mayr
• Keywords: Bisimulation Equivalence, Computational Complexity, IANDC 2010, Weak Bisimulation Equivalence