[hwayne]

I do think there's an interesting and deep connection between the world of model checking and the world of planning (as most often done in logic languages).