The State-Explosion Problem from Trace to Bisimulation Equivalence. F. Laroussinie and Ph. Schnoebelen. FoSSaCS 2000 Abstract: We show that any relation between the simulation preorder and bisimilarity is EXPTIME-hard when systems are given as networks of finite state systems (or equivalently as automata with boolean variables, etc.). We also show that any relation between trace inclusion and ready trace equivalence or possible-futures equivalence is EXPSPACE-hard for these systems. These results match the already known upper bounds and partially answer a conjecture by Rabinovich. They strongly suggest that there is no way to escape the state explosion problem when checking behavioural relations. For the branching-time relations, our proof uses a new construction that immediately applies to timed automata, a family of systems for which these complexity results are new.