Non-monotonic Temporal Logics for Goal Specification

1 Introduction andMotivation

In specifying goals of agents [Bacchus and Kabanza, 1998; Niyogi and Sarkar, 2000; Baral et al., 2001; Baral and Zhao, 2004; 2006] many have used temporal logics such as linear temporal logic LTL, branching time temporal logics CTL∗ , π-CTL∗ , and their extensions. However, all these logics are monotonic. In specifying goals of agents, often there is a need of being able to specify goals non-monotonically. For example, initially, an agent may be given a goal of having p true through the trajectory while reaching s. Later, the agent may decide to weaken its goal so that in certain exceptional cases p does not have to be true. One way to do that would be for the agent to replace its original goal by a revised goal. Coming up with a completely new revised goal, or obtaining the revised goal by doing surgery on the original goal specification violate the principle of elaboration tolerance [McCarthy, J., 1988]. But if we use existing temporal logics, we do not have a choice. What we need is a goal specification language that allows us to update the goal specification by simply adding new statements to the original specification. Such a goal specification language would be non-monotonic.

Another motivation for having a non-monotonic goal specification language that allows easy updating through adding is that we may not want to give the agent a directive that is too specific, too complicated, and that takes into account all possible exceptions, from the very beginning. Besides we may not even know all the exceptions initially. A good non-monotonic goal specification language should allow us to specify a simple goal initially and should allow us to refine it by adding new exceptions.

Although non-monotonic versions of various modal logics [McDermott, 1982] have been proposed in the past, so far we have come across only two 1 [Fujiwara and Honiden, 1991; Saeki, 1987] non-monotonic versions of temporal logics. The first extends auto-epistemic logic with temporal operators and does not explore issues such as elaboration tolerant representation of exceptions and weak exceptions. The second has semantics issues that are mentioned in the first.

In this paper we start with developing a non-monotonic temporal logic based on the linear temporal logic LTL and then briefly mention non-monotonic versions of a branching time temporal logic. In designing our non-monotonic versions of temporal logics, we keep focus on our overall aim of having non-monotonic goal languages. So rather than follow the path of non-monotonic modal logics and auto-epistemic logic we focus on specific aspects of knowledge representation that need non-monotonicity and borrow some specific techniques that allow such non-monotonicity.

One of the important use of non-monotonicity is the ability to express normative statements such as "normally q's have the property p." This resonates well with our need of nonmonotonic goal languages as we may need to specify that "normally a state should satisfy the property p". Accompanying normative statements we have various kinds of exceptions. For example, consider the age old normative statement "birds normally fly". One kind of exception (called "strong exceptions") to such a statement is that "penguins are birds that do not fly". Another kind of exception, referred to as weak exceptions, is that "injured birds are weak exceptions to the normative statement about birds flying;" as for wounded birds we do not know whether they fly or not. There is a need of similar exceptions with respect to goal specifications. A normative goal specification may specify that "normally a state should satisfy the property p". Strong exceptions may be states that satisfy some specific conditions, while weak exceptions may be other states that satisfy some other specific conditions.

1 There are several other papers, such as [Giannotti et al., 1999; Stein and Morgenstern, 1994; MacNish and Fallside, 1990], which from their titles seem like dealing with non-monotonic temporal logics. However, they are not quite related.

To accommodate the above we introduce two special notations 2

• [r]φ
• [[r]]φ

The intuitive meaning of the first one is that normally φ holds in a state and the label r lists the weak exceptions. The intuitive meaning of the second one is that normally φ holds in a state and the label r lists the strong exceptions.

The role of r here is similar to the role of labeling defaults and normative statements when representing them in logic programming. There, often the label is used as a parameter with respect to the ab predicates.

Since the non-monotonicity in goal languages is not due to having incomplete knowledge about the states, but rather due to the specifier not quite precisely knowing what she wants, we do not use operators such as the negation as failure operator 'not' from logic programming. Here the issue is different from inferring or assuming negation by default.

On the other hand we borrow the idea behind program completion in logic programming to specify and interpret the conditions listed corresponding to the label r. Thus there may be a set of conditions written as

that specify the strong exception or weak exception conditions with respect to r. Given the above, the overall condition associated with r becomes ψ1 ∨ . . . ∨ ψk. One is allowed to add additional conditions. For example, if 〈r : ψk+1〉 is added to the above set then the overall condition associated with r becomes ψ1 ∨ . . . ∨ ψk ∨ ψk+1.

