Model Checking and Graph Theory in sequential ATPG