Model Checking and Reachability