Defining Classical Planning Problems in Functional STRIPS [WORK IN PROGRESS]

Functional STRIPS (FSTRIPS, for short) is a classical planning language that extends STRIPS with functional systems in order to provide a number of expressive and computational advantages, such as the ability of making indirect refernce to domain objects through the use of nested terms.

Tarski lifts Geffner’s original restrictions on the language, and follows a full first-order logic approach. We will use the classical Blocks World domain as a running example.

Problem Language

Tarski supports the formulation of FSTRIPS problems \(P\) defined over a many-sorted first-order logic language with equality. We note the language associated with a prolem \(P\) as \({\cal L}(P)\).

As we have seen in previous chapters of this Tutorial, Tarski languages are made up of a finite set of sorts \(T\), a possibly infinite number of variables \(v_{1}^t\), \(v_{2}^t, \ldots\) for each sort \(t \in T\), a set \(\Phi\) of function symbols and a set \(\Pi\) of relation symbols, assumed to include a number of symbols with fixed denotation, such as equality.

We can create the language \({\cal L}(P)\) for Blocks World as follows

import tarski
from tarski.syntax import *

# 1. Create language to model the domain
bw = tarski.language('BlocksWorld', theories=['equality', 'arithmetic'])

Tarski comes with several theories that define a number of useful built-in predicates and functions. For the purpose of this example we will be adding the theory of equality, which gives us access to the predicates \(=\) and \(\neq\). The set of supported theories is covered in a specific tutorial.

We define the set of sorts \(T_{blocksworld}\) in our language like this

# 2. Define sorts that organise the objects considered
place = bw.sort('place')
block = bw.sort('block', place)

where the sort block is a subset of place. We define domain specific function symbols \(\phi_{blocks world}\)

# 3. Define functions
loc = bw.function( 'loc', block, place )
width = bw.function('width', place, bw.Real)
looking_at = bw.function( 'looking_at', block )
holding = bw.function( 'holding', block)

and domain specific predicate symbols \(\Pi_{blocksworld}\)

# 4. Define predicates
clear = bw.predicate( 'clear', block)

Problem Interpretations

The current version of Tarski requires that the universe of discourse in any FSTRIPS problem \(P\) is fixed. That is, all valid interpretations \({\cal M}\) for \({\cal L}(P)\) have the same universe, denoted by \({\cal U}_P = \{ {\cal U}_t \}_{t \in T}\). It is further required that the universe \({\cal U}_t\) of any sort \(t\) is finite, this is a limitation of the current and provably future versions of Tarski.

In our model of Blocks World interpretations \({\cal M}\) for \({\cal L}(P)\) consist of two sorts as defined above. We set \({\cal U}_{place}\) to \(\{ b_1, b_2, b_3, b_4, table \}\) as follows

table = bw.constant('table', place)
b1, b2, b3, b4 = [ bw.constant('b_{}'.format(k), block) for k in (1,2,3,4) ]

Note that since block is a subtype of place, every time a new constant of sort block is defined the domain of place changes accordingly. The universe of the second sort we defined, \({\cal U}_{blocks}\), has been set implicitly as well. We will collect all the blocks in a list for convenience.

the_blocks = [b1, b2, b3, b4]

As a result of the universe of discourse being fixed, every interpretation for the language bw shares sorts and associated constant symbols. On the other hand, the denotation of functions and predicates is subject to change. Interpretations (or models) \({\cal M}\) of Tarski languages are objects that allow to associate function symbols with constants and predicate symbols with truth values.

Models are created around a given language

import tarski.model

M = tarski.model.create(bw)

and require an evaluation method to be bound by the user

from tarski.evaluators.simple import evaluate

M.evaluator = evaluate

For the purposes of this example, we will set the denotation of function and predicate symbols as follows

M.set( loc(b1), b2) # loc(b1) := b2
M.set( loc(b2), b3) # loc(b2) := b3
M.set( loc(b3), table) # loc(b3) := table
M.set( loc(b4), table) # loc(b4) := table

M.set( width(b1), 3.0) # width(b1) := 3.0
M.set( width(b2), 2.0) # width(b2) := 2.0
M.set( width(b3), 1.0) # width(b3) := 1.0
M.set( width(b4), 0.5) # width(b4) := 0.5
M.set( width(table), 100.0) # width(table) := 100.0

M.set( looking_at(), b1) # looking_at() := b1

M.add( clear, b1) # clear(b1) := T
M.add( clear, b4) # clear(b4) := T

Action Schemas

A Functional STRIPS action schema \(a\) is defined by: - a name, an alphanumeric identifier, - a signature \((v_1,\ldots,v_n)\), where each \(v_i\) is a variable of some sort \(T\), - a precondition formula \(\mathrm{pre}(a)\), an arbitrary formula over \({\cal L}(P)\), - a set of conditional effects \(\mathrm{effs}(a)\)

Each effect \(e \in \mathrm{effs}(a)\) can be either a relational or functional effect. Actions have unspecified durations, measured as number of time steps \(dur(a)\). In Classical FSTRIPS problems durations of all actions are \(1\), Differential FSTRIPS problems allow \(dur(a)\) to be fixed to or bounded by an arbitrary constant. Note: This formalisation is still WIP.

