AGM Revision of Beliefs about Action and Time

1 Introduction

Reasoning about the interplay between action and time is fundamental for the design and development of intelligent systems such as autonomous systems, robotic applications, and service agents [Wooldridge, 2000; Doherty et al., 2009]. Analyzing the behavior of such systems, which are often specified in terms of actions' pre- and post-conditions together with some (behavioral/temporal) constraints, is not only indispensable for checking system properties (e.g., safety and liveness), there are also various applications that require automatic reasoning about the interplay between actions and time. For example, a calendar agent assisting its user in managing her calendar needs to reason about the actions/activities scheduled in time to detect possible conflicts of activities.

On the one hand, reasoning about actions and time has received an overwhelming attention in the last couple of decades [Reiter, 2001; Kvarnstr¨om, 2005; Mueller, 2010; Thielscher, 2001; Broersen, 2009], as well as in philosophy [Nuel Belnap, 2001]. On the other hand, the theory of Dragan Doder †

∗Funded by the National Research Fund (FNR), Luxembourg, RationalArchitecture project.

† Funded by the National Research Fund (FNR), Luxembourg, PRIMAT project.

University of Luxembourg Luxembourg dragan.doder@uni.lu

Leendert van der Torre

University of Luxembourg Luxembourg leendert@vandertorre.com

belief revision has been investigated in detail [Peppas, 2007; G¨ardenfors, 2003; Van Benthem, 2011]. However, few attempts have been made to combine these two approaches, i.e. revision of theories that are defined in terms of action specifications with behavioral and temporal constraints.

Moreover, virtually all of the attempts to combine logics for reasoning about action and time with belief revision have been restricted purely to the syntactical level, mostly by showing that revision in the proposed logic satisfies the AGM postulates (e.g., [Shapiro et al., 2011; Jin and Thielscher, 2004; Scherl, 2005; Scherl and Levesque, 2003], but see Section 6 for a more detailed discussion). Surprisingly, none of these attempts prove the well-known representations theorems linking revision to a total pre-order on models.

The aim of this paper is to develop a logic about action and time, such that this logic can be used within a more general framework of belief revision. It is this constraint of using the logic within a belief revision setting that drives the design of the logic. Therefore, since belief revision is originally defined for propositional logic, it is our methodology to stay as close to propositional logic as possible.

We first develop the logic Parameterized-time Action Logic (PAL). The language of this logic contains formulas to reason about preconditions, postconditions, and the execution of actions. Atoms in the language are parameterized with the state at which they are true. The main result of the paper is that we prove the Katsuno-Mendelzon (KM) representation theorem and the Darwiche-Pearl (DP) representation theorem in PAL. To this end, we define a revision operator that revises formulas up to a specific time point. We show that this leads to models of system behaviors which can be finitely generated, i.e. be characterized by a single formula. We illustrate our approach by examples and show how it can be applied to various models of time, possibility and action. For example, doing an action may imply its precondition, or it may be equivalent to it.

The rest of this paper is organised as follows. Section 2 is preliminary and introduces belief revision concepts, in Section 3 we introduce PAL, in Section 4 we study belief revision in PAL, in Section 5 we provide some examples, and in Section 6 we discuss related work.

2 Preliminaries: Belief Revision

The AGM postulates [Alchourron et al., 1985] formulate properties that should be satisfied by any (rational) revision operators defined on deductively closed sets of propositional formulas. Katsuno and Mendelzon (KM) [1991] represent a belief set B as a propositional formula y such that B = {j | y ⊢ j}. They define the following six postulates for revision on y and show that these are equivalent to the eight AGM postulates:

• (R1) y◦j implies j
• (R2) If y∧j is satisfiable, then y◦j≡y∧j
• (R3) If j is satisfiable, then y◦j is also satisfiable
• (R4) If y≡y′ and j≡j′ , then y◦j≡y′ ◦j′
• (R5) (y◦j)∧j′ implies y◦(j∧j′ )
• (R6) If (y◦ j) ∧j′ is satisfiable, then y◦ (j∧j′ ) implies (y ◦ j) ∧ j′

Given a set I of all interpretations over some propositional language, they define a faithful assignment as a function that assigns each y to a pre-order ≤y on models satisfying the following three conditions:

1. If I, I ′ ∈Mod(y), then I <y I ′ does not hold.
2. If I ∈Mod(y) and I ′ ̸∈Mod(y), then I <y I ′ holds.
3. If y≡f, then ≤y=≤f.

