  The verification of planning domain models is crucial to ensure the safety,
integrity and correctness of planning-based automated systems. This task is
usually performed using model checking techniques. However, unconstrained
application of model checkers to verify planning domain models can result in
false positives, i.e.counterexamples that are unreachable by a sound planner
when using the domain under verification during a planning task. In this paper,
we discuss the downside of unconstrained planning domain model verification. We
then introduce the notion of a valid planning counterexample, and demonstrate
how model checkers, as well as state trajectory constraints planning
techniques, should be used to verify planning domain models so that invalid
planning counterexamples are not returned.
