In this paper, we report on a preliminary study on the feasibility of applying techniques and tools for finding errors in programs, or prove them entirely correct, to efectively explore the large state space of instances of the automated planning problem (AP). To leverage the recent advancements in the symbolic program analysis, we design a simple reduction from AP to the configuration reachability problem of programs and then use of-the-shelf program verification tools. We evaluate the feasibility of our approach on the Agricola-sat18 benchmark used at IPC'18.
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 eficient 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 [
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 [
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 instance ::= domain problem the states of a transition system, a set of states along with a domain ::= (define (domain id ) set of actions that can change the current system state. Thus, ((::cpornesdtiacnattsesidplliisstt)) given a set of states and a set of actions over them, the actions ) planning problem simply asks whether there is a sequence actions ::= (aactcitoinosnacidtions | of actions from that starting from an initial state take the (:parameters parlist ) system to a state in a goal set . ((::perfefceoctndibt)ion b ) )
To express the planning problem instances, we consider problem ::= (define (problem id ) a simple PDDL-like language. The syntax is given in Figure (:domain id ) 1. Here, an instance is composed of a domain and a problem. ((::ionbijtectastlisitd)list ) The domain part essentially identifies the transition system by (:goal b ) ) defining the possible states through a set of Boolean predicates Figure 1: Planning language. 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 efect 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 efect 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.
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. Code-to-code translation. To illustrate our codeto-code translation, we refer to the example shown proc move() in Figure 2 (a). We use a simple imperative pro- bebg=irnand; x=rand; y=rand; gramming language (such as that of the analyzer if (Clear[y] and Clear[b] and On[b,x]) ConcurInterproc: http://pop-art.inrialpes.fr/interproc/ theCnlear[x] = true; Clear[y] = false; concurinterprocweb.cgi). The program is shown in On[b,y] = true; On[b,x] = false; Figure 2 (b). We use scalar variables or arrays with end global scope to encode predicates. We initialize these proc moveToTable() var b:obj, x:obj; variables using the expression initial derived from bebg=irnand; x=rand; the init component of the problem definition. The ac- if (On[b,x] and Clear[b]) then tions are each modelled with a procedure of the same COlne[abr,[txa]ble] == ttrruuee;; name. Here we declare a number of local variables On[b,x] = false; that model the parameters. These variables are ini- end tialized with a non deterministic value taken from the begin //main procedure domain of the variables using the expression rand. To whiifl(ebr(atnrdu)e)then move(); endif; simulate the action we first check that the guessed if (brand) then moveToTable(); endif; values make the precondition evaluate to true, and if endasser/t/(fnaoitl Oinf[Ag,oBa]l ocronnfotisOnr[eBa,cCh]e)d; so we update the arrays modelling the predicates with (b) Program encoding 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 nondeterministic 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.
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 [
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.