We now illustrate the above with respect to an example.

Example 1 Suppose initially we want to maintain p true while reaching for s. We know beforehand that our aim to maintain p is not strict; it is just that we do not know yet, under what conditions truth of p may not be necessary. After a while, we realize that when q is true we may not need to have p true.

The initial goal can be written in our language as 〈g : (✷[r]p)∧✸s〉. It says that we should maintain p while reaching s. If the strong exception r happens in some states, we may not need to maintain p in those states. The weak exception r is then specified as 〈r : q〉.

To informally illustrate how non-monotonicity is manifested in the above example, we first define when a language is monotonic.

Definition 1 A logic L together with a query language Q and entailment relation |= is monotonic if for all T , T ′ in L and t in Q, T |= t implies T ∪ T ′ |= t. ✷

With respect to Example 1 let T be {〈g : (✷[r]p) ∧✸s〉}, T ′ = {〈r : q〉}. Intuitively, T |= ✷p and T ∪T ′ is equivalent to ✷(p∨q)∧✸s in LTL; thus T ∪T ′ ̸|= ✷p. This illustrates the non-monotonicity of our proposed language. We now move to the formal definition of our language and its semantics.

2 Unlike traditional exceptions and weak exceptions, we want the specifier to have pre-decided control over whether a particular goal fragment could have a weak exception or an exception, but not both.

The rest of this paper is organized as follows: Since our first non-monotonic goal language N-LTL is based on LTL, we first give an overview of the temporal logic LTL. Then, in Section 3, we propose the syntax and semantics of a new language N-LTL, together with its properties. In Section 4, we study the relationship between N-LTL and logic programs. We then briefly discuss how one can use a similar approach to develop non-monotonic versions of other temporal logics such as CTL∗ .

2 Background: Goal Representation Using LTL

In this section, we summarize the linear temporal logic LTL and what it means for a sequence of actions to be a plan with respect to a goal in LTL. Syntactically, LTL formulas are made up of propositions, propositional connectives ∨, ∧, and ¬, and future temporal connectives ©, ✷, ✸ and U. We now formally define truth values of temporal formulas with respect to trajectories. A trajectory is an infinite sequence of states.

Definition 2 Let 〈p〉 be an atomic proposition, 〈f〉 an LTL formula.

Definition 3 Let σ given by s0, s1, . . . , sk, sk+1, . . . be a trajectory, p denote a propositional formula, sj (j ≥ 0) denote a state, and f and fis (i = 1, 2) denote LTL formulas.

• (sj, σ) |= p iff p is true in sj.
• (sj, σ) |= ¬f iff (sj, σ) ̸|= f.
• (sj, σ) |= f1 ∨ f2 iff (sj, σ) |= f1 or (sj, σ) |= f2.
• (sj, σ) |= f1 ∧ f2 iff (sj, σ) |= f1 and (sj, σ) |= f2.
• (sj, σ) |=©f iff (sj+1, σ) |= f.
• (sj, σ) |= ✷f iff (sk, σ) |= f, for all k ≥ j.
• (sj, σ) |= ✸f iff (sk, σ) |= f, for some k ≥ j.
• (sj, σ) |= f1 U f2 iff there exists k ≥ j such that (sk, σ) |= f2 and for all i, j ≤ i < k, (si, σ) |= f1. ✷

Often [Bacchus and Kabanza, 1998; Baral et al., 2001] planning with respect to LTL goals are formalized with the assumption that there is complete information about the initial state, and the actions are deterministic. Let Φ be a transition function that defines transitions between states due to actions. Φ(si, ak) = sj iff the action ak transits the agent from state si to state sj. Let s be a state designated as the initial state, and let a1, . . . , an be a sequence of deterministic actions whose effects are described by a domain description.

Since truth of LTL formulas are defined with respect to a reference state and a trajectory made up of an infinite sequence of states, to define the correctness of a plan consisting of a finite sequence of actions with respect to an initial state and an LTL goal, the finite sequence of states obtained by applying the plan to the initial state is appended with the last state infinitely.

The trajectory corresponding to s and a1, . . . , an is the sequence s0, s1, . . . , that satisfies the following conditions: s = s0, si+1 = Φ(si, ai+1), for 0 ≤ i ≤ n - 1, and sj+1 = sj, for j ≥ n.

