{Model Checking in {CLP}}