Abstraction in Planning via Model Checking