Semi-external LTL Model Checking