=Paper=
{{Paper
|id=Vol-2987/paper3
|storemode=property
|title=Automated Planning Through Program Verification
|pdfUrl=https://ceur-ws.org/Vol-2987/paper3.pdf
|volume=Vol-2987
|authors=Salvatore La Torre,Gennaro Parlato
|dblpUrl=https://dblp.org/rec/conf/gandalf/TorreP21
}}
==Automated Planning Through Program Verification==
https://ceur-ws.org/Vol-2987/paper3.pdf
Automated Planning Through Program Verification
Salvatore La Torre1 , Gennaro Parlato2
1
University of Salerno, Italy
2
University of Molise, Italy
Abstract
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 effectively 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 off-the-shelf program verification tools. We evaluate the feasibility
of our approach on the Agricola-sat18 benchmark used at IPCβ18.
Keywords
Automated Planning, Formal Methods, Program Verification
1. 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 well-
studied 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.
OVERLAY 2021: 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis,
September 22, 2021, Padova, Italy
" slatorre@unisa.it (S. La Torre); gennaro.parlato@unimol.it (G. Parlato)
0000-0002-4978-4307 (S. La Torre); 0000-0002-8697-2980 (G. Parlato)
Β© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org)
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.
2. Preliminaries
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 )
(:constants idlist )
set of actions that can change the current system state. Thus, (:predicates plist )
given a set of states π and a set of actions π΄ over them, the actions )
actions ::= actions actions |
planning problem simply asks whether there is a sequence (action id
of actions from π΄ that starting from an initial state take the (:parameters parlist )
system to a state in a goal set πΊ. (:precondition b )
(:effect 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 )
(:objects idlist )
1. Here, an instance is composed of a domain and a problem. (:init atlist )
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 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.
3. 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.
Figure 2.(a) gives a PDDL-like encoding of a plan- (define (domain blocks)
ning instance based on this domain where the initial (:constants table)
(:predicates (On ?x ?y)(Clear ?x) )
state is given by two piles: one formed by the sole block (:action move
B and the other formed by block C on top of block A. :parameters (?b ?x ?y)
:precondition (and (On ?b ?x)
The goal instead consists of a single pile formed by (Clear ?b) (Clear ?y) )
block A on B and block B on C. We use the predicate :effect (and (On ?b ?y) (Clear ?x)
(not(On ?b ?x)) (not(Clear ?y)) ) )
On(x,y) to indicate that block x is on y (note that (:action moveToTable
parameters are preceded by ? in the style of PDDL- :parameters (?b ?x)
syntax), where y is either another block or the table. :precondition (and (On?b?x)(Clear ?b))
:effect (and (On ?b table) (Clear ?x)
We use another predicate Clear(x) to denote that (not(On ?b ?x)) ) ))
x is top. In the domain, the actions are move and (define (problem p1)
moveToTable. Action move(b,x,y) moves a block (:domain blocks)
(:objects A B C )
b on top of a block y provided that b and y are both top, (:init (On A table) (On B table)
additionally the object x (that might be a block as well (On C A) (Clear B) (Clear C) )
or the table) sitting right below b must become top.
(:goal (and (On A B) (On B C)) ) )
Action moveToTable(b,x) just moves a top block (a) PDDL-like instance
b on the table and makes the object x below b a typedef obj = enum {table,A,B,C};
top one. A solving plan for the described planning var On[obj,obj]:bool, Clear[obj]:bool;
instance consists of three steps: movetoTable(C,A), initial( On[A,table] == true and
move(B,table,C), and move(A,table,B). On[B,table] == true and
On[C,A] == true and
Clear[B] == true and
Code-to-code translation. To illustrate our code- Clear[C] == true );
to-code translation, we refer to the example shown proc move() var b:obj, x:obj, y:obj;
begin
in Figure 2 (a). We use a simple imperative pro- b=rand; 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/ then
Clear[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;
begin
variables using the expression initial derived from b=rand; 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 Clear[x] = true;
On[b,table] = true;
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
while (true)
domain of the variables using the expression rand. To if (brand) then move(); endif;
simulate the action we first check that the guessed if (brand) then moveToTable(); endif;
assert(not On[A,B] or not On[B,C]);
values make the precondition evaluate to true, and if end //fail if goal conf is reached
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 Figure 2: (a) PDDL-like Example (b)
the main procedure: it goes through an infinite loop a program that simulates the
whose body is crafted to simulate all actions in a non- behaviour of (a).
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.
4. Implementation and experiments
To evaluate our approach, we implemented it into a prototype tool and conducted some prelimi-
nary 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.
References
[1] M. Ghallab, D. S. Nau, P. Traverso, Automated Planning and Acting, Cambridge University
Press, 2016.
[2] J. Rintanen, Planning and SAT, in: A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.),
Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications,
2009, pp. 483β504. URL: https://doi.org/10.3233/978-1-58603-929-5-483.
[3] F. Giunchiglia, P. Traverso, Planning as model checking, in: Recent Advances in AI
Planning, Berlin, Heidelberg, 2000, pp. 1β20.
[4] A. L. Ferrara, P. Madhusudan, G. Parlato, Security analysis of role-based access control
through program verification, in: 25th IEEE Computer Security Foundations Symposium,
CSF 2012, 2012, pp. 113β125. URL: https://doi.org/10.1109/CSF.2012.28.
[5] A. L. Ferrara, P. Madhusudan, G. Parlato, Policy analysis for self-administrated role-based
access control, in: Tools and Algorithms for the Construction and Analysis of Systems -
19th International Conference, TACAS 2013. Proceedings, volume 7795 of LNCS, 2013, pp.
432β447. URL: https://doi.org/10.1007/978-3-642-36742-7_30.
[6] A. L. Ferrara, P. Madhusudan, T. L. Nguyen, G. Parlato, Vac - verifier of administrative
role-based access control policies, in: Computer Aided Verification - 26th International
Conference, CAV 2014. Proceedings, volume 8559 of LNCS, 2014, pp. 184β191. URL: https:
//doi.org/10.1007/978-3-319-08867-9_12.
[7] O. Inverso, E. Tomasco, B. Fischer, S. La Torre, G. Parlato, Bounded model checking of
multi-threaded C programs via lazy sequentialization, in: Computer Aided Verification -
26th International Conference, CAV 2014. Proceedings, volume 8559 of LNCS, 2014, pp.
585β602. URL: https://doi.org/10.1007/978-3-319-08867-9_39.
[8] E. Tomasco, O. Inverso, B. Fischer, S. La Torre, G. Parlato, Verifying concurrent programs
by memory unwinding, in: Tools and Algorithms for the Construction and Analysis of
Systems - 21st International Conference, TACAS 2015. Proceedings, volume 9035 of LNCS,
2015, pp. 551β565. URL: https://doi.org/10.1007/978-3-662-46681-0_52.
[9] T. L. Nguyen, B. Fischer, S. La Torre, G. Parlato, Lazy sequentialization for the safety
verification of unbounded concurrent programs, in: Automated Technology for Verification
and Analysis - 14th International Symposium, ATVA 2016. Proceedings, volume 9938 of
LNCS, 2016, pp. 174β191. URL: https://doi.org/10.1007/978-3-319-46520-3_12.
[10] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem (Eds.), Handbook of Model Checking,
2018. URL: https://doi.org/10.1007/978-3-319-10575-8.
[11] H. Foffani, A python PDDL parser, 2017. URL: https://pypi.org/project/pddlpy/.
[12] G. J. Holzmann, R. Joshi, A. Groce, Swarm verification techniques, IEEE Trans. Software
Eng. 37 (2011) 845β857. URL: https://doi.org/10.1109/TSE.2010.110.
[13] E. Tomasco, B. Fischer, S. La Torre, T. L. Nguyen, G. Parlato, P. Schrammel, Parallel
bug-finding in concurrent programs via reduced interleaving instances, in: Proceedings of
the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE
2017, 2017, pp. 753β764. URL: https://doi.org/10.1109/ASE.2017.8115686.