  This paper introduces an approach to validate the functional equivalence of
planning domain models. Validating the functional equivalence of planning
domain models is the problem of formally confirming that two planning domain
models can be used to solve the same set of problems for any set of objects.
The need for techniques to validate the functional equivalence of planning
domain models has been highlighted in previous research and has applications in
model learning, development and extension. We prove the soundness and
completeness of our method. We also develop D-VAL, an automatic functional
equivalence validation tool for planning domain models. Empirical evaluation
shows that D-VAL validates the functional equivalence of all examined domains
in less than 43 seconds. Additionally, we provide a benchmark to evaluate the
feasibility and performance of this and future related work.
