Abstract
Evaluation of the properties of various planning techniques such as completeness and termination plays an important role in choosing an appropriate planning technique for a particular planning problem. In this paper, we use the already existing formal specification of two well-known and classic state space planning techniques, forward state space planning and goal stack state space planning techniques, in Transaction Logic(\( \mathcal {TR} \)) to study their completeness. Our study shows that using \( \mathcal {TR} \), we can formally specify the serializability of planning problems and prove the completeness of \( \textit{STRIPS}\) planning problems for planning problems with serializable goals.
This work was supported, in part, by the NSF grant 0964196.
Access provided by Autonomous University of Puebla. Download conference paper PDF
Similar content being viewed by others
Keywords
1 Introduction
Evaluation of different properties of planning techniques such as termination and completeness becomes more essential when, in many cases, different search strategies of a planning technique may affect the performance of planning process while different properties such as completeness and termination is required. For example, forward state space planning and goal stack space planning techniques may have different execution time when they are used by a robot in the famous block world example while Sussman Anomaly [1] shows that goal stack space planning is not guaranteed to succeed. Such considerations need appropriate formal frameworks to represent the planning techniques properly.
Using logical deduction to solve a planning problem has been a popular approach for more than three decades [2–6]. However, none of the existing logical frameworks of deductive planners are used to study the different properties of planning techniques because these planners are just relying on their corresponding inference systems to search for a plan and they are not expressive enough to formally represent more complicated planning techniques such as goal state space planning. Therefore, the requirement of a formal, neat, and expressive logical framework for such studies seems to be inevitable.
In this paper, we are using the encoding of forward state space planning and goal stack state space planning techniques in Transaction Logic(\( \mathcal {TR} \)) for the evaluation of their completeness. Our paper shows that \( \mathcal {TR} \) is an appropriate logical framework for such evaluation. Unlike above mentioned logical frameworks, the well-defined model theory of \( \mathcal {TR} \) together with its sound and complete proof theory let us easily prove different properties of planning techniques such as completeness. It also lets us formally redefine the concept of goal serializablity in planning that is used to examine the completeness of goal stack state space planning technique for planning problems. Our simple and straightforward proofs for two classic planning techniques, forward state space planning (called naïveFootnote 1) and goal stack state space (called \( \textit{STRIPS}\) Footnote 2) are evidences for this claim.
The next section briefly characterizes a planning problem. The third section explains how we formally encode planning techniques in \( \mathcal {TR} \) and the last section concludes our paper.
2 Characterization of a Planning Problem
In a \( \textit{STRIPS}\) planning problem, actions update the state of a system. We assume denumerable sets of variables \( \mathcal {X} \), constants \( \mathcal {C} \), and disjoint sets of predicate symbols, extensional (\( \mathcal P_{ext}\)) and intensional (\( \mathcal P_{int}\)) ones. A term is a variable or constant. Extensional (resp. intensional) Atoms have the form \(p(t_1,...,t_n)\), where \( t_i \) is a term and \(p \in \mathcal P_{ext}\) (resp. \(p \in \mathcal P_{int}\)). A ground atom is a variable free atom. A literal is either an atom or a negated extensional atom, \(\lnot p(t_1,...,t_n)\). Note that negative intensional atoms cannot form literals. A substitution \( \theta \) is a set of expressions of the form \( X \longleftarrow c \), where \( X \in \mathcal X\) and \( c \in \mathcal C\). Given a substitution \( \theta \), an atom \( a\theta \) is obtained from atom a by replacing its variables with constants according to \( \theta \).
Intensional predicate symbols are defined by rules. A rule r, shown as \( head(r) \leftarrow b_1 \wedge \dots \wedge b_n \), consists of an intensional atom head(r) in the head and a conditional body, a (possibly empty) conjunction of literals \( b_1,\dots ,b_n \), where \( b_i \in body(r) \). A ground instance of a rule, \(r\theta \), is any rule obtained from r by a substitution of head(r) and body(r) with ground atoms \( head(r)\theta \) and \( body(r)\theta \) respectively. Given a set of literals \(\mathbf S\) and a ground rule \( r\theta \), the rule is true in \(\mathbf S\) if either \(head(r)\theta \in \mathbf S\) or \( body(r)\theta \not \subseteq \mathbf S\). A (possibly non-ground) rule is true in \(\mathbf S\) if all of its ground instances are true in \(\mathbf S\). A set \(\mathbf S\) of literals is consistent if there is no atom, a, such that \(\{a,\lnot a\} \subseteq \mathbf S\).
Definition 1
(State). Given a set of rules \( \mathbb R\), a consistent set \(\mathbf S\) of literals is called a state if and only if
-
1.
For each ground extensional atom a, either, \(a \in \mathbf S\), or \(\lnot a \in \mathbf S\).
-
2.
Every rule of \(\mathbb R\) is true in \(\mathbf S\).
Definition 2
( STRIPS action). A \(\textit{STRIPS}\) action \( \alpha = \langle p_\alpha (X_1,...,X_n),\) \( Pre(\alpha ) , E(\alpha ) \rangle \) consists of an intensional atom \(p_\alpha (X_1,...,X_n)\) in which \(p_\alpha \in \mathcal P_{int}\) is a predicate that is reserved to represent the action \(\alpha \) and can be used for no other purpose, a set of literals \(Pre(\alpha )\), called the precondition of \(\alpha \), and a consistent set of extensional literals \(E(\alpha )\), called the effect of \(\alpha \). The variables in \(Pre(\alpha )\) and \(E(\alpha )\) must occur in \(\{X_1,...,X_n\}\).
Note that the literals in \(Pre(\alpha )\) can be both extensional and intensional, while the literals in \(E(\alpha )\) can be extensional only.
Definition 3
(Execution of a STRIPS action). A \(\textit{STRIPS}\) action \(\alpha \) is executable in a state \(\mathbf S\) if there is a substitution \(\theta \) such that \(\theta (Pre(\alpha )) \subseteq \mathbf S\). A result of the execution (with respect to \(\theta \)) is the state \(\mathbf S'\) such that \(\mathbf S' = (\mathbf S\setminus \lnot \theta (E(\alpha ))) \cup \theta (E(\alpha ))\), where \(\lnot E= \{ \lnot \ell \vert \ell \in E \}\).
Note that \(\mathbf S\) is well-defined since \(E(\alpha )\) is consistent. Observe also that, if \(\alpha \) has variables, the result of an execution, \(\mathbf S\), may depend on the chosen substitution \(\theta \).
Definition 4
(Planning problem). Given a set of rules \(\mathbb R\), a set of \(\textit{STRIPS}\) actions \( \mathbb A\), a set of literals G, called the goal, and an initial state \(\mathbf S\), a planning solution (or simply a plan) for the planning \( \varPi = \langle \mathbb R, \mathbb A, G, \mathbf S\rangle \) is a sequence of ground actions \(\sigma = \alpha _1,\dots , \alpha _n\) such that for each \( 1 \le i \le n \);
-
there is a substitution \( \theta _i\) and a \( \textit{STRIPS}\) action \( \alpha '_{i} \in \mathbb A\) such that \( \alpha '_{i}\theta = \alpha _{i} \); and
-
there is a sequence of states \(\mathbf S_0,\mathbf S_1, \dots , \mathbf S_n\) such that
-
\(\mathbf S= \mathbf S_0\) and \(G \subseteq \mathbf S_n\) (i.e., G is satisfied in the final state);
-
\(\alpha _i\) is executable in state \(\mathbf S_{i-1}\) and the result of that execution is the state \(\mathbf S_i\).
The following definition of goal serializable planning problems constitutes a measure that recognizing planning problems, for which the \( \textit{STRIPS}\) planning technique is proven to be complete.
Definition 5
(Goal serializable planning problem). Given a planning problem \( \varPi = \langle \mathbb R, \mathbb A, \mathbf S,G \rangle \), let \( \sigma \) be the shortest solution plan for \( \varPi \) and \( G' \subset G \) be any arbitrary set of literals such that \( G \ne G' \). We call \( \varPi \) a goal serializable planning problem if and only if, for every \( \sigma ' \), that is a planning solution for \( \varPi ' = \langle \mathbb R, \mathbb A, G', \mathbf S\rangle \) and the result of its execution is \( \mathbf S' \) where \( \vert \sigma ' \vert \le \vert \sigma \vert \), there is a planning solution \( \sigma '' \) for \( \varPi '' = \langle \mathbb R, \mathbb A, G, \mathbf S' \rangle \) such that \( \vert \sigma '' \vert < \vert \sigma \vert \).
A brief introduction to the subset of \( \mathcal {TR} \) [8–11] has been appeared in [12–14]. Although such introduction is required to make our paper self-contained, we omit that introduction to save space and refer the reader to [14].
3 The \(\mathcal {TR}\) Planners
The informal idea of using \(\mathcal {TR}\) as a planning formalism and an encoding of \(\textit{STRIPS}\) and naive planning as a set of \(\mathcal {TR}\) rules first appeared in an unpublished report [8]. We extend and slightly modify the original methods to prove different properties of each planning technique.
Given a set of extensional literals G, we define \(\textit{Enf}(G)\) to be the set of elementary updates that makes G true. Next we introduce a natural correspondence between \(\textit{STRIPS}\) actions and \(\mathcal {TR}\) rules.
Definition 6
(Actions as \(\mathcal {TR}\) rules). Let \( \alpha = \langle p_\alpha (\overline{X}), Pre(\alpha ), E(\alpha ) \rangle \) be a \(\textit{STRIPS}\) action. We define its corresponding TR rule, \(tr(\alpha )\), to be a rule of the form
Note that in (1) the actual order of action execution in the last component, \(\otimes _{u\in \textit{Enf}(E(\alpha ))}u\), is immaterial, since all such executions happen to lead to the same state.
We now define a set of \(\mathcal {TR}\) clauses that simulate naive and \(\textit{STRIPS}\) [7] planning techniques. Moreover, for convenience, we use \( a\,\widehat{ \otimes }\,b \) as a shorthand for \( a \otimes b \vee b \otimes a \). This connective is called the shuffle operator in [8]. We define it to be commutative and associative and thus extend it to arbitrary number of operands.
Definition 7
(Naïve planning rules). Given a \( \textit{STRIPS}\) planning problem \(\varPi =\langle \mathbb R,\mathbb A,G,\mathbf S\rangle \) (see Definition 4), we define a set of \(\mathcal {TR}\) rules, \(\mathbb P(\varPi )\), which simulate naive planning technique to provide a planning solution to the planning problem. \(\mathbb P(\varPi )\) has two parts, \(\mathbb P_{general}\), \(\mathbb P_\mathbb A\), described below.
-
The \(\mathbb P_{general}\) part: contains a couple of rules as follows;
$$\begin{aligned} \begin{array}{l} plan \leftarrow . \\ plan \leftarrow execute\_action \otimes plan. \end{array} \end{aligned}$$(2)These rules construct a sequence of actions and bind them to the plan.
-
The \(\mathbb P_{actions}\) part: for each \(\alpha \in \mathbb A\), \(\mathbb P_{actions}\) has a couple of rules as follows;
$$\begin{aligned} \begin{array}{l} p_\alpha (\overline{X}) \leftarrow (\wedge _{\ell \in Pre(\alpha )}\ell ) ~ \otimes ~ (\otimes _{u\in \textit{Enf}(E(\alpha ))}u) . \\ execute\_action \leftarrow p_\alpha (\overline{X}). \end{array} \end{aligned}$$(3)This is the \(\mathcal {TR}\) rule that corresponds to the action \(\alpha \), introduced in Definition 6 and generally links an action to a plan.
Definition 8
( STRIPS planning rules). Let \(\varPi =\langle \mathbb R,\mathbb A,G,\mathbf S\rangle \) be a \(\textit{STRIPS}\) planning problem (see Definition 4). We define a set of \(\mathcal {TR}\) rules, \(\mathbb P(\varPi )\), which simulate \(\textit{STRIPS}\) planning technique to provide a planning solution to the planning problem. \(\mathbb P(\varPi )\) has three disjoint parts, \(\mathbb P_\mathbb R\), \(\mathbb P_\mathbb A\), and \(\mathbb P_G\), described below.
-
The \(\mathbb P_\mathbb R\) part: for each rule \(p(\overline{X}) \leftarrow p_1(\overline{X}_1) \wedge \dots \wedge p_k(\overline{X}_n)\) in \(\mathbb R\), \(\mathbb P_\mathbb R\) has a rule of the form
$$\begin{aligned} achieve\_p(\overline{X}) \leftarrow \widehat{ \otimes }_{i = 1}^{n} achieve\_p_i(\overline{X}_i) . \end{aligned}$$(4)Rule (4) is an extension to the classical \(\textit{STRIPS}\) planning algorithm. It captures intentional predicates and ramification of actions, and it is the only major aspect of our \(\mathcal {TR}\)-based rendering of \(\textit{STRIPS}\) that was not present in the original in one way or another.
-
The part \(\mathbb P_\mathbb A= \mathbb P_{actions} \cup \mathbb P_{atoms} \cup \mathbb P_{achieves}\) is constructed out of the actions in \(\mathbb A\) as follows:
-
\(\mathbb P_{actions}\): similar to Definition 7.
-
\(\mathbb P_{atoms} = \mathbb P_{achieved} \cup \mathbb P_{enforced}\) has two disjoint parts as follows:
-
\(\mathbb P_{achieved}\): for each extensional predicate \(p\in \mathcal P_{ext}\), \(\mathbb P_{achieved}\) has the rules
$$\begin{aligned} \begin{array}{l} achieve\_p(\overline{X}) \leftarrow p(\overline{X}) .\\ achieve\_not\_p(\overline{X}) \leftarrow \lnot p(\overline{X}) .\\ \end{array} \end{aligned}$$(5)These rules say that if an extensional literal is true in a state then that literal has already been achieved as a goal.
-
\(\mathbb P_{enforced}\): for each action \(\alpha =\langle p_\alpha (\overline{X}),Pre(\alpha ), E(\alpha )\rangle \) in \(\mathbb A\) and each \(e(\overline{Y})\in E(\alpha )\), \(\mathbb P_{enforced}\) has the following rule:
$$\begin{aligned} achieve\_e(\overline{Y}) \leftarrow \lnot e(\overline{Y}) \otimes execute\_p_\alpha (\overline{X}) . \end{aligned}$$(6)This rule says that one way to achieve a goal that occurs in the effects of an action is to execute that action.
-
\(\mathbb P_{achieves}\): for each action \(\alpha =\langle p_\alpha (\overline{X}),Pre(\alpha ), E(\alpha )\rangle \) in \(\mathbb A\), \(\mathbb P_{achieves}\) has the following rule:
$$\begin{aligned} execute\_p_\alpha (\overline{X}) \leftarrow (\widehat{ \otimes }_{\ell \in Pre(\alpha )} achieve\_\ell ) \otimes p_\alpha (\overline{X}). \end{aligned}$$(7)This means that to execute an action, one must first achieve the precondition of the action and then perform the state changes prescribed by the action.
-
\(\mathbb P_G\): Let \(G=\{g_1,...,g_k\}\). Then \(\mathbb P_G\) has a rule of the form:
$$\begin{aligned} achieve_G \leftarrow (\widehat{ \otimes }_{g_i = 1}^k achieve\_g_i) \otimes (\wedge _{i=1}^k g_i) . \end{aligned}$$(8)
Given a \( \textit{STRIPS}\) planning problem \(\varPi =\langle \mathbb R,\mathbb A,G,\mathbf S\rangle \), each of Definitions 7 and 8 gives a set of \(\mathcal {TR}\) rules that specifies the corresponding planning strategy for that problem. To find a solution for that planning problem, one simply needs to place the request (9) (resp. (10)) in the initial state and use the set of rules from Definition 7 (resp. Definition 8) and the \(\mathcal {TR}\)’s inference system to find a proof.
Completeness of a planning strategy means that, for any \(\textit{STRIPS}\) planning problem, if there is a solution, the planner will find at least one plan.
Theorem 1
(Completeness of naive planning). If there is a plan that achieves the goal G from the initial state \( \mathbf D_0 \) then the \(\mathcal {TR}\)-based naive planner will find a plan.
Proof
(Sketch). The proof is a direct consequence of \( \mathcal {TR} \) inference system completeness.
Theorem 2
(Completeness of STRIPS planning). Given a goal serializable planning problem \(\varPi =\langle \mathbb R,\mathbb A, G,\mathbf D_0\rangle \), if there is a plan that achieves the goal G from the initial state \( \mathbf D_0 \) then the \(\mathcal {TR}\)-based \(\textit{STRIPS}\) planner will find a plan.
Proof
(Sketch). By induction on the length of the plan. The full proof can be found in the full report.Footnote 3
4 Conclusion
This paper has demonstrated that the use of Transaction Logic opens up new possibilities for generalizations and considerations of the properties of existing planning techniques. For instance, we have shown that once the \(\textit{STRIPS}\) algorithm is cast as a set of rules in \(\mathcal {TR}\), the different properties of the framework can be studied, almost for free, to recognize and define such advanced concepts as goal serializability of planning. The concept of serializability, not only classifies planning problem regarding to the completeness of \( \textit{STRIPS}\) planning technique, but also establishes further explorations in different areas such as algorithms and graph theory.
Notes
- 1.
Due to its simple nature.
- 2.
As it was originally proposed by [7] in \( \textit{STRIPS}\).
- 3.
References
Sacerdoti, E.D.: The nonlinear nature of plans. In: Proceedings of the 4th International Joint Conference on Artificial Intelligence, IJCAI 1975, vol. 1, pp. 206–214. Morgan Kaufmann Publishers Inc., San Francisco (1975)
Bibel, W.: A deductive solution for plan generation. In: Schmidt, J.W., Thanos, C. (eds.) Foundations of Knowledge Base Management. Topics in Information Systems, pp. 453–473. Springer, Heidelberg (1989)
Kahramanoğulları, O.: On linear logic planning and concurrency. In: Martín-Vide, C., Otto, F., Fernau, H. (eds.) LATA 2008. LNCS, vol. 5196, pp. 250–262. Springer, Heidelberg (2008). doi:10.1007/978-3-540-88282-4_24
Cresswell, S., Smaill, A., Richardson, J.: Deductive synthesis of recursive plans in linear logic. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS (LNAI), vol. 1809, pp. 252–264. Springer, Heidelberg (2000). doi:10.1007/10720246_20
Guglielmi, A.: Concurrency and plan generation in a logic programming language with a sequential operator. In: Hentenryck, P.V. (ed.) ICLP, pp. 240–254. MIT Press (1994)
Kahramanogullari, O.: Towards planning as concurrency. In: Hamza, M.H. (ed.) Artificial Intelligence and Applications, pp. 387–393. IASTED/ACTA Press (2005)
Fikes, R.E., Nilsson, N.J.: STRIPS: a new approach to the application of theorem proving to problem solving. Artif. Intell. 2, 189–208 (1971)
Bonner, A., Kifer, M.: Transaction logic programming (or a logic of declarative and procedural knowledge). Technical report CSRI-323, University of Toronto, November 1995. http://www.cs.toronto.edu/~bonner/transaction-logic.html
Bonner, A., Kifer, M.: A logic for programming database transactions. In: Chomicki, J., Saake, G. (eds.) Logics for Databases and Information Systems, pp. 117–166. Kluwer Academic Publishers, March 1998
Bonner, A.J., Kifer, M.: An overview of transaction logic. Theoret. Comput. Sci. 133(32), 205–265 (1994)
Bonner, A., Kifer, M.: Transaction logic programming. In: International Conference on Logic Programming, Budapest, Hungary, pp. 257–282. MIT Press, June 1993
Basseda, R., Kifer, M., Bonner, A.J.: Planning with transaction logic. In: Kontchakov, R., Mugnier, M.-L. (eds.) RR 2014. LNCS, vol. 8741, pp. 29–44. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11113-1_3
Basseda, R., Kifer, M.: Planning with regression analysis in transaction logic. In: Cate, B., Mileo, A. (eds.) RR 2015. LNCS, vol. 9209, pp. 45–60. Springer, Heidelberg (2015). doi:10.1007/978-3-319-22002-4_5
Basseda, R., Kifer, M.: State space planning using transaction logic. In: Pontelli, E., Son, T.C. (eds.) PADL 2015. LNCS, vol. 9131, pp. 17–33. Springer, Heidelberg (2015). doi:10.1007/978-3-319-19686-2_2
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Basseda, R., Kifer, M. (2016). Formalizing Goal Serializability for Evaluation of Planning Features. In: Michael, L., Kakas, A. (eds) Logics in Artificial Intelligence. JELIA 2016. Lecture Notes in Computer Science(), vol 10021. Springer, Cham. https://doi.org/10.1007/978-3-319-48758-8_33
Download citation
DOI: https://doi.org/10.1007/978-3-319-48758-8_33
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48757-1
Online ISBN: 978-3-319-48758-8
eBook Packages: Computer ScienceComputer Science (R0)