Abstract interpretation and partition refinement for model checking by D.R. Dams