D-VAL: An automatic functional equivalence validation tool for planning domain models

TL;DR

This paper presents D-VAL, an automatic tool for validating the functional equivalence of planning domain models, ensuring they can solve the same problems, with proven soundness, completeness, and efficient performance.

Contribution

The paper introduces D-VAL, a novel automatic validation tool for planning domain models, with proven correctness and a new benchmark for evaluation.

Findings

D-VAL validates equivalence in under 43 seconds for tested domains.

The method is sound and complete.

A benchmark for future evaluation is provided.

Abstract

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.