Temporal Action Logics (TAL) is an expressive class of nonmonotonic temporal logics for reasoning about action and change. In previous work, it has been shown that a very general fragment of the logic can be reduced to firstorder logic with equality. Consequently, standard theorem proving techniques can be used to reason in TAL. TAL is intended to be used for robotics. In this case, standard theorem proving techniques are too general and do not provide efficient decision procedures. The goal of this article is to identify a limited subset of TAL that can be directly mapped to a normal logic program. Although quite restrictive, this sets the lower bound on what can be done with direct mappings to logic programs. Discussions concerning extensions to the restricted fragment are also provided.
Temporal Action Logics (TAL) [
The generality of TAL is useful in other domains as a natural semantic
specification language. For instance, it provides a formal specification of TALplanner.
TALplanner5 [
In this paper, the focus is on isolating a restricted fragment of TAL and showing that it can be encoded in a sound manner into normal logic programs. Unfortunately, the fragment for which this works is highly restrictive. The subset of TAL narratives with deterministic single step actions and complete information about initial state can be encoded soundly into logic programs. This in fact makes sense, since any nondeterminism in TAL narratives must be excluded from such a direct mapping. Relaxing the single step constraint and complete information at initial state both result in introducing non-determinism and thus multiple minimal models. This, in fact, would apply to any alternative action formalism.
The systematic use of logic programming as a basis for soundly implementing
fragments of action formalisms was introduced in the case of the Situation Calculus by
Reiter (see [
An algorithm is developed for the systematic translation of definitional theories of TAL into logic programs. The definitional fragment of TAL identified is called TALM. It is then shown that extending this fragment via the use of direct encodings into normal logic programs is not feasible. Any attempt to generalize the TALM fragment results in the introduction of non-determinism into the fragment. The main limitation here is the inability to encode a unique values axiom for features in TAL narratives. This immediately rules out non-deterministic actions, actions with duration and an incomplete initial state.
The rest of this paper is organised as follows: In Section 2 we introduce the basic concepts of TAL, in Section 3 we develop an algorithm to translate definitional theories into logic programs, in Section 4 we reformulate a constrained TAL theory, TALM, as a definitional theory, and finally in Section 5 we discuss the limitations of the translation. 2
Due to lack of space, we refer the reader to [
In TAL, a scenario (or narrative) can be described in a compact surface language
L(ND), which is a high-level macro expandable language consisting of action type
specifications (acs), dependency constraints (dep), domain constraints (dom),
persistence statements (per), observation statements (obs), and action occurrence statements
5 http://www.ida.liu.se/divisions/aiics/aiicssite/projects/talplanner.en.shtml
6 http://www.ida.liu.se/divisions/aiics/aiicssite/index.en.shtml
(occ). To make sure that fluents will not be persistent when they are changed by an
action, the reassignment macro R can be used. R([t2] ) ensures that will hold at the
time point t2. Consider the following scenario due to Reiter [
Example 1 (Simple robot specification). There is one robot called rob and there are two objects, namely a ball and a vase. A robot can only pick up an object if he is not holding anything and if he is next to the object, and he can only drop an object if he is holding it. When a robot drops an object it will fall on the floor. Initially, rob is next to vase and not next to ball. Rob is not holding anything. First, rob picks up vase, after which he walks to ball and drops vase. The narrative specification of this example in the macro language L(ND) is: acs1 [t1; t2] pickup(r; o) ; acs2 [t1; t2] walk(r; o) ; acs3 [t1; t2] drop(r; o) ; [t1] 8o1 [:holding(r; o1)] ^ nextto(r; o) !
R([t2] holding(r; o) ^ :onfloor(o)) R([t2] nextto(r; o)) ^ 8o1 [o 6= o1 ! R([t2] :nextto(r; o1))] [t1] holding(r; o) ! R([t2] :holding(r; o) ^ onfloor(o)) obs1 [0] nextto(rob; vase) ^ :nextto(rob; ball) obs2 [0] 8z:holding(rob; z) obs3 [0] onfloor(vase) ^ onfloor(ball) occ1 [0; 1] pickup(rob; vase) occ2 [1; 2] walk(rob; ball) occ3 [3; 4] drop(rob; vase)
Reasoning about a narrative in L(ND) is done by translating it into the base
language L(FL)), which is an order-sorted classical first-order language using a linear,
discrete time structure. The language uses the ternary predicates H olds and Occurs,
and the binary predicate Occlude. The translation from L(ND) to L(FL) is given by the
function T rans [
Consider any narrative N and let Nper; Nobs; Nocc; Nacs; Ndomc; and Ndepc denote the sets of persistence statements, observation statements, action occurrence statements, action type specifications, domain constraints, and dependency constraints in N respectively. The TAL domain description (referred to as preferred narrative) N is given by CIRC[ occ; Occurs] ^ CIRC[ depc ^ acs; Occlude] ^ fnd ^ time ^ per ^ obs ^ domc; where per; obs; occ; acs; domc; and depc are the formulas in L(FL) (first-order logic formulas) obtained by applying T rans on N ; Nobs; Nocc; Nacs; Ndomc; and Ndepc respectively; fnd is the set of foundational axioms in L(FL), containing unique name axioms, unique value axioms, etc., and time is the axiomatization of the particular temporal structure used in TAL.
By proposition 18.2 in [
Example 2 (Robot Specification, Ctd.). The following is a representation of acs1 in the language L(FL): acs1’ Occurs(t1; t2; pickup(r; o)) !
The circumscription of the Occurs predicate in the action occurrences (occ1, occ2, and occ2) above is equivalent to the following first-order formula:
Occurs(t1; t2; a) $(t1 = 0 ^ t2 = 1 ^ a = pickup(rob; vase))_ (t1 = 1 ^ t2 = 2 ^ a = walk(rob; ball))_ (t1 = 2 ^ t2 = 3 ^ a = drop(rob; vase))
The circumscription of the Occlude predicate in the action specifications (acs1, acs2, and acs3) above is equivalent to the following set of first-order formulas:
o = vase ^ 8o1 [:Holds(0; holding(r; o1); true)]^
t 2 Occlude(t; nextto(rob; o)) $ o = ball ^ t = 2
o = vase ^ (t = 1 ^ 8o1 [:Holds(0; holding(rob; o1); true)]^
Holds(0; nextto(rob; o); true) _ t = 3 ^ Holds(2; holding(rob; o); true) 3
def2P Algorithm: From Definitional Theories to Logic Programs We begin by providing some background definitions and techniques for the sake of completeness. Although these techniques are well-known by now, we state them here for completeness and readability of the paper. 3.1
The most widely accepted declarative semantics for negation as failure is the
“completed database” introduced by Clark [
A
L1; : : : ; Lm where A is an atom and L1; : : : ; Lm are literals. To avoid tedious repetition we shall assume that all programs referred to are normal. Similarly goals and queries will be assumed to be normal, i.e. of the forms L1; : : : ; Lm, and ? L1; : : : ; Lm, respectively.
Norms logic programs generally does not use classical negation, but negation as
failure. This means exactly what it says: if some fact cannot be derived from the theory
(i.e. it fails), then we assume that the negation of this fact can be derived from the
theory (i.e. it succeeds). One of the most widely applicable and often used semantics for
negation as failure was given by Clark [
Although Clark’s theorem assumes that a Prolog program P can be obtained from the theory T by writing the if-halves, it does not give any details on how this is done. Because Prolog only uses disjunctions and conjunctions as connectives, we will translate the other connectives (implication, bi-implication and quantifiers) into a form such that it is amenable for a Prolog interpreter. The same can be said for the query goals.
The Lloyd-Topor transformations [
(W2 ! W1)). 6. lt((8x)W ) = lt(:(9x):W ). 7. lt((9x)W ) = lt(W ).
W2) ^ 8. lt(::W ) = lt(W ). 9. lt(:(W1 ^ W2)) = lt(:W1) ^ lt(:W2). 10. lt(:(W1 _ W2)) = lt(:W1) _ lt(:W2). 11. lt(:(W1 ! W2)) = lt(:(:W1 _ W2)). 12. lt(:(W1 W2)) = lt(:(W1 ! W2) ^
:(W2 ! W1))). 13. lt(:(8x)W ) = lt((9x):W ). 14. lt(:(9x)W ) = :lt(W ).
Clark’s theorem is not applicable to any Prolog interpreter, but only to proper Prolog
interpreters. Such an interpreter is one that evaluates a negative literal not A, using
negation as failure, and moreover, does so only when (at the time of evaluation) the
atom A is ground. When A is not ground, the interpreter may suspend its evaluation,
working on other literals until A does become ground, or it may abort its computation.
Either way, it never tries to fail on non-ground atoms, because this can result in unsound
behaviour [
every variable which occurs in it occurs in a positive literal of it; a program clause A L1; :::; Ln is allowed if every variable which occurs in it occurs in a positive literal of its body L1; :::; Ln and a program is allowed if all of its clauses are allowed.
The contents of the previous section can be summarized into a single algorithm that translates a definitional theory to a Prolog program.
Definition 2 (def2P algorithm). The def2P algorithm takes a definitional theory T as
input and output a Prolog program def2P(T ) by performing the following steps:
1. T is augmented with Clark’s Equality Axioms [
The following result follows directly from the previous discussion.
def2P(T ) is complete for the theory T . 4
We constrain TAL to integer and positive time, relational and inertial fluents, complete
initial state and deterministic, single-step and non-overlapping actions. Moreover, we
omit symbolic constants, dependency constraints and domain constraints. Finally we
assume a consistent narrative specification. Call this constrained formalism TALM.
7 For a more detailed discussion see [
Occurs(t1; t2; a):
Occlude: Circumscribing Occlude works in a similar way. The predicate Occlude
occurs only in the postcondition of dependency constraints and actions specification
formulas. Each member of acs and dep can be transformed syntactically into the
logically equivalent form 8t;f i(t; f ) ! Occlude(t; f ). Again, by proposition 18.2 in [
k 8t;f [ _ i=1 i(t; f )]
Occludes(t; f ) Holds: We obtain the definition of the Holds predicate using case distinctions. The following proposition simplifies the TALM narrative.
in TALM can be inferred from actions and can thus be removed from the narrative. Proof. Let be some narrative specification in TALM. Let 0 be the narrative with all observations at t > 0 removed. We have to show that and 0 have the same models, i.e. , 0. The truth value of Occurs and Occlude is equivalent for both narratives, because these predicates do not occur in the observations. This means that it suffices to show that j= Holds(t; f; v) , 0 j= Holds(t; f; v) for any time point t, fluent f and valuation v.
”)”: Suppose for some time point t, fluent f and valuation v 2 ftrue; falseg we have that j= Holds(t; f; v). We have to show that 0 j= Holds(t; f; v). Suppose that Holds(t; f; v) is not an observation, it follows now directly that 0 j= Holds(t; f; v), obs ^ (1) (2) because the only difference between and 0 are observations. Suppose to the contrary that Holds(t; f; v) is an observation. Now, if there is no action specification that implies Holds(t; f; v), then this observation follows from the persistence statement as well, otherwise it will be contradicting with it and the narrative is inconsistent. Therefore, the observation is redundant. On the other hand, if there is an action specification formula that implies Holds(t; f; v), then since the action specification formulas are unchanged in 0, it follows that 0 j= Holds(t; f; v).
”(”: Follows directly from the fact that 0 is a subset of , meaning that everything that is valid in 0 will be valid in .
Now, to obtain a definition for the Holds predicate, suppose some time point t, fluent f and value v.
– Suppose t = 0. The only formulas that can assign a value to the Holds predicate at t = 0 are observations, because at time point 0 no actions can occur since an action has a minimal duration of 1 and a minimal starting time of 0. Moreover, all fluents are assigned a value through the observations because TALM has a complete initial state. So, given that t = 0, – Suppose t > 0. We introduce a second case distinction on Occlude: Suppose :Occlude(t; f ). Using the persistence statement (see Definition (3)) we obtain 8vHolds(t; f; v) Holds(t 1; f; v). So, given that t > 0 and :Occlude(t; f ),
Holds(t 1; f; v) Suppose Occlude(t; f ). By Eq. (2) we obtain i(t; f ). Because actions are deterministic and non-overlapping, and because there will be no observations (Proposition 1) there will be a unique action specification formula that is now true and implies a single Holds statement for the fluent f . Using this we obtain Holds(t; f; v). This means that, given that t > 0 and Occlude(t; f ), ( i(t; f ) ^ v = vi) Theorem 2 (Completion of Holds). Formulas (3), (4) and (5) provide necessary and sufficient conditions for the predicate Holds:
" k # t = 0 ^ _ f = Pj (ui) ^ v = vi _
i=1 t > 0 ^ (:Occlude(t; f ) ^ Holds(t 1; f; v)_
Occlude(t; f ) ^ i(t; f ) ^ v = vi)
Holds(t; f; v) Proof. Formulas (3), (4) and (5) are the only formulas that make the Holds predicate true in a TALM narrative. We obtain the definition directly by putting these formulas in a disjunction and adding the conditions for each case.
Fortunately, it turns out that every definitional theory of a TALM narrative fall into the class of allowed programs of Definition 1. We show this in the following theorem. Theorem 3 (Allowed program). Suppose is a TALM narrative , which is translated into a definitional theory by using the equivalences above. Let P be the program that is obtained from this theory by applying Clark’s Theorem. P falls into the class of allowed programs. That is, every variable that occurs in a rule in P occurs in a positive literal of the body of the rule.
Proof. We have to show that each program clause in P is an allowed program clause.
Each clause corresponds to a predicate of the theory, which means that we will have
to consider Occurs, Occlude, and Holds. By definition, all literals occurring in the
definition of Occurs are positive [
The variables occurring in the negative literal are t and f , which both occur positively in the Holds predicate that directly follows it. Therefore, Holds is an allowed clause too, because all variables occurring in a negative literal occur in a positive literal in the body.
We will now demonstrate the translation of our running example. We invite the reader to download the application that was developed along with this paper called TALTranslator. This application can perform the transformation automatically and comes with a user-friendly GUI and several examples8.
Example 3 (Robot specification, continued). The definition of the Holds predicate for the fluent onfloor is (slightly simplified for readability):
t = 0 ^ v = true_ t > 0^ (o = vase ^ (t = 1 ^ 8o1 [Holds(0; holding(rob; o1); f alse)]^ Holds(0; nextto(rob; o); true) ^ v = false_ t = 3 ^ Holds(2; holding(rob; o); true) ^ v = true)_ :Occlude(t; onfloor(o)) ^ Holds(t 1; onfloor(o); v)) 8 Download from http://icr.uni.lu/marc/TALTranslator.rar Next, we input this definitional theory into the def2P algorithm (Def. 2). Since Prolog provides the equality axioms (step 1), we can directly apply the Lloyd-Topor transformations. What follows is the Prolog code for the fluent onfloor(o) (note that Prolog uses ”;” for disjunction): In the previous sections we have introduced a restricted fragment of TAL, which we referred to as TALM. We then showed how it can be translated into a logic program sound for the narrative in question.
In this section we will consider if, and to what extent the constraints on TALM can be relaxed while still being able to use direct mappings of TAL narratives into logic programs. We discuss non-deterministic actions, concurrent actions, actions with duration and an incomplete initial state. Almost all the restrictions that we will discuss (except for concurrent actions) have one property in common: relaxing each of them will result in a non-deterministic narrative. This means essentially that a narrative can have multiple interpretations.
The unique values axioms associated with the foundational axioms in TAL for any narrative are crucial when discussing non-deterministic narratives, because it rules out narratives in which a fluent has two values at the same time point. This implies that rather than modelling several alternative values for a fluent in one mode, several minimal models are required instead. The unique values axioms follow: 8t;f 9vHolds(t; f; v) 8t;f;v1;v2 [v1 6= v2 :(Holds(t; f; v1) ^ Holds(t; f; v2))] (7) (8) In the previous section we did not explicitly encode these axioms into the definitional theory, because each narrative in TALM is fully deterministic: it will have a unique model in which each fluent has exactly one value. Satisfaction of the axioms is implicit in the encoding of TALM narratives into a logic program.
each fluent has exactly one value per time point. has a unique model m in which Proof. We show that for each narrative in TALM, the interpretations of the predicates Holds, Occlude and Occurs are unique. Because these are the only predicates occurring in the narrative, it follows directly that the narrative has a unique model. Suppose some narrative , – For Occurs: The interpretation of Occurs is determined only by the action occurrences. This interpretation is unique because the assignments of the action occurrences are non-deterministic and non-overlapping. – For Occlude: Similar to Occurs. – For Holds: This follows directly from the case distinction used when constructing the definition of the Holds predicate (see Section 2). 5.1
Any relaxation of the restrictions on TAL narratives associated with TALM introduce one form or another of non-deterministic choices of fluent values at time points. This implies that in the general case, Theorem 4 no longer holds. For any relaxation of TALM to be sound relative to encoding into a logic program, the unique values axioms would have to become an explicit part of the the definitional theory. Unfortunately, this is not possible.
Observe that Equation 8 is equivalent to,
v1 6= v2 ! :Holds(t; f; v1) _ :Holds(t; f; v2); It is in general not possible to bring such a formula into a definitional form. To obtain a definition of a predicate P , we require a set of formulas of the form,
( 1 ! P ) ^ ::: ^ ( i ! P ); which can then be combined to ( 1 _ ::: _ i) ! P .
Unfortunately the unique values axiom does not provide us with such a construction, and we can also not transform it in a direct manner into one. This means that we cannot hope to express the unique values axiom and at the same time maintain a transformation to an equivalent definitional theory. Therefore, we generally cannot allow non-deterministic actions in TALM, because it will possibly lead to an inconsistent model in which a fluent has two values at one time point. This immediately rules out the possibility to extend TALM with any form of non-determinism, including nondeterministic actions, multi-step actions, and an incomplete initial state, because each of these extensions introduce a form of non-determinism into the theory. This is not surprising as it applies to most any approach to modelling action and change. 5.2
Much work in reasoning about action and change has been done under the assumption that there is a single agent performing sequences of non-overlapping actions. The use of explicit time points in TAL enables the direct specification of narratives where action execution intervals are partly or completely overlapping, whether those actions are performed by a single agent or by multiple agents. No special concurrency operators are required to do this.
Independent Concurrent Actions: Extending TALM with independent concurrent actions involving disjoint sets of features is unproblematic. Since the effects of the actions do not interfere with each other (i.e. two actions change the same fluent at the same time), the expected effects will take place. Such concurrent actions will not introduce multiple models. We omit the proof of this proposition because it is trivial. The consequence of this is that the unique value axioms can be omitted, which means that it is possible to extend TALM with independent concurrent actions.
Dependent Concurrent Actions: In the case where actions affecting the same fluents occur concurrently, concurrent actions that affect the value of the same fluent can never assign different values to this fluent, because this would lead to an inconsistent narrative. Otherwise, both actions assign the same value to the fluent. In either case, it is not necessary to add the unique values axioms to the theory because there are no multiple models introduced. Again, the proof of this is trivial and is omitted. Thus, concurrent actions are allowed as long they do not assign different values to the same fluent at the same time. Or in other words: concurrent actions that assign different values to the same fluent are not allowed. 6
The aim of this paper was to isolate a definitional fragment of the highly expressive
TAL formalism and show how it can be soundly encoded into a normal logic program.
This was done by defining the fragment TALM and providing an algorithm, def2P, that
encodes TAL narratives in this fragment into logic programs that can be shown to be
sound and complete relative to this particular fragment. One would of course like to
find more general reasoning techniques that relax some of the restrictions associated
with TALM narratives. At the very least, one would require a mapping to disjunctive
logic programs such as Answer Set Programs. Lee and Palla [
Marc van Zee is funded by the National Research Fund, Luxembourg.