Model Checking and Abstraction