The computational complexity of avoiding spurious states in state space abstraction