Simulation Preorder on Simple Process Algebras

We consider the problem of simulation preorder/equivalence between infinite-state processes and finite-state ones. We prove that simulation preorder (in both directions) and simulation equivalence are intractable between all major classes of infinite-state systems and finite-state ones. This result is obtained by showing that the problem whether a BPA (or BPP) process simulates a finitestate one is PSPACE-hard, and the other direction is co-NP-hard; consequently, simulation equivalence between BPA (or BPP) and finite-state processes is also co-NP-hard. The decidability border for the mentioned problem is also established. Simulation preorder (in both directions) and simulation equivalence are decidable in EXPTIME between pushdown processes and finite-state ones. On the other hand, simulation preorder is undecidable between PA and finite-state processes in both directions. The obtained results also hold for those PA and finite-state processes which are deterministic and normed,...

• Type: Conference
• Year: 1999
• Where: ICALP
• Authors: Antonín Kucera, Richard Mayr
• Keywords: ICALP 1999, Programming Languages, Simulation, Simulation Equivalence, finite-state Ones