Hardness of equivalence checking for composed finite-state systems

Computational complexity of comparing behaviours of systems composed from interacting finite-state components is considered. The main result shows that the respective problems are EXPTIME-hard for all relations between bisimulation equivalence and trace preorder, as conjectured by Rabinovich (Inf Comput 139(2):111-129, 1997). The result is proved for a specific model of parallel compositions where the components synchronize on shared actions but it can be easily extended to other similar models, to labelled 1-safe Petri nets. Further hardness results are shown for special cases of acyclic systems.