Deductive local model checking : on the verification of CTL* properties of infinite-state reactive systems