Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems