D-VAL: An automatic functional equivalence validation tool for planning domain models
This addresses a need in planning model development and learning, though it appears incremental as it builds on prior research.
The paper tackles the problem of validating functional equivalence between planning domain models, introducing D-VAL, an automatic tool that proves soundness and completeness and validates all examined domains in under 43 seconds.
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.