Introduction

The automated planning problem is a central problem in AI which concerns with the search and the synthesis of a sequence of actions aimed to reach a given goal. It is a complex and wellstudied problem, and in the years several efficient solutions have been proposed in the literature to solve it. These include direct approaches such as forward or backward chain searches and partial order scheduling [1]. Other solutions consist of reducing it to other problems for which scalable and effective solutions exist, such as Boolean formula satisfiability (SAT) or model checking [2,3].

In this paper, we expand this arsenal of solutions by contributing another reduction, this time to the program verification problem. Given an instance of the planning problem, we construct a simple imperative program that nondeterministically simulates a sequence of actions starting from an initial state that fails an assertion whenever a target state is reached (see [4,5,6,7,8,9] for similar approaches in other domains). This type of reduction, although simple, opens up the possibility of using off-the-shelf automatic techniques and tools designed to verify programs in order to synthesise plans. These include approaches such as Bounded Model Checking (BMC), Abstract Interpretation, Counter-example Guided Abstraction Refinement, to name a few (see [10]). The programs produced through our reduction have a very particular form that we think could be exploited to refine and then specialise these approaches and techniques to work well for this class of noncanonical programs.

We begin our study following this direction, exploring the possibility of using BMC-based techniques in a simple way. We apply our approach to some benchmarks taken from the planning competition to demonstrate its feasibility. We leave for future investigations the possibility of exploiting other program verification techniques and tools. The planning problem is essentially a search problem over the states of a transition system, a set of states along with a set of actions that can change the current system state. Thus, given a set of states 𝑆 and a set of actions 𝐴 over them, the planning problem simply asks whether there is a sequence of actions from 𝐴 that starting from an initial state take the system to a state in a goal set 𝐺.

Preliminaries

To express the planning problem instances, we consider a simple PDDL-like language. The syntax is given in Figure 1. Here, an instance is composed of a domain and a problem. The domain part essentially identifies the transition system by defining the possible states through a set of Boolean predicates and constants, and a set of actions. Each action is defined over a list of parameters (that can assume the values of the given constants) and has a precondition and an effect with the meaning that an action can be taken on each state where the precondition holds and when taken, produces the change of the truth values of the predicates as described in the effect part. The problem part instead completes the domain with more constants (object part), and gives the initial values for the predicates (identifying the initial state) and the condition that must old for the goal states.

The syntax allowed for the preconditions and goals may vary depending on the specific planning language. Also, constants and objects may be typed, and functions that manipulate numeric types can be added. To keep the presentation simple here we limit to conditions that are just conjunctions of positive and negative atoms, and omit functions and types. However, these features and more complex conditions can be easily included in our code-to-code transformation.

Reduction to program verification: code-to-code translation

In this section, we describe the code-to-code translation that is the main part of our reduction. Instead of giving the formal translation we illustrate it by an example. For this we will use a classical and well-known planning domain, the so-called blocks world.

Example: blocks world. The blocks world domain consists of a set of cube-shaped blocks sitting on a table. The blocks can be piled up such that only one block can fit directly on top of another. A robot can pick up a block that is not below other ones (top) and move it to another position, either on the table or on top of another block. In this domain, both the initial state and the goal may consist of one or more piles of blocks. The goal instead consists of a single pile formed by block A on B and block B on C. We use the predicate On(x,y) to indicate that block x is on y (note that parameters are preceded by ? in the style of PDDLsyntax), where y is either another block or the table. We use another predicate Clear(x) to denote that x is top. In the domain, the actions are move and moveToTable. Action move(b,x,y) moves a block b on top of a block y provided that b and y are both top, additionally the object x (that might be a block as well or the

Code-to-code translation.

To illustrate our codeto-code translation, we refer to the example shown in Figure 2 (a). We use a simple imperative programming language (such as that of the analyzer ConcurInterproc: http://pop-art.inrialpes.fr/interproc/ concurinterprocweb.cgi). The program is shown in Figure 2 (b). We use scalar variables or arrays with global scope to encode predicates. We initialize these variables using the expression initial derived from the init component of the problem definition. The actions are each modelled with a procedure of the same name. Here we declare a number of local variables that model the parameters. These variables are initialized with a non deterministic value taken from the domain of the variables using the expression rand. To simulate the action we first check that the guessed values make the precondition evaluate to true, and if so we update the arrays modelling the predicates with a sequence of assignments derived from the effect of the action. The simulation is then orchestrated by the main procedure: it goes through an infinite loop whose body is crafted to simulate all actions in a non-deterministic way. The body also contains an assertion whose condition corresponds to the negation of the goal condition of the problem. Thus, to synthesise a plan we check whether the program fails this assertion. If so, by inspecting the counterexample we are able to construct a plan by listing the actions simulated along the counterexample. Of course, an instance of the planning problem that does not admit a plan leads to a program that is actually correct, that is, a program that has no executions leading to an assertion violation.

Implementation and experiments

To evaluate our approach, we implemented it into a prototype tool and conducted some preliminary experiments on the Agricola-sat18 benchmark taken from the 9th International Planning Competition (IPC'18) held at ICAPS 2018.

Prototype tool. Our tool is a code-to-code translation from PDDL planning instances to C programs. It is entirely written in python (version 3.8) and relies on the library pddlpy [11] to parse the PDDL instances. pddlpy provides a convenient API to extract the different kinds of elements of PDDL domains and problems.We have also extended the API of pddlpy to simplify the translation into a C program. The prototype uses CBMC (https://www.cprover.org/cbmc/) as backend for the program analysis. Thus a main parameter in the implemented approach is the number of rounds where we select the actions (which corresponds to the unwinding depth of the infinite loop of the main procedure). We support also a few more input parameters that can be given to trigger a swarm-like analysis (see [12,13]), enable some light partial order reductions, and few more search heuristics. Agricola-sat18. This benchmark set is based on the board game Agricola that models a farm with some workers. The game has a number of turns and stages, in which the player must select actions for the workers that are finalized to obtain more resources. The player may decide also to increase the number of workers. To reach the goal the player may take several actions per turn however this also increases the amount of food consumed at the end of the turn, that may lead into dead ends. The benchmark is composed of twenty planning instances sharing a common domain file. The model is written in the STRIPS fragment of PDDL which is slightly more expressive than the fragment presented in this paper: objects and constants are typed and also cost functions and numerical types are allowed.

Experiments. We run our tool on the entire benchmark set with round bound 20 finding plans for 6/20 problems and taking overall about 900s. We repeated the same experiment with bound 30, now taking about 7000s (including three 1200s timeouts) and finding plans for six more problems. We then focused only on the remaining eight unsolved problems by using increasing number of rounds up to 70 and timeouts up to 7200s. We found plans in three more problems for a total of 15/20 problems. Interestingly, the new plans where discovered with relatively low computational resources: 26 rounds and 1800s timeout, 31 rounds and 3000s timeout, 33 rounds and 300s timeout, respectively. These preliminary experiments show that our approach, although straightforward, is competitive with the best performing tools at the ICP'18 which were only able to solve one more problem, thus confirming our intuition that program verification can play a role in the automated planning domain.