## Abstract

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.

Original language | English |
---|---|

Pages (from-to) | 772-796 |

Number of pages | 25 |

Journal | Information and Computation |

Volume | 208 |

Issue number | 7 |

DOIs | |

Publication status | Published - Jul 2010 |