Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete