Unfortunately I'm missing something rather crucial with the Model Checking stuff. Page 102 of the notes gives a primitive recursive definition for ReachBy with ReachBy n R B s n = number of steps R = transition relation B = initial states But what is s? Many Thanks, James