Exploiting Transition Locality in the disk based Murphi Verifier