Definition 4 (Plans with respect to LTL goals) The sequence of actions a1, . . . , an is a plan from the initial state s for the LTL goal f, if (s, σ) |= f, where σ is the trajectory corresponding to s and a1, . . . , an. ✷

The role of LTL in specifying planning goals has been well studied and examples of that can be found in [Bacchus and Kabanza, 1998; Niyogi and Sarkar, 2000; Baral et al., 2001].

3 N-LTL: ANon-monotonic Extension of LTL

In this section, we extend LTL to capture non-monotonic requirements in specifying a goal. We call the new language N-LTL which stands for non-monotonic LTL. We first define the syntax and semantics of the language.

3.1 Syntax

While designing the language we asked ourselves two questions.

• If syntactically the goal is one temporal formula, how can we revise it to have new goals by just adding to the original formula?
• How to refer to one part of a specification in another part of the specification?

For the first we borrow ideas from Reiter's approach to reason about actions [Reiter, 2001] where he compiles his specification to classical logic. While the classical logic part is monotonic, reasoning with respect to the specification language is non-monotonic and the non-monotonicity is achieved through the compilation process. For the second we borrow ideas from logic programming. Similar to a logic program consisting of a set of rules, we consider each N-LTL formula to be a set of rules and we use rule labels such as r in Example 1 to link these rules into one temporal formula.

Definition 5 Let {g}, R, and P be three disjoint sets of atoms. Let 〈r〉 be an atom in R, 〈p〉 be an atom in P, e ∈ {g} ∪ R. 〈f〉 is a formula defined below:

An N-LTL formula is a set of rules 〈e : f〉, Where e is the head, and f is the body of the rule 〈e : f〉. ✷

In an N-LTL formula, g is a special symbol that stands for the final goal formula. R is the set of labels to be used to define corresponding strong exceptions and weak exceptions. A formula f defines the conditions of atoms in R or the conditions of g. Intuitively, [〈r〉](〈f〉) means that normally f is true, with theweak exceptions denoted throughr. [[〈r〉]](〈f〉) means that normally f is true, with the strong exceptions denoted through r. The weak and strong exception conditions corresponding to r are defined through other rules.

Definition 6 (AtomDependency) Let 〈e1 : f1〉 be a rule in an N-LTL formula. If e2 ∈ R occurs in the body of 〈e1 : f1〉, then e2 depends on e1. The dependency relation is transitive. ✷

Definition 7 (Loop Free) An N-LTL formula is loop free if in the formula, no atom in R depends on itself. ✷

Example 2 The following formula

is not loop free as r1 depends on r2 and r2 depends on r1.

An N-LTL specification is a loop free N-LTL formula.

3.2 Semantics of N-LTL Specifications

As we mentioned earlier, we define the semantics of N-LTL specifications by following the approach taken by Reiter to reason about actions: we compile N-LTL specifications to LTL theories.

Definition 8 Given a loop-free N-LTL formula (i.e., an NLTL specification) T , we translate it to an LTL formula Tr(T) as follows:

1. Let 〈e : f1〉, 〈e : f2〉, · · · , 〈e : fn〉 be all the rules in T with e in the head, e ∈ {g}∪R. We construct a formula f1∨f2∨· · ·∨fn, and we call it E(e). We do this for any atom e if the set of rules with e in the head is not empty.
2. If atom a1 depends on atom a2, and E(a1) is defined, we replace any occurrence of [a1](f) in E(a2) with f ∨ E(a1). The revised formula is still called E(a2).
3. If atom a1 depends on atom a2, and E(a1) is defined, we replace any occurrence of [[a1]](f) in E(a2) with E(a1). The revised formula is still called E(a2).
4. We do Step 2 and Step 3 recursively until no atoms e depending on g while E(e) is not empty occurs in E(g).
5. Finally, in E(g), we replace all remaining [r](f) and [[r]](f) with f. The revised goal formula is Tr(T).

✷

Example 3 Let us consider the N-LTL formula T as follows:

According to the definition, we know initially E(g) = ✸[r1](p) ∧ [r3](q), E(r1) = [[r2]](v) ∨ ✷t, and E(r2) = s. By replacing the formulas according to the dependence relations, we have E(g) = ✸(p∨[[r2]](v)∨✷t)∧[r3 ](q) = ✸(p∨ s ∨✷t) ∧ [r3](q). There is no rules with r3 as the head. Thus E(g) = ✸(p∨s∨✷t)∧q. Further, T r(T ) = ✸(p∨s∨✷t)∧q.