They show in a representation theorem that a revision operator ◦ satisfies postulates (R1)-(R6) iff there exists a faithful assignment that maps each formula y to a total preorder ≤y such that

Darwiche and Pearl (DP) [1997] observe that the AGM postulates are too permissive to enforce plausible iterated revision. In order to remedy this, they suggest two changes to the KM postulates (R1)-(R6):

• Instead of performing revision on a propositional formula, perform revision on an abstract object called an epistemic state Y, which contains, in addition to the propositional beliefs Bel(Y), the entire information needed for coherent reasoning. Formally, this means that each y in (R1)-(R6) is replaced with Y, where Y means Bel(Y) whenever it is embedded in a propositional formula. So Y∧j means Bel(Y)∧j, and Y1 ≡Y2 means Bel(Y1) ≡ Bel(Y2), while Y◦ j means an (abstract) epistemic state.
• Postulate (R4) is weakened as follows: (R*4) If Y=Y′ and j≡j′ , then Y◦j≡Y′ ◦j′

We refer to the DP postulates defined on epistemic states as (R*1)-(R*6). DP propose the following four additional postulates for a revision operator ◦ on epistemic states.

• (C2) If j |=¬j′ , then (Y◦j′ )◦j≡Y◦j
• (C3) If Y◦j |=j′ , then (Y◦j′ )◦j |=j′
• (C4) If Y◦j ̸|=¬j′ , then (Y◦j′ )◦j ̸|=¬j′

They alter the KM definition of a faithful assignment to epistemic states and obtain a representation theorem similar to that of KM above. They show in a second representation theorem that a revision operator ◦t satisfying their postulates (R*1)-(R*6) satisfies postulates (C1)-(C4) if and only if the operator and its corresponding faithful assignment satisfy:

• (CR1) If m1 |=j and m2 |=j, then m1 ≤Y m2 iff m1 ≤Y◦j m2.
• (CR2) If m1 ̸|=j and m2 ̸|=j, then m1 ≤Y m2 iff m1 ≤Y◦j m2.
• (CR3) If m1 |=j, m2 ̸|=j and m1 <Y m2, then m1 <Y◦j m2.
• (CR4) If m1 |=j, m2 ̸|=j and m1 ≤Y m2, then m1 ≤Y◦j m2.

All the above results are based on propositional logic. Logics for reasoning with beliefs about action specifications and time are generally not propositional, but use modalities or high-order logics (see Section 6 for a more detailed discussion). When moving from propositional logic to such more expressive logics, it is in general no longer possible to represent a belief set by a single formula y, because it can no longer be guaranteed that the number of models for the logic is finite. This may have different reasons: Time can be infinite, actions can be non-deterministic, or modalities may lead to infinite models. Consequently, the KM and DP representation theorem can no longer be obtained directly for such logics. In the following section, we develop a simple temporal logic and show in the section following it that we can reproduce both the KM and the DP representation theorems for a restricted fragment of this logic.

3 Parameterized-time Action Logic (PAL)

Our aim in this section is to develop a logical system that represents an agent's beliefs about the current moment and future moment and actions that may be performed. Beliefs are represented by the formal language L .

Definition 1 (Language). Let Act = {a,b,c, . . .} be a finite set of deterministic primitive actions, and Prop = {p,q,r, . . .} ∪ {pre(a), post(a) | a ∈ Act} be a finite set of propositions. 1 The sets Prop and Act are disjoint. The language L is inductively defined by the following BNF grammar:

with c ∈ Prop, a ∈ Act, and t ∈ N0. We abbreviate ¬□t ¬ with ♦t , and define ⊥≡ p0 ∧¬p0 and ⊤≡¬⊥. Past(t) is the set of all PAL formulas generated by boolean combinations of pt ′ , pre(a)t ′ , post(a)t ′ , □t ′ j, and do(a)t ′-1 where t ′ ≤ t and j is some PAL formula.

Intuitively, pt means that the atomic formula p is true at time t, do(a)t means that action a is executed at time t. To every action and every time we associate formulas pre(a)t and post(a)t+1, which are understood as the preconditions and postconditions of action a at time t. The modal operator

1 Throughout this paper we denote atomic propositions with c.

□t is interpreted as necessity, indexed with a time point t. The other boolean connectives are defined as usual.

