The State Explosion Problem from Trace to Bisimulation Equivalence

摘要

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.