Loop-free N-LTL formulas (also called N-LTL specification) have the following properties.

Proposition 1 Given an N-LTL specification T , Tr(T) is a well defined LTL formula.

Given this property, we can define when a plan satisfies an N-LTL goal.

Definition 9 Let T be an N-LTL specification. Given a state s, and a trajectory σ = s0, s1, · · · , sk, · · · , (s, σ) |= T in N-LTL if (s, σ) |= T r(T ) with respect to LTL. ✷

Definition 10 (Plans with respect to N-LTL goals) Let T be an N-LTL specification. A sequence of actions a1, · · · , an is a plan from the initial state s for the N-LTL goal T , if σ is the trajectory corresponding to s and a1, · · · , an, and (s, σ) |= T in N-LTL. ✷

N-LTL specifications that do not have any strong exceptions (but may have weak exceptions) always make the goal weaker by accepting more plans when adding new rules.

Proposition 2 For any N-LTL specification T and T ∪ T ′ , if P is a plan with respect to T which does not have any strong exceptions (but may have weak exceptions), then P is a plan with respect to T ∪ T ′ .

Temporal logics such as LTL have a different property when we consider an LTL goal formula to be a set of temporal formulas and add new formulas to an existing theory. If P is a plan with respect to an LTL goal T ∪ T ′ then P is also a plan with respect to T . In LTL, adding more formulas reduces (or at best leaves it unchanged) the set of plans satisfying it while in N-LTL that does not have strong exceptions, adding more rules enlarges the set of plans satisfying it (or at least leaves it unchanged). This is not the case when the N-LTL theory has strong exceptions.

Example 4 Consider the problem in Example 1. The initial N-LTL formula is the specification T given as:

According to the definition, since there are no rules with head r1, we have (sj, σ) |= T in N-LTL iff (sj, σ) |= ✷p ∧✸s in LTL.

Suppose we add T ′ , as given below, to it:

According to the definition, we know E(g) = (✷[r1](p))∧✸s and E(r1) = (q). Further revision makes E(g) = ✷(p ∨ q) ∧ ✸s. Thus, (sj, σ) |= (T ∪ T ′) in N-LTL iff (sj, σ) |= ✷(p ∨ q) ∧ ✸s in LTL.

We can check that any plan satisfies LTL formula ✷p ∧ ✸s also satisfies ✷(p ∨ q) ∧ ✸s. T does not have strong exceptions, and Proposition 2 holds here.

Now, let us define what do we mean when we say that NLTL is non-monotonic. LTL is monotonic since T |= t implies T ∪T ′ |= t where T and T ′ are two sets of LTL temporal formulas and t is an LTL temporal formula. We consider the following entailment in N-LTL.

Definition 11 (Entailment) T |= t if Tr(T) |= t, where T is an N-LTL specification and t is an LTL formula. ✷

Proposition 3 The entailment in Definition 11 is nonmonotonic.

Let us consider one example to illustrate the use of N-LTL.

Example 5 One professor asks his robot to make a photocopy of one document and fetch a cup of coffee. However, before the robot goes out the office, the professor finds out that the coffee is sold out. No plan can satisfy the goal given to the robot. The professor would now like to weaken the goal. Following are three possibilities:

1. He would be happy with a cup of tea instead;
2. He just needs the copy of the document and is willing to forget about the coffee;
3. The robot may come back to his officewith the document copied and go about looking for the coffee later.

If the professor was using N-LTL and from past experience knows that he may have to revise his goal, especially with respect to coffee, he can express his initial goal as:

It is equivalent to satisfying✸(coffee∧copy∧✸office) in LTL.

Later on, according to the new conditions and new alternatives, the professor may revise his original goal by adding one of the following three rules:

1. Adding the new rule 〈r : tea〉 which makes the overall goal equivalent to✸((coffee∨tea)∧copy∧✸office) in LTL;
2. Let ⊤ denote true and ⊥ denote false. Adding the new rule 〈r : ⊤〉 which makes the overall goal equivalent to ✸((coffee ∨ ⊤) ∧ copy ∧ ✸office) in LTL, which is equivalent to ✸(copy ∧ ✸off ice) in LTL;
3. Adding the new rule 〈r : ✸(coffee∧✸office)〉 which makes the overall goal equivalent to ✸(coffee∧copy∧ ✸of f ice)∨✸(copy∧✸of f ice∧✸(cof f ee∧✸of f ice)) in LTL. Now it allows the agent to get the document copied first before waiting for the coffee.

