Exploiting Transition Locality in Automatic Verification