Model Checking Multithreaded Programs by means of reduced models