If we want to get tea instead of coffee, we should know initially that the sub-task of getting coffee can be replaced by a different goal. 3 Now, the initial formulation is

When we add a new goal 〈r : tea〉. The goal afterwards is equivalent to ✸(tea ∧ copy ∧ ✸off ice) in LTL.

Note that "copy" must be satisfied in this domain as the professor does not want to weaken this condition. While the robot is on its way of getting things done, some other exceptions may happen. With N-LTL, we may further refine part of the goal.

Note that if a rule in the formula has a substring [[r1]](f), then removing rules 〈r1 : ⊥〉 may affect the semantics of the formula. If there is no substring [[r1]](f) in any part of the formula, then we can remove rules〈r1 : ⊥〉 without affecting the semantics of the formula.

3 We made this design decision consciously. Thus unlike in logic programming where the same default may have strong exceptions and weak exceptions, here we empower the initial goal specifier to make that decision beforehand.

3.3 Complexity of N-LTL

The complexity of various problems (planning etc.) with respect to N-LTL specifications is at the same level of the polynomial hierarchy as with respect to LTL specifications. This is because, the loop-free criteria and the fact that there are polynomial number of special symbols like [r] and [[r]] ensure that an N-LTL specification can be converted to an LTL specification in polynomial time and the increase in size is also polynomial.

4 Relation to Logic Programs

We now consider the relation between N-LTL goals and logic programs, especially with respect to planning. Use of temporal domain knowledge in planning was first proposed in [Bacchus and Kabanza, 1998]. Planning with temporal logic LTL has also been studied in [Neljanko and Niemel¨a, 2001; Son et al., 2002]. In this section, we translate a domain description and a goal specified in N-LTL to a logic program. We consider the relations of stable models of the translated programs and the original planning problems. In the following translation, for i ̸= j, even if si and sj in the trajectory are referring to the same state, we assign them different labels.

Definition 12 Let σ given by s0, s1, · · · , sk, · · · be a trajectory, p denote an atom, sj denote a state, f , f1, and f2 denote LTL formulas that also take elements in R as atoms. We now define an encoding of σ, called encoding(σ, T), where T is an N-LTL formula. The encoding consists of the following parts:

1. For any i such that 0 ≤ i, there is a rule

1. For any 0 ≤ i < j, there is a rule

1. If p is true in state s, there is a rule

where si is the ith state in the trajectory and it corresponds to the state s.

1. The following rules corresponding to ¬, ∨, and ∧ are in the program

1. The following rules corresponding to temporal operators ©, ✸, and ✷ are in the program:

1. The following rules corresponding to the temporal operator U are in the program:

✷

Definition 13 We encode an N-LTL formula T into a logic program, denoted by LP (T ) as follows:

For each rule 〈e : f〉 in T , we create a list of the atoms from R (the set of rule labels) that occur in f. If one atom occurs multiple times in f , we include it as many times in the list. We now revise f to a set of new formulas simplify(f):

• For any atom rk in the list, if it is not in the head of any rule, then we replace all occurrences of [rk](fk) or [[rk]](fk) with fk;
• Otherwise, suppose the ith atom in the list is ej. If it occurs in the formula f as [[ej]](fj), then we replace this sub-formula [[ej]](fj) in f with ej.
• Suppose a list of atoms ei1, ei2, · · · , eil remain in formula f . We calculate a Cartesian product of l sets, where the sth set is {eis, fis} and the sth atom eis occurs in the formula f as [eis](fis). We replace each occurrence [eis](fis) by either eis or fis according to its value in one element of the Cartesian product. Thus we have 2l different combinations. We consider each combination as one instance of simplify(f), the revised formula of f .

We then add the rule

Example 6 Suppose one rule in an N-LTL goal T is as follows:

There are rules in T with the head r1 and also rules with the head r2. There are no rules in T with the head r3. We need to add the following 4 rules into LP(T ):

Note that in the translated program, we have an atom holds(s, f ∧ r2 ∧ r1 ∧ t). r1 and r2 are not atoms in the transition system. They are defined by other rules.

Example 7 Consider the N-LTL goal as follows:

It is known that this formula is equivalent to the LTL formula h ∨ ✸(h ∨ ✷t ∨ f ). We have the following rules in LP (T ):

