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 tau-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 polynomial if either parameter x or y is fixed. Crown Copyright (C) 2010 Published by Elsevier Inc. All rights reserved.