Verification and Validation of Planning Domain Models

Abstract

The verification and validation of planning domain models is one of the biggest challenges to deploying planning-based automated systems in the real world.
The state-of-the-art verification methods of planning domain models are vulnerable to false positives, i.e. counterexamples that are unreachable by sound planners when using the domain under verification during planning tasks. False positives mislead designers into believing correct models are faulty. Consequently, designers needlessly debug correct models to remove these false positives. This process might unnecessarily constrain planning domain models, which can eradicate valid and sometimes required behaviours. Moreover, catching and debugging errors without knowing they are false positives can give verification engineers a false sense of achievement, which might cause them to overlook valid errors.
To address this shortfall, the first part of this thesis introduces goal-constrained planning domain model verification, a novel approach that constrains the verification of planning domain models with planning goals to reduce the number of unreachable planning counterexamples. This thesis formally proves the correctness of this method and demonstrates the application of this approach using the model checker Spin and the planner MIPS-XXL. Furthermore, it reports the empirical experiments that validate the feasibility and investigates the performance of the goal-constrained verification approach. The experiments show that not only the goal-constrained verification method is robust against false positive errors, but it also outperforms under-constrained verification tasks in terms of time and memory in some cases.
The second part of this thesis investigates the problem of validating the functional equivalence of planning domain models. 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. Despite the need and importance of proving the functional equivalence of planning domain models, this problem attracted limited research interest.
This thesis builds on and extends previous research by proposing a novel approach to validate the functional equivalence of planning domain models. First, this approach employs a planner to remove redundant operators from the given domain models; then, it uses a Satisfiability Modulo Theories (SMT) solver to check if a predicate mapping exists between the two domain models that makes them functionally equivalent. The soundness and completeness of this functional equivalence validation method are formally proven in this thesis.
Furthermore, this thesis introduces D-VAL, the first planning domain model automatic validation tool. D-VAL uses the FF planner and the Z3 SMT solver to prove the functional equivalence of planning domain models. Moreover, this thesis demonstrates the feasibility and evaluates the performance of D-VAL against thirteen planning domain models from the International Planning Competition (IPC). Empirical evaluation shows that D-VAL validates the functional equivalence of the most challenging task in less than 43 seconds. These experiments and their results provide a benchmark to evaluate the feasibility and performance of future related work.

Date of Award	5 Dec 2023
Original language	English
Awarding Institution	University of Bristol
Sponsors	Engineering and Physical Sciences Research Council & Schlumberger
Supervisor	Kerstin I Eder (Supervisor) & Derek Long (Supervisor)