2
Planning domain model veri cation aims to demonstrate that any produced plan satis es a set of properties. To achieve this, formal planning domain model veri cation methods leave the planning goal open. This, we de ne as unconstrained veri cation of planning domain models, i.e. the veri cation is expected to hold for any potential goal. Unconstrained veri cation searches the domain model for a sequence of actions that can falsify the given property, regardless of any other conditions. In particular, whether or not a planner would consider this sequence to be a plan, is not taken into account. This is a critical oversight, because, when the domain model is used to solve a speci c planning problem, the sequence of actions that constitutes such a counterexample might, in fact, be \pruned away" by the planner, if it does not satisfy the planning goal. Hence, we consider them to be invalid planning counterexamples.
As an example, we consider the classical cave diving planning domain taken from the Satis cing Track of
the
The planning goals of this domain specify the required underwater locations of which photos are to be taken and mandate the divers must return to the surface after completing the mission.
A critical safety property, p, is that divers should not drown, i.e. they should not be in an underwater location, other than the entrance, where neither the divers nor the location have at least one full oxygen tank.
In this example, the chosen planning goal is to have a photo of the rst location, L1, and to get the diver outside the water. In unconstrained veri cation with only the safety property p, a counterexample could be hprepare-a-tank, enter-water, swim (L0; L1)i. Indeed, this counterexample leads the diver to a drowning state. At the end of this sequence, the diver will have consumed their oxygen tank and will be in underwater location L1. This is not the entrance, so they can not surface and they do not have an oxygen tank to swim back to the entrance. However, this is not a plan because it does not achieve any useful goal. Therefore, it will not be produced by any sound planner when it is used in a practical scenario (taking a photo of any location). Though this counterexample is obviously unreachable and should not misguide the designers to overcomplicate the model in an attempt to remove it, in a real-world sized application such invalid planning counterexamples can be much more di cult to recognise as such.
To overcome this, we observe that planning is performed for a speci c goal. To exploit this observation for domain model veri cation, we propose to use the goal given to the planner as a constraint to ensure that the counterexamples returned by a model checker, or other tools used in this context, falsify the given safety property while also achieving the planning goal. The details of this method are further explained in the next section. 3
Goal-constrained veri cation can be performed using advanced search algorithms, such as model checkers or classical planners, to nd a valid counterexample for the given safety property, if one exists.
We de ne a valid planning counterexample to be a sequence of actions that, rstly, can falsify the given safety property, secondly, can achieve the planning goal from the given initial state, and, thirdly, none of the sub-sequences of the counterexample can achieve the goal.
Formally, this is de ned as follows: Let the planning problem, P , be a tuple, (D; s0; g), where D is the domain model that describes the set of all available actions, A, s0 is the initial state and g is the desired goal. The plan is a solution to the planning problem P , de ned as a sequence of actions, = ha0; a1; :::; ani. These actions are chosen from A, ai 2 A, such that j= g. In other words, when is applied to the initial state s0 it yields a sequence of states S( ), S( ) = hs0; s1; :::; sni where the last state sn satis es the planning goal g, sn j= g. We say a plan satis es a property p, j= p, if the sequence of states S( ), generated by the plan , satis es the property p, S( ) j= p.
Furthermore, as de ned in [GNT04], we call a plan a redundant plan, if contains a subsequence, 0, 0 j , that achieves the goal g.
De nition 1: A valid planning counterexample for a safety property, p, of a planning problem is a non-redundant plan, , that falsi es the safety property, 6j= p.
Plans are required to be non-redundant in the de nition of valid planning counterexamples to exclude any plans that are enriched with action sequences which are unnecessary to achieve the planning goal but required to falsify the given safety property. Since sound planners can produce valid plans that have redundant subsequences, the scope of our method is limited to non-redundant planners, i.e. planners that are guaranteed to produce nonredundant plans.
We note that none of the current planning domain model veri cation methods verify planning domain models in their generality. Firstly, current methods require a grounded model, which represents a nite set of planning problems, in contrast to the in nite set of planning problems that non-ground domain models represent. Secondly, all methods need a speci c initial state to be able to perform the veri cation tasks. In our approach, by using the planning goal as one further constraint, we perform veri cation of single planning instances. This restriction is the cost associated with delivering a veri cation method that is robust against invalid planning counterexamples.
In the following subsections, we demonstrate how this concept can be realised using model checkers and state trajectory constraints planning techniques. 3.1
Model checkers verify safety properties by searching for counterexamples that falsify those properties. In the case of planning applications, any sequence of actions that does not achieve the given goal, will be pruned by any sound planner. Therefore, in planning domain veri cation, any counterexample that does not achieve the given planning goal should be eliminated on the basis that this counterexample is unreachable by the planner.
To force model checkers to only return valid planning counterexamples, the safety property is rst negated and then joined with the planning goal in a conjunction. This conjunction is then negated and supplied to the model checker as an input property. The nal property requires the model checker to nd a counterexample that both, falsi es the safety property and satis es the planning goal. Note that, unlike Def. 1, this permits sequences that falsify the property after satisfying the goal. To eliminate these sequences, model transitions should be augmented with an additional guard, representing the negation of the goal, to restrict all transitions once the goal is achieved. With this modi cation, the model checker is forced to return counterexamples that falsify the safety property before achieving the goal.
For a veri cation problem, V = (D; (s0; g); p), we rst check whether the planning goal is achievable, then we translate the domain model D into the model checker's input language, obtaining the model M that incorporates the initial state s0. Then, the model M is modi ed to M 0 by augmenting the guards of all transitions with the negation of the goal condition.
From the de nition of M 0, we can derive two properties: First, P1: all plans generated from M are also plans that can be generated from M 0. Proof: any sequence of transitions from M that ends with a transition that achieves the goal is also a sequence of transitions from M 0. These sequences represent valid plans as they terminate with a transition that achieves the goal. Therefore, all plans generated from M are also plans in M 0. Second, P2: any valid counterexample for M 0 is also a valid counterexample for M . Proof: as M 0 is a more constrained version of M , the set of all legal transition of M 0, (M 0), is contained in the set of all legal transitions of M , (M ), i.e. (M ) (M 0). It follows that any valid counterexample in (M 0) is also in (M ).
The model checker is then applied to the veri cation problem V 00 = (M 0; p0), where p0 is de ned using F , the eventually operator from Linear Temporal Logic (LTL) [CGP99], as follows:
p0 = : F (:p) ^ F (g) There are two possible outcomes. First, if the model checker returns a counterexample : 9 2 9 2 From the de nition of the LTL eventually operator F : (M 0): 6j= p0
(M 0): j= (F (:p) ^ F (g)) j= :p) Furthermore, from (8) it follows that 6j= p, con rming that there is at least one sequence of actions from D 9i 9j 0; si 2 S( ); si j= :p 0; sj 2 S( ); sj j= g
It follows that there is at least one sequence S( ) that falsi es the property p, and there is a state sj in that sequence which satis es the goal g, according to (3) and (4). In addition to that, in the sequence S( ), p is guaranteed to be falsi ed before g is satis ed. This is because 2 (M 0) and M 0 is constrained to not produce any transitions after achieving the goal. Thus, the counterexample is a valid planning counterexample in M 0 for the original safety property p as per Def. 1. Furthermore, from (P2 ), is also a counterexample in M . This proves that the DUV does not satisfy the safety property p with respect to the goal g.
The other potential outcome is that the model checker fails to nd a counterexample, then 8 2 (M 0): j= p0 j= :(F (g) ^ F (:p)) j= (:F (g) _ :F (:p))
j= G(p) j= :F (g) _ j= :F (:p) 6j= F (g) _ (6) j= F (g) ) j= G(p) (7) where G is the LTL always operator. This means p is always true for any sequence of actions in M 0 that achieves the goal, i.e. for all possible plans. Since from (P1 ) all plans generated from M are also plans in M 0, and from (7) all plans in M 0 are safe, we can conclude that all plans in M are safe. This proves that the DUV satis es the original property with respect to the goal. 3.2
Goal-constrained planning domain veri cation using planning techniques with state trajectory constraints Domain models can be veri ed to only produce safe plans, in terms of satisfying a given safety property, for a speci c goal using planners that use breadth rst search. This is achieved by consulting a planner over the DUV to produce a plan that can satisfy the goal and the negation of the property. If the domain model permits producing plans that, along with achieving the goal, contradict the safety property, then an unsafe plan can be found. Thus, the returned plan is a counterexample.
For a veri cation problem, V = (D; (s0; g); p), the safety property, p, is negated and expressed in terms of PDDL3.0 modal operators as shown in [GHL+09]. The result is added as a state trajectory constraint to the original domain model.
Using the algorithm proposed in [EJN06], the new model is transformed into a PDDL2 compatible version. This is performed by rst translating the state trajectory constraint into a non-deterministic nite state automaton (NFA). The NFA which can capture property violations is then embodied in the model in terms of additional predicates and conditional e ects. These additions observe the behaviour of the automaton that represents the constraint and stop goal satisfaction unless the constraint is satis ed too.
This yields a new planning problem, P 0 = (D0; s00; g0), where D0; s0 ; g0 are modi ed instances of D; s0; g 0 that are supplemented with the additional predicates and conditional e ects of the automaton that represents the introduced constraint. Let the set of legal sequences of actions that can be generated from D be (D) and from D0 be (D0). Note that D0 is an augmented version of D and the additions to D0 do not a ect the number of original operators, their preconditions, or their e ects. Furthermore, the additional conditional e ects do not a ect the original predicates. Hence, (D) = (D0).
Then, a planner is applied to P 0 with two possible outcomes. First, if the planner nds a plan then: 9 2 (D0): j= g0. Since the satisfaction of g0 implies both, the satisfaction of the original goal g at the last state of the sequence S( ), and the satisfaction of the state trajectory constraint (the negation of the safety property) by the sequence S( ): 9 2 (D0): ( j= g ^ j= :p). Furthermore, since (D) = (D0): (1) (2) (3) (4) (5) (8) that achieves the goal while not respecting the safety property. Therefore, this sequence is a valid planning counterexample for that property as per Def. 1. Hence, the DUV does not satisfy the property wrt. the planning goal. Alternatively, if the planner fails to nd a plan, then, as opposed to (8), we have: (D): ( j= g ^ (D): ( j= g ) j= :p) j= p)
(D): ( 6j= g _ 6j= :p) 8 2
Hence, any sequence of actions from D that achieves the goal also satis es the safety property. Therefore, the property holds for the planning domain model wrt. the given goal. (9) (10) (a) Evaluated states vs error depth using Spin (b) Evaluated states vs goal depth using Spin (c) Evaluated states vs error depth using MIPS (d) Evaluated states vs goal depth using MIPS To evaluate the feasibility and the behaviour of our approach, we designed two experiments to investigate how constraining the veri cation with the planning goal impacts the veri cation cost. This cost is measured by the number of states evaluated by the veri cation tools to con rm whether or not a counterexample exists.The scripts to repeat the experiments along with the data are available online.1
The rst experiment focuses on comparing the cost of both unconstrained and goal-constrained veri cation tasks while varying the safety property violation depth in order to explore situations with and without a valid planning counterexample. The safety property violation depth is hereafter termed \error depth". We synthesised a fully reachable model that consists of one critical and three independent variables, each with a range from 0 to 31. Each variable has two actions, one to increase and one to decrease its value by one. The goal is achieved when the critical variable value reaches 14. The error condition is changed from the value of the critical variable being 1 to 31. The range of the variables is chosen as 31 to expose any possible trends. Consequently, the number of variables is set to four to allow the model to be explored within a memory limit of 10 GB.
The second experiment investigates the e ect of the early termination of the veri cation process, after achieving the goal, on the cost of veri cation tasks while increasing the depth of the planning goal. The model used in this experiment has one critical and four independent variables, each with a range from 0 to 15. Variables have two actions as in the previous model. This time, there is no error in the model and the goal condition is varied from critical value 1 to 14. The variables' range is reduced to 15 to permit increasing the number of variables to ve while keeping the required memory within the 10 GB constraint. Both experiments are performed using the Spin model checker and the MIPS-XXL-IPC5 planner with breadth rst search option.
1https://github.com/Anas-Shrinah/Goal-constrained-planning-domain-model-veri cation-repository In the rst experiment, our approach showed broadly similar behaviour when it was applied using Spin and MIPS in Figure 1a and 1c. Note that the aim of these experiments is to showcase the feasibility of using our approach and to explore its behaviour, rather than comparing the performance of the veri cation tools. We believe such comparison depends heavily on the model under veri cation, for more insights the reader is referred to [Ede03, ABM09, LSD+12]. Ergo, we focus our discussion on the results obtained from model checking.
The vertical line in Figure 1a marks the goal level (critical value of 14) and splits the graph into two areas. On the right-hand side, the errors are deeper than the goal, i.e. the errors can only be reached after the goal is achieved. Thus, these errors are regarded as invalid planning counterexamples by our method as per Def. 1. Therefore, unlike unconstrained veri cation approaches, our method continues its exhaustive search to con rm the non-existence of any valid planning counterexamples. Thus, our method evaluates the maximum number of states for these veri cation tasks as shown in Figure 1a-(1).
On the left-hand side, the errors are shallower than the goal, i.e. the errors are reachable before achieving the goal. Hence, these errors are considered as valid planning counterexamples according to Def. 1. For the same veri cation task, Figure 1a-(2) shows that our method assesses more states than the unconstrained approaches as depicted in Figure 1a-(3). This is due to the fact that after nding an error, a safety property violation, our method keeps exploring and searching for a path to the planning goal while traditional methods terminate as soon as an error is found. However, the short counterexamples returned by these methods may or may not be valid planning counterexamples, whereas our method is guaranteed to return valid planning counterexamples only. The extra states visited by our approach are the cost associated with this guarantee.
In Figure 1a-(2) (and in Figure 1c-(2), respectively), we notice a drop in the number of evaluated states by our method as the error depth gets closer to the goal depth. This is attributed to the fact that the safety property (state trajectory constraint) in the model checker (planner) is translated into an automaton. This automaton in uences the state space exploration during the veri cation process. The automaton has a transition that is activated when an error is reached. Therefore, if an error is reached in an early stage in the veri cation, the error transition is triggered and the veri cation tool is forced to explore more states than if the error transition was triggered closer to the goal. Once both the error and the goal transitions are triggered, then the automaton reaches an acceptance state. Thus, the search terminates with a valid planning counterexample.
In the second experiment, Figure 1b shows that when using Spin with a planing domain model with no counterexample, our approach explores fewer states than unconstrained veri cation methods. This reduction in the veri cation cost is realised by the early termination of the veri cation search once the goal is achieved and no error could be found at shallower depths. This advantage of the goal-constrained veri cation approach comes at the cost of limiting the veri cation results to a single planning goal. Additionally, it is observed that the number of evaluated states by the goal-constrained veri cation method rises as an e ect of the increasing goal depth. This is caused by the expansion of the part of the model that needs to be checked as the goal depth increases. On the other hand, the unconstrained methods visit a constant number of states as they are independent from the goal depth by de nition.
Another interesting observation when using the planner in Figure 1d is that our method explores more states than the unconstrained veri cation approaches when the planning goal depth is more than three. This behaviour is caused by the interaction of two factors. In our approach, MIPS translates the state trajectory constraint to an automaton which is then incorporated in the planning domain model. Thus, the model used in our method is more complicated than the model used by the unconstrained approaches were state trajectory constraints are not used. After a certain depth of the planning goal, the extra states evaluated as a result of the additional state trajectory constraint in our method outweigh the saving from the early termination of the veri cation process. 5
Closely related, but di erent, is the work by [ABM09]. Their main objective is to treat veri cation as a planning task, whereas our aim is to demonstrate how model checkers and planners can be used for domain model veri cation. They proposed to perform system model veri cation using classical planners. To do this, they rst translated the model of the system under veri cation into a planning domain model. Then, the negation of the safety property to be established is used as the goal for the planner, which is then consulted to nd a plan that acts as counterexample for the given property. In our study, because our aim is to verify domain models against a given safety property with respect to a speci c goal, we use state trajectory constraints to restrict counterexamples to identify plans that can achieve the planning goal while falsifying the safety property. In their work the negation of the safety property is used as the goal. Whereas, in our method, the negation of the safety property is represented as a state trajectory constraint and the goal is the given planning goal.
[RPB09] also applied veri cation as planning to verify planning domain models, starting from LTL speci cations. This work fundamentally di ers from our work. They tested the impact of individual atomic propositions on the validity of the overall veri ed property by translating the speci cation properties into trap formulas. However, their method does not consider the interaction between property testing and the original planning goal. Note that nding a planning constraint to exercise a speci c atomic proposition is not enough to ensure the constraint itself would be exercised during the planning process. For example, a planning goal might be achieved through a state trajectory that does not exercise the hard constraint used to represent the tested property. Our work is mainly focused on investigating this interaction. Therefore, we use state trajectory constraints to guarantee the property is tested while achieving the planning goal.
[GKS12] also used classical planners for planning systems veri cation, but they examined verifying plans rather than domain models. They proposed an approach that uses classical planners to nd counterexamples for a given planning problem and plan instance. Their work and ours are related in that both suggest performing planning veri cation for a speci c planning problem rather than attempting unconstrained veri cation of a planning system. However, their work is limited to the veri cation of single plan instances, whereas our method veri es all potential plans that can be spun from a domain model for a speci c goal.
Among others, the researchers in [PPH98, KMH00, SHCS05, HGH+08, CFF+10] used model checkers to verify planning domain models. They translated the respective domain models into the input language of the selected model checker. The model checker is then applied to verify the domain model wrt. a given speci cation property. Similarly, we also propose a method to verify domain models using model checkers. However, our method di ers from the others in two aspects. First, in the way we de ne the planning domain model veri cation problem, and, second, in the way we use model checkers to perform veri cation. As explained in Section 3, we constrain the veri cation of planning domain models with a speci c goal. In contrast, previous studies perform unconstrained veri cation of domain models, i.e. they leave the goal open. As discussed in Section 2, the unconstrained goal may cause the model checker to return counterexamples that are unreachable when a planner uses the DUV. On the other hand, when the goal is constrained for veri cation, then we show that the returned counterexamples, if any, are guaranteed to be reachable by any sound planner. The second di erence is that, after the planning domain model is translated to the model checker's input language, we augment the model transitions, introducing the negation of the goal as a new constraint, thereby forcing the model checker to terminate once the goal is reached. This modi cation prevents the model checker from returning counterexamples that falsify the given property after satisfying the goal; these are unreachable by planners. 6
The veri cation of planning domain models is essential to guarantee the safety of planning-based automated systems. Invalid planning counterexamples returned by unconstrained planning domain model veri cation techniques undermine the veri cation results. They can mislead system designers to perform unnecessary remediations that can be prone to errors. In this paper, we introduced goal-constrained veri cation, a new concept to address this problem, which restricts the veri cation task to a speci c goal. This limits counterexamples to those practically reachable by a planner that is tasked with achieving the goal. Since we have excluded redundant plans from our de nition of valid planning counterexamples, the veri cation results of our method are limited to the application of non-redundant planners. A weaker form of non-redundancy will be considered in future work.
We have demonstrated how model checkers and planning techniques can be used to perform goal-constrained planning domain model veri cation. Our experimental evaluation con rms the feasibility of our method and presents its bene ts and limitations compared to unconstrained veri cation methods.
We note that a grounded planning domain model de nes a nite set of planning problems. Only a limited number of these problems are typically useful in practice. As such, our method might completely verify such subsets. As future work we intend to employ veri cation techniques such as veri cation reusability and compositionality [BLA+99], abstraction [CGL94] and symmetry reduction [CEJS98] to perform complete veri cation for practical subsets of grounded planning domain models. 6.0.1
The authors are grateful to Derek Long for his useful comments. [ABM09]
A. Albarghouthi, J. A. Baier, and S. A. McIlraith. On the use of planning technology for veri cation. In In VVPS09. Proceedings of the ICAPS Workshop on Veri cation & Validation of Planning & Scheduling Systems, 2009.
S. Bensalem, K. Havelund, and A. Orlandini. Veri cation and validation meet planning and scheduling. International Journal on Software Tools for Technology Transfer, 16(1):1{12, Feb 2014.