Consider a trajectory σ = s0, s1, s1, · · · , s1, · · · where only t is true in state s1. No fluent is true in state s0. In the program encoding(σ, T), we know holds(s2,✷t) is true in all its stable models. Thus we have holds(s2, r1) in all stable models of encoding(σ, T) ∪ LP(T). Further, according to Item 5 in Definition 12, since there is a rule holds(s0,✸r1) ← holds(s0, r1), future(s0, s1). we know holds(s1,✸r1). Thus holds(s0, g) is true in all stable models of the program.

Proposition 4 Given a trajectory σ = s0, s1, · · · , sn, · · · . Let T be an N-LTL specification. (s0, σ) |= T in N-LTL iff encoding(σ, T ) ∪ LP (T ) |= holds(s0, g).

5 Non-monotonic Extension of CTL∗ , π-CTL∗ , and P-CTL∗

Different from LTL, in CTL∗ [Emerson and Srinivasan, 1989; Emerson, 1990], π-CTL∗ [Baral and Zhao, 2004], and PCTL∗ [Baral and Zhao, 2006], formulas are categorized as state formulas and path formulas. As a consequence, the corresponding non-monotonic languages should be defined with respect to path formulas and state formulas respectively. We now define the way of extending the definition of nonmonotonic temporal logics for CTL∗ , called N-CTL∗. We base the language N-CTL∗ on CTL∗ .

We refer readers to [Emerson and Srinivasan, 1989; Emerson, 1990] for the syntax and semantics of CTL∗ . There are two kinds of formulas in CTL∗ : state formulas and path formulas. Normally state formulas are properties of states while path formulas are properties of paths. Recall that the symbols A and E are the branching time operators meaning 'for all paths' and 'there exists a path' respectively.

Definition 14 Let {g}, Rpf , Rsf and P be four disjoint sets of atoms. Let 〈rpf 〉 be an atom in Rpf , 〈rsf 〉 be an atom in Rsf , 〈p〉 be an atom in P , e ∈ {g} ∪ Rsf . Let 〈sf〉 denote a state formula, and 〈pf〉 denote a path formula.

AnN-CTL∗ formula is a set of rules 〈e : sf〉, or 〈rpf : pf〉. Each of e or rpf is the head of the rule, and each of sf or pf is the body of the rule 〈e : sf〉 or 〈rpf : pf〉. ✷

The semantics of N-CTL∗ is defined in a way similar to the definition of the semantics of N-LTL. We now illustrate the usefulness of N-CTL∗ through two examples.

Example 8 The initial goal is to require that p be true until q is reached. However, it is realized that in some domain, this goal is too strong as no plan can always have p until reaching q. If in some states in the main path, all possible trajectories will have p true in the future, then we may consider it as a strong exception and may allow not to have p. The initial goal can be represented as 〈g : [r](p)Uq〉 in N-CTL∗ . This goal is equivalent to pUq in CTL∗ . It can be further refined by adding one rule about the weak exception r as 〈r : A✸p〉. The revised goal is equivalent to (p∨A✸p)Uq, which is equivalent to (A✸p)Uq.

Example 9 Initially, the goal is tomake sure that inmost trajectories starting from the initial state, ✸p is true. However, later on, we may require that once ✸q is satisfied by some trajectories, those trajectories are considered as exceptional ones and we do not require them to satisfy ✸p. The initial goal is represented as: 〈g : A[r](✸p)〉. Later, the goal can be weakened by adding the weak exception rule 〈r : (✸q)〉.

The initial goal is equivalent to the CTL∗ formula A✸p and the revised goal is equivalent to A(✸p ∨ ✸q).

6 Conclusion and Future Work

In this paper, we proposed a non-monotonic temporal logic based on LTL and hinted at a branching time non-monotonic temporal logic based on CTL∗ . We motivated the need for such non-monotonic temporal logics from the point of view of needing ways to express goals that can be changed in an elaboration tolerant manner. We presented several properties of our non-monotonic goal language N-LTL and briefly discussed its encoding using logic programming.

One possible controversial design decision that we made is to empower the specifier to decide whether weak exceptions or strong exceptions are allowed. This is in contrast to use of defaults in standard non-monotonic logics where the normative statement itself does not refer to strong exception or weak-exception, but rather they are added separately. Further study to compare the two approaches is an immediate future work.

7 Acknowledgement

This work was supported by a contract from ARDA and NSF grant 0412000. We thank the anonymous reviewers for their comments, especially for pointing us to the earlier work [Fujiwara and Honiden, 1991].