Relational Effects

Relational effects of actions \(a\) specify general properties states must have after the action has been executed. The current version of Tarski requires relational effects to be of the form

\[\phi \rightarrow L\]

where \(\phi\) is an arbitrary formula over \({\cal L}(P)\) and \(L\) is a literal. Literals are atomic formulas \(R(\bar{t})\) or their negation, \(\neg R(\bar{t})\) over the predicates \(R\) of a given language. In the first case, we say that the effect is an add effect, in the second, a delete effect.

Relational effects can be formalised as Linear Temporal Logic (LTL) formulas such as

\[\phi \rightarrow X L\]

The above specifies the precise meaning of the effect, that is: that if \(\phi\) is true on the current state, then necessarily \(L\), as interpreted in the current state, needs to be true in the neXt state.

Functional Effects

Functional effects of actions \(a\) allow actions to set directly the denotation of a given functional symbol \(f(\bar{t})\) in states resulting from \(a\) being done. Tarski current implementation of Functional STRIPS requires these effects to have the form

\[\phi \rightarrow f(\bar{t}) := w\]

where \(w\) is an arbitrary term. \(f(\bar{t})\) is made up of a function symbol \(f\), of whatever arity, over a tuple of terms \(\bar{t}\) of appropiate size and type. The types of the term \(w\) and symbol \(f\) must coincide.

The LTL specification for functional effects is as follows

\[\phi \rightarrow X( f(\bar{t}) = w)\]

with the same semantics, and proviso with respect to interpretation of terms, as above.

Constructing action schemas with Tarski

In order to define action schemas, we need to load Tarki’s fstrips module

import tarski.fstrips as fs

Let \(A\) be our set of actions, initially empty

A = []

The first action we will model is move that allows us to move the block we’re currently looking at on top of a different one which is currently clear. The action involves two objects. One is referred to indirectly as whatever is looking_at() mapping to. The second one is unspecified, it could be any block other than the one we’re looking at. Hence we define it as a variable of sort block

dest = bw.variable('dest', block)

and the precondition formula is the conjunction

pre = land( clear(looking_at()), clear(dest), looking_at() != dest )

This formula is only true whenever: - The block we’re looking at is clear, - the block referred to by variable \(dest\) is clear too, and - both blocks are different.

Note that we have not needed to define the predicate \(\neq\), it was attached automatically to the FOL \(bw\) when we called the constructor above.

The effects of the action are such that: - The block we’re looking at is now placed on top of \(dest\) (i.e. \(loc(looking\_at()):= dest\))

eff1 = fs.FunctionalEffect(loc(looking_at()), dest)

• block \(dest\) is no longer clear (i.e. \(\neg clear(dest)\) must be true in the next state)

eff2 = fs.DelEffect(clear(dest))

We put together the components of the action and tag it with a descriptive name

move_schema = fs.Action(bw, name='move', \
                     parameters=[dest], \
                     precondition=pre,
                     effects = [eff1, eff2])

and update the set of actions \(A\) s.t. \(A = A \cup \{ move \}\)

A.append(move_schema)

The other action we need allows to change the block we’re looking at. We can do that at any time - the precondition is \(\top\), that is, always true - and the effect is that we end up looking at whatever block we have selected.

We define the action reusing the variable symbol \(dest\) we created above and set preconditions, effects and name as follows.

look_at_schema = fs.Action( bw, name='look_at',\
                           parameters=[dest],\
                           precondition=top,\
                           effects = [ fs.FunctionalEffect(looking_at(), dest)]
)

and we add it to to our set of actions

A.append(look_at_schema)

Below follows the text based representation of the actions we have modeled so far

for k, a in enumerate(A) : print('{}. {}'.format(k,a))

0. move(dest: block)
1. look_at(dest: block)

Constraints

The truth values of the predicate \(clear(p)\) for any place \(p\) need to be consistent with the following formula

\[\forall x/place,\, \neg clear(x) \leftrightarrow x \neq table \land \exists y/block,\, loc(y)=x\]

x = bw.variable('x', block)
y = bw.variable('y', block)
clear_constraint = forall( x, equiv( neg(clear(x)), land( x != table, exists(y, loc(y) == x ) )) )
print(clear_constraint)

forall x : ((((not (not clear(x))) or (!=(x,table) and exists y : (=(loc(y),x)))) and ((not (!=(x,table) and exists y : (=(loc(y),x)))) or (not clear(x)))))

The (redundant) constraint above is binding the truth value of the predicate \(clear(x)\) to two conditions:

• \(x\) is not the \(table\) object, or in other words, \(clear(table)\) is always true

• there is no block \(y\) on top of \(x\), e.g. \(loc(y) = x\)

Goals

The final constraint we need to specify is the one that goal states need to comply with, the goal formula

\[loc(b_1) = loc(b_2) \land loc(b_3) = loc(b_4) \land loc(b_4) = table\]

which corresponds with the blocks arranged in a tower, one of top the other.

land( loc(b1) == loc(b2), land( loc(b3) == loc(b4), loc(b4) == table))

(=(loc(b_1),loc(b_2)) and (=(loc(b_3),loc(b_4)) and =(loc(b_4),table)))

First-Order Quantification

Conditional Effects

Derived Predicates