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, directly applying 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 propose a fail-safe practice for designing planning domain models that can inherently guarantee the safety of the produced plans in case of undetected errors in domain models.   In addition, we demonstrate how model checkers, as well as state trajectory constraints planning techniques, should be used to verify planning domain models so that unreachable counterexamples are not returned. Planning and task scheduling techniques are increasingly applied to real-world problems such as activity sequencing, constraint solving and resource management. These processes are implemented in planning-based automated systems which are already used in space missions BID14 BID3 BID0 , search and rescue BID12 , logistics BID19 and many other domains. Since the failure of such systems could have catastrophic consequences, these applications are regarded as safety-critical. Therefore, verification methods that are robust, trustworthy and systematic are crucial to gain confidence in the safety, integrity and correctness of these systems.The literature is rich with studies on verification of planning systems. For instance, BID17 carried out scenario-based testing and model-based validation of the remote agent that controlled the Deep Space 1 mission. Another example is the verification of the safety of the autonomous science agent design that was deployed on the Earth Orbiter 1 spacecraft .A typical planning system consists of a planning domain model, planning problem, planner, plan, executive, and mon-itor. Planners take as an input a domain model which describes application-specific states and actions, and a problem that specifies the goal and the initial state. From these inputs, a sequence of actions that can achieve the goal starting from the initial state is returned as plan. The plan is then executed by an executive to change the world state to match the desired goal.Our research focuses on the verification of planning domain models wrt. safety properties . Domain models provide the foundations for planning. They describe real-world actions by capturing their pre-conditions and effects. Due to modelling errors, a domain model might be inconsistent, incomplete, or inaccurate. This could cause the planner to fail in finding a plan or to generate unrealistic plans that will fail to execute in the real world. Moreover, erroneous domain models could lead planners to produce unsafe plans that, when executed, could cause catastrophic consequences in the real world.This paper addresses the fact that the state-of-the-art verification methods for planning domain models are vulnerable to false positive counterexamples. In particular, unconstrained verification tasks might return counterexamples that are unreachable by planners. Such counterexamples can mislead designers to unnecessarily restrict domain models, thereby potentially blocking valid and possibly necessary behaviours. In addition, false positive counterexamples can lead verification engineers to overlook counterexamples that are reachable by planners.To overcome these deficiencies, we propose to employ planning goals as constraints during verification. Thus, we introduce goal-constrained planning domain model verification, a novel concept that eliminates unreachable counterexamples per se. We formally prove that goal-constrained planning domain model verification of safety properties is guaranteed to return reachable counterexamples if and only if any exist. We also demonstrate two different ways to perform goal-constrained planning domain model verification, one using model checkers and the other using state trajectory constraints planning techniques. To the best of our knowledge, this work is the first to recommend fail-safe planning domain model design practice; introduce the concept of goal-constrained planning domain model verification. and demonstrate how model checkers, as well as state trajectory constraints planning techniques, can be used to perform goal-constrained planning domain model verification The rest of this paper is organised as follows. First, Section 2, contrasts the concepts presented here with related work. Second, Section 3 discusses the problem of unreachable counterexamples in planning domain model verification. Third, Section 4 proposes a design practice for planning domain models that can inherently guarantee domain model safety even in the case of undetected modelling errors. A verification concept of planning domain models that avoids returning unreachable counterexamples is presented in Section 5. Then, Section 6 discusses the implementation of this concept on the Cave Diving planning domain using Spin and MIPS-XXL. Finally, Section 7 concludes the paper and suggests future work . The verification of planning domain models is essential to guarantee the safety of planning-based automated systems.Unreachable counterexamples returned by unconstrained planning domain model verification techniques undermine the verification results.In this paper, we have discussed the potential deficiencies of this problem and provided an example of an unreachable counterexample form the literature. We then introduced goal-constrained verification, a new concept to address this problem, which restricts the verification task to a specific goal and initial state pair. This limits counterexamples to those practically reachable by a planner that is tasked with achieving the goal given the initial state. Consequently, our method verifies the domain model only wrt. a specific goal and initial state. This is an acceptable limitation, given that planners also operate on this basis.We have demonstrated how model checkers and planning techniques can be used to perform goal-constrained planning domain model verification. In addition, we have recommended an inherently safe practice for domain model design that guarantees the safety of domain models "by construction" in case of undetected modelling errors. Goalconstrained domain model verification ensures accurate verification results and complements the inherently safe domain model design practice to generate safe and error-free planning domain models.In conclusion, the main message of this paper is that the direct application of verification algorithms to the planning domain model verification problem can return counterexamples that would never be reached by planners in real planning tasks. These unreachable counterexamples can mislead the designers to perform unnecessary remediations that can be prone to errors. The proposed solution is simple which makes it readily usable in practice. It is also effective as formally proven in the paper.Currently, we are investigating the use of Temporally Extended Goals (TEGs) translators BID20 to perform goal-constrained domain model verification. As future work, we intend to automate the proposed methods, so that they can be applied to real-world sized planning domain models. Finally, we would like to perform an empirical comparison of the proposed methods to assess their scalability and performance.
Why and how to constrain planning domain model verification with planning goals to avoid unreachable counterexamples (false positives verification outcomes).
{"src": "scitldr-AIC_train", "paper_id": "SkxEtOGIqE"}