The semantics of our logic is similar to CTL* [Reynolds, 2002], namely a tree structure containing nodes and edges connecting the nodes. 2 With each natural number i ∈ N0 we associate a set of states Si such that all these sets are disjoint. We then define the accessibility relation between states such that it generates an infinite, single tree.

Definition 2 (Tree). A tree is quadruple T = (S,R,v,act) where S = ⋃n∈N0 Sn is a set of states, such that each St is the set of states at time t, Si ∩ Sj = /0 for i ̸= j; R ⊆ ⋃n∈N0 Sn×Sn+1 is an accessibility relation that is serial, linearly ordered in the past and connected (so S0 is a singleton); v : S→2 Prop is a valuation function from states to sets of propositions; and act : R → Act is a function assigning actions to elements of the accessibility relation, such that actions are deterministic, i.e. if act((s,s′ )) = act((s,s′′ )), then s′ = s′′ .

Definition 3 (Path). Given a tree T = (S,R,v,act), a path p = (s0,s1, . . .) in T is a sequence of states such that (st , st+1) ∈ R. We write pt to refer to the t'th state of the path p and we thus write v(pt ) and act((pt ,pt+1)) to refer respectively to the propositions true and the next action on path p at time t. For readability, we abbreviate act((pt ,pt+1)) with act (pt ).

Intuitively, v(pt) are the propositions true at time t on path p, and act(pt) is the next action a on the path. There is a natural equivalence relation ∼t on paths.

Definition 4 (Path equivalence). Two paths p and p′ are equivalent up to time t, denoted p ∼t p′ , if and only if they contain the same states up to and including time t, i.e. p∼t p′ iff (∀t ′ ≤t).(v(pt ′ )=v(p′ t ′ )) and (∀t ′ < t ).(act (pt ′ ) = act (p′ t ′ )).

Formulas in PAL are evaluated on a path. Therefore, a model for a formula is pair consisting of a tree and a path in this tree. This, together with some additional constraints related to the pre- and post-conditions of actions, is our definition of a model.

Definition 5 (Model). A model is a pair (T,p) where T = (S,R, v,act) is a tree and p is a path in T such that the following conditions hold:

1. If act(pt) =a, then post(a) ∈ v(pt+1),
2. If pre(a) ∈ v(pt), then there is some p′ in T with p∼t p′ and act(p′ t ) = a.

We denote models with m1,m2, . . . and sets of models with M1,M2, . . .. We denote the set of all models with M.

Definition 6 (Truth definitions). Let m= (T,p) be a model with T = (S, R, v, act ):

• T,p |=ct iff c ∈ v(pt) with c ∈Prop

T,p |= ¬j iff T,p ̸|= j

2 A tree can equivalently be seen as an enfolded transition system, thereby representing all the possible runs through it. We choose to represent our semantics using trees because it simplifies the completeness proofs. See Reynolds [2002] for an overview of different kinds of semantics and conceptual underpinnings.

The logical notions of satisfiability, validity and semantics consequence are defined as usual.

Definition 7. The logic PAL consists of the following axiom schemas and rules:

The relation ⊢ is defined in the usual way with the restriction that (NEC) can be applied to theorems only.

Theorem 1 (Completeness Theorem). The logic PAL is sound and strongly complete, i.e. T ⊢ j iff T |=j.

Proof Sketch. We prove the following formulation of completeness: each consistent set of formulas T has a model. We use the fact that each consistent set can be extended to a maximally consistent set (mcs) S, i.e. S is consistent and each proper superset of S is inconsistent. In the first step we extend T to a mcs T ∗ . We define a tree MT ∗ = (S,R, v,a):

1. S = ⋃t∈NSt where St ={[T ∗ ]t | T ∗ ≡t T ∗}
2. sRs′ iff (∃T ∗ ,t ∈N).(s = [T ∗ ]t ∧s′ = [T ∗ ]t+1)
3. p ∈ v(s) iff (∃T ∗ ,t ∈N).(s = [T ∗ ]t ∧ p t ∈ T ∗ ).
4. a = act((s,s′ )) iff (∃T ∗ ).(s = [T ∗ ]t ∧ s′ = [T ∗ ]t+1 ∧ do(a)t ∈ T ∗ ).

where [T ∗ ]t = {T ∗ | T ∗ ≡t T ∗ } s.t. ≡t is an equivalence relation on mcs's defined by T ∗ 1 ≡t T ∗ 2 iff T ∗ 1 ∩Past(t) = T ∗ 2 ∩ Past(t). If p(T ∗ ) = (s0, s1, . . .), where st = [T ∗ ]t , then one can show that (MT ∗ ,p(T ∗ )) is a model. Finally, we prove that for each j, (MT ∗ ,p(T ∗ ) |= j iff j ∈ T ∗ ), using induction on the depth of the proof. Consequently, MT ∗ , p(T ∗ ) |= T .

We shortly highlight the most important axiomatization considerations. First, note that exactly one action is executed in each time point (A6 and A7), and that actions are deterministic (A10). Semantically, this means that from a state, one can never reach two different successor states through the same action. The fact that postconditions of actions always hold on a path (A9), but that preconditions may not (A8), suggests that preconditions, unlike postconditions, need not be believed when an action is selected. We might therefore think of our belief model as, in some sense, one of "optimistic" beliefs. Returning to the calendar agent, it may be well possible that a calendar contains the entry to possibly attend IJCAI in July 2015, i.e. ♦Jan2015do(attend IJCAI)Jul2015, while the precondition is not satisfied yet, i.e. the paper is not accepted yet. And even if it would turn out that the paper is accepted, there may be no budget yet, or no flight booked. Therefore, we allow actions to be believed while preconditions are not satisfied (yet). We will return to these considerations in more detail in Section 5.

4 Belief Revision in PAL

Time in PAL is infinite in the future, so it is generally not possible to represent a PAL belief set closed under consequence by a single formula y, since this may potentially lead to an infinite conjunction. Therefore, we cannot prove the KM and DP representation theorems directly. In this section, we define a bounded revision function and we restrict the syntax and semantics of PAL up to a specific time point. We then prove two representation theorems.

Single-Step Revision We define a bounded revision function ∗t revising a set of PAL formulas B with another PAL formula j, denoted B∗t j, where t is the maximal time point occurring in both B and j. In order to do so, we first define the set of formulas Formt containing all PAL formulas with time points no larger than t, and Belt containing all sets of Formt formulas.

Definition 8 (AGM t-Bounded Revision Function). Suppose some t ∈ N0. Let max t(j) denote the maximal time point occurring in j. Let Formt = {j ∈L | max t(j) ≤ t} and Belt = {Cl(S) | S ⊆ Formt }.

An AGM t-bounded revision function ∗t : Belt ×Formt → Belt maps a deductively closed set from Belt and a formula from Formt to deductively closed set from Belt , and satisfies the AGM postulates [Alchourron et al., 1985].

We next define a bounded model as a pair consisting of a tree and a path, in which all paths in the tree are cut off up to a specific time point.

Definition 9 (t-BoundedModel). Suppose some model m= (T,p). A t-bounded path p[t] is defined from a path p in T as p[t] = (p0, . . . ,pt ). A t-bounded model m[t] = (T [t],p[t]) is a pair where T[t] = {p[t] | p ∈ T}. M[t] is the set of all t-bounded models. If the time point t is irrelevant or clear from the context, we may abbreviate p[t],T[t],m[t] and M[t] with p,T ,m, and M, respectively.

We will show in Lemma 4 below that it is possible to represent each B ∈ Belt by a formula y ∈ Formt such that Cl(B) =Cl(y). Using this lemma, we adapt the definition of a KM faithful assignment.

Definition 10 (t-Bounded Faithful Assignment). A tbounded faithful assignment is a function that maps each belief formula y ∈ Formt to a total preorder ≤t y on all models such that:

1. If m1,m2 ∈Mod(y), then m1 ≤t y m2 and m2 ≤t y m1
2. If m1 ∈Mod(y) and m2 ̸∈Mod(y), then m1 <t y m2
3. If y≡f, then ≤t y=≤t f
4. If m1 =m2, then m1 ≤t y m2 and m2 ≤t y m1

Since we only consider beliefs up to some time t, we do not want to distinguish between models that are the same up to time t in the total pre-order ≤t y. This is essentially what condition (4) of the faithful assignment above ensures. The first three conditions are the same as those by KM.

Theorem 2 (Representation Theorem). A t-bounded revision operator ◦t satisfies postulates (R1)-(R6) iff there exists a t-bounded faithful assignment that maps each belief set y to a total preorder ≤t y such that

We will use the remainder of this subsection to prove the representation theorem above. We first show that the number of t-bounded model is finite.

Proof. Suppose some t ∈N0. Since actions are deterministic and there are finitely many actions in our logic, each state has a finite number of successor states. Moreover, since there are finitely many propositions in our language, the number of possible valuations of the states is finite as well. Therefore, the number of models in M[t] is finite.

The following lemma obtains a correspondence between semantic consequence of two models equivalent up to t. The proof is by induction on the depth of the formula.

Lemma 2. For each j ∈ Formt and models m1,m2 ∈M, if m1[t] =m2[t], then m1 |=j iff m2 |=j.

Let Ext(m) be the set of all possible extensions of the bounded model m to models, i.e. Ext(m) = {m′ ∈ M | m′ [t ] = m}. We next show that we can represent each Ext(m) by a single formula.

Lemma 3. For all t ∈N0 and m∈M[t], there exists a formula f orm(m) ∈Formt such that Mod( f orm(m)) =Ext(m).

Proof. For t ∈N0 and m= (T,p) we define:

Then we define:

It follows directly from our construction that m is a model of f orm(m). By Lemma 2 for each m′ ∈ Ext(m) : m′ |= f orm(m). What remains to show is that if m′ = (T ′ ,p′ ) and m ̸= m′ , then m′ ̸|= f orm(m). Since m′ ̸= m we have (1) T ̸= T ′ or (2) p ̸= p′ . In case (1), if there exists some path p′′ ∈ T s.t. p′′ ̸∈ T ′ , then the formula ♦0ap′′ is true in m but not in m′ . But then f orm(m) is also not true in m′ , hence m′ ̸|= f orm(m). If there exists some path p′′ ∈ T ′ and p′′ ̸∈ T, then ¬♦0ap′′ is true in m but not in m′ , so m′ ̸|= f orm(m) follows as well. In case (2) ap ̸= ap′ and thus m′ ̸|= f orm(m).

We can now show that it is indeed possible to represent a belief base in Belt as a single formula.

Lemma 4. For each B ∈ Belt there exists a formula y such that B =Cl(y).

Proof. Suppose an arbitrary B ∈ Belt . It follows from Lemma 1 that the number of t-bounded models for B is finite. Therefore, using Lemma 3 we define y = ∨m[t]|=B f orm(m). So, the set of t-bounded models of y is the union of the set of t-bounded models of B. Therefore, m[t] |=B iff m[t] |=y. By Lemma 2, m |= B iff m |= y, so B |= j iff y |= j. Finally, by the completeness theorem we can conclude B ⊢ j iff y ⊢ j.

We next provide a proof sketch of Theorem 2.

Proof Sketch (Theorem 2). (⇒): We define a t-bounded faithful assignment ≤t y as: m1 ≤t y m2 iff m1 ∈ Mod(y) or m1 ∈ Mod(y ◦t f orm(m) ∨ f orm(m′ )). Let us prove the new condition (4) of Def. 10. Let m and m′ be such that m = m′ . By Lemm 3, Mod( f orm(m)) = Ext(m) = Ext(m′ ) =Mod( f orm(m′ )). Hence, f orm(m) ≡ f orm(m′ ), so f orm(m,m′ )≡ f orm(m). By (R4): Mod(y◦t f orm(m))= Mod(y◦t f orm(m,m′ ))). By (R1), m ∈Mod(y◦t f orm(m), so m ∈Mod(y◦t f orm(m,m′ )). Hence, by the definition of ≤t y: m≤t y m′ . We can prove m′ ≤t y m similarly.

(⇐): We show that there exists some y◦t j ⊆ Formt s.t. Mod(y ◦t j) = min(Mod(j),≤t y). Suppose that j is consistent (j ≡⊥ is trivial). If m ∈ min(Mod(j),≤t y), by condition (4) we obtain Ext(j) ⊆ min(Mod(a),≤t y). Thus, there exists a set S ⊆M[t] s.t. min(Mod(j),≤t y) = ∪m∈SExt(m). If y◦t j is the formula ∨m∈S f orm(m), then Mod(y◦t j) = ∪m∈SExt(m) by Lemma 3. So there exists such y◦t j. For the other parts of the proof we modify KM straightforwardly.

Iterated Revision Recall from Section 2 that Darwiche and Pearl propose to revise epistemic states instead of belief bases. When switching from belief revision on a belief state to belief revision on an epistemic state the definition of a faithful assignment should be adopted accordingly. We will do this now for our setting. Recall that Y stands for Bel(Y) whenever it is embedded in a propositional formula.

Definition 11 (t-bounded faithful assignment on epistemic states). A t-bounded faithful assignment on epistemic states maps each epistemic state Y with Bel(Y) from Belt , to a total pre-order ≤t Y on all models such that:

1. If m1,m2 |=Y, then m1 ≤t Y m2 and m2 ≤t Y m1
2. If m1 |=Y and m1 ̸|=Y, then m1 <t Y m2
3. If Y=F, then ≤Y=≤F
4. If m1 =m2, then m1 ≤t Y m2 and m2 ≤t Y m1

The next representation theorem is similar to Theorem 2, but it uses the DP postulates on epistemic states and the tbounded faithful assignment on epistemic states that we defined above. Recall that we refer to the DP postulates as (R*1)-(R*6).

Theorem 3 (Representation Theorem). A t-bounded revision operator ◦t satisfies postulates (R*1)-(R*6) precisely when there exists a t-bounded faithful assignment on epistemic states that maps each epistemic state Y to a total preorder ≤t Y such that

Proof Sketch. Straightforward modification of the proof of Theorem 2.

Theorem 4. Suppose that a t-bounded revision operator on epistemic states satisfies postulates (R*1)-(R*6). The operator satisfies postulates (C1)-(C4) iff the operator and its corresponding faithful assignment satisfy:

• CR1 If m1 |=j and m2 |=j, then m1 ≤t Y m2 iff m1 ≤t Y◦j m2.
• CR2 If m1 ̸|=j and m2 ̸|=j, then m1 ≤t Y m2 iff m1 ≤t Y◦j m2.
• CR3 If m1 |=j, m2 ̸|=j and m1 <t Y m2, then m1 <t Y◦j m2.

Proof Sketch. (⇐): Identical to DP.

(⇒): We prove (C1)⇒(CR1), the proofs for the other postulates are similar. Suppose that (C1) holds and m,m′ |=j. Let a = f orm(m, m′ ). By Lemma Lemma 3, Mod(a) = Ext(m)∪ Ext(m′ ). If m′′ ∈ Ext(m), then m = m′′ , so by Lemma Lemma 2 we obtain m′′ |= j. Similarly, if m′′ ∈ Ext(m′ ), then m′′ |= j, so a |= j. By (C1), (Y◦t j) ◦t a ≡ Y◦t a. In other words, min(Mod(a),≤t Y◦t j ) = min(Mod(a),≤t Y). Consequently, m ≤t Y◦tj m′ iff m≤t Y m′ .

5 Examples

We start with a simple example illustrating revision using a pre-order over models in our temporal logic.

Example 1. Suppose a setting with two actions, i.e. Act = {a,b} and no propositions other than the preand postconditions for these actions, i.e. Prop = {pre(a), post(a), pre(b), post(b)}. Suppose that y is equivalent to

The three 1-bounded models of y are {m1,m2,m3}. See Figure 1, note that formulas that are false in a state have been omitted. If we define ≤t y as m1 ≤t y m2 iff m1 ∈ Mod(y) or m1 ∈Mod(y◦t ( f orm(m1)∨ f orm(m2)), then these three models are minimal. Suppose we for instance revise with ¬♦0 post(b)1. Then, bounded models m2 and m3 are removed, i.e. Mod[1](y◦1 ¬♦0post(b)1) = {m1}, while revising with ♦0do(b)0 will remove model m1, since in this model it is not possible that action b is executed.

Our next example considers the relation between preconditions and actions in the axiomatization of PAL.

Example 2. The calendar agent believes that IJCAI is attended in July 2015 because a paper has been submitted. Now, the agent learns in March that the paper to IJCAI is rejected, which causes the agent to believe that it will be impossible to attend IJCAI. However, the agent upholds its belief that IJCAI is attended in July. Let t1 and t2 as before.

As we already briefly mentioned in Section 3, in our current model preconditions are sufficient conditions of actions to be possible, but they are not necessary. Such a model can be used in planning domains in which it, at the moment of planning, may not be clear whether preconditions are true [Shoham, 2009]. While such optimistic beliefs allow an agent to reason about its actions while not being committed to accept the preconditions of these action, this assumption may in some cases be considered rather weak. We can straightforwardly strengthen this assumption by replacing axiom (A8) with the following:

Completeness is preserved by changing the condition (2) of Definition 5 from an "if" to an "if and only if". Indeed, it can be verified that in the previous example adopting the belief that the precondition to attend IJCAI is impossible will cause the agent to drop its belief that it will attend IJCAI.

6 RelatedWork

Many logical systems have been developed for reasoning about the pre and postconditions of actions with explicit time points, such as the Event Calculus [Mueller, 2010], Temporal Action Logics [Kvarnstr¨om, 2005], extensions to the Fluent Calculus [Thielscher, 2001], and extensions to the Situation Calculus [Papadakis and Plexousakis, 2003] (see [Patkos, 2010, Ch.2] for an overview). Much effort in this field concentrates on extending these action theories to incorporate sensing or knowledge-producing actions, i.e., actions whose effects change the mental state of an agent instead of the world. Shapiro [2011] extends the Situation Calculus to reason about beliefs rather than knowledge by introducing a modality B and shows that both the AGM postulates and the DP postulates are satisfied in this framework. A similar approach concerning the Fluent Calculus has been formalized by Jin and Thielscher [2004], and is further developed by Scherl [2005] and Scherl and Levesque [2003] by taking into account the frame problem as well. Although these approaches all obtain correspondences with the AGM or DP postulates on a syntactical level, none of them prove representations theorems linking revision to a total pre-order on models.

Baral and Zhang [2005] model belief updates on the basis of semantics of modal logic S5 by specifying an update according to the minimal change on both the agent's actual world and knowledge. They show that their knowledge update operator satisfies all the KM postulates. Bonanno [2007] combines temporal logic with AGM belief revision as well, and extends a temporal logic with a belief operator and an information operator. Both these approaches do not take action or time into account and do not provide a representation theorem.

Semantically, PAL is close to CTL* [Reynolds, 2002], dating back to Prior [1967] with three important differences. First, PAL contains time-indexed modalities, which allows one to express statements such as "It is possible in February that I will attend IJCAI in July". Secondly, PAL allows for explicit reasoning about pre-and postconditions of deterministic actions (axiom A10). Thirdly, PAL only contains one type of modality, while CTL* contains a next operator and an until operator as well. The last two reasons arguably make PAL less expressive that CTL*, but in return the axiomatization is straightforward, we are able to obtain strong completeness, and it is possible to prove both representation theorems. It seems that this is not possible for CTL* in general.

The logic PAL is also closely related to the logic developed by Icard et al. [2010], who study the joint revision of beliefs and intentions using AGM-like postulates. However, we show in a recent paper that one of their axioms is not sound and that their logic is noncompact, so no axiomatization using their syntax and semantics (including theirs) is strongly complete [van Zee et al., 2015]. Moreover, we focus on revision of beliefs up to time t and iterated revision.

7 Summary and Outlook

We present a temporal logic for reasoning about beliefs and action in time. To apply the Katsuno-Mendelzon and Darwiche-Pearl representation theorems to belief sets of this logic, we restrict ourselves to beliefs generated by formulas which represent beliefs up to certain time. Using this restriction, we prove both representation theorems for our logic.

The main challenge of this paper is to define revision in a temporal logic with infinite time. While much research has focused on extending existing logics for reasoning about action and change with the incorporation of new beliefs, the semantic counterpart in the form of a total pre-order on models is not taken into account. This paper has tried to take a first step into this direction, but there are many directions from here that should be explored:

The frame problem is one of the most fundamental problems in reasoning about action and change. The challenge is how to specify the non-effects of actions succinctly. For instance, if a proposition such as "The table is red" is true at some time t, and no action occurs that affects the truth value of this proposition, then it seems plausible that the table is still red at time t +1. Currently, our framework does not contain so-called "frame axioms", and it is an interesting question how the AGM and DP postulates can be extended to account for such behavior as well.

Other mental attitudes, such as intentions, goals, desires and preferences, we have left out completely. This is not because we assume that they are unimportant, but because it was our goal to focus on belief revision in a temporal setting. However, returning to our calender assistant, there is nothing keeping us from treating the appointments that a user makes as "intentions", and given the recent work in the revision of intentions [Shoham, 2009; van der Hoek et al., 2007; Icard et al., 2010; Lorini et al., 2009] this certainly is a direction worth exploring.