Ivan José Varzinczak
email: ivan.varzinczak@irit.fr

Action Theory Contraction and Minimal Change

This work is about changing action domain descriptions in dynamic logic. We here revisit the semantics of action theory contraction, giving more robust operators that express minimal change based on a notion of distance between models. We then define syntactical contraction operators and establish their correctness w.r.t. our semantics. Finally we show that our operators satisfy the PDL-counterpart of the standard postulates for theory change adopted in the literature.

Introduction and Motivation

Let an intelligent agent be designed to perform rationally in a dynamic world, and suppose she should reason about the dynamics of an automatic coffee machine. Suppose that the agent believes that a coffee is a hot beverage. Now suppose that some day she gets a coffee and observes it is cold. In such a case, the agent must change her beliefs about the relationship between the propositions "I have a coffee" and "I have a hot beverage". This example is an instance of the problem of changing propositional belief bases and is largely addressed in the literature about belief change [START_REF] Gärdenfors | Knowledge in Flux: Modeling the Dynamics of Epistemic States[END_REF]) and belief update [START_REF] Kaufmann | On the difference between updating a knowledge base and revising it[END_REF].

Next, let our agent believe that whenever buying a coffee on the machine, she gets a hot beverage. This means that in every state of the world that follows the execution of buying, the agent possesses a hot beverage. Some day, it may happen that the machine is running out of cups, and then after buying, the coffee runs through the shelf and so the agent holds no hot beverage.

Imagine now the agent believes that if she has a token, then it is always possible to buy coffee. However, during a blackout, even with a token the agent does not manage to order her coffee on the machine.

The last two examples illustrate situations where changing the beliefs about the behavior of the action of buying coffee is mandatory. In the first one, buying coffee, once believed to be deterministic, has now to be seen as nondeterministic, or alternatively to have a different outcome in a more specific context (e.g. if there is no cup in the machine).

In the second example, the executability of the action under concern is questioned in the light of new information showing a context that was not known to preclude its execution.

Such cases of theory change are very important in logical descriptions of dynamic domains: it may always happen that one discovers that an action actually has a behavior that is different from that one has always believed it had.

Up to now, theory change has been studied mainly for knowledge bases in classical logics, both in terms of revision and update. Since [START_REF] Fuhrmann | On the modal logic of theory change[END_REF], only in a few recent works it has been considered in the realm of modal logics, viz. in epistemic logic [START_REF] Hansson | A Textbook of Belief Dynamics: Theory Change and Database Updating[END_REF] and in dynamic logics [START_REF] Herzig | Elaborating domain descriptions[END_REF], and in action languages [START_REF] Eiter | Updating action domain descriptions[END_REF]. Some other works [START_REF] Shapiro | Iterated belief change in the situation calculus[END_REF][START_REF] Jin | Iterated belief revision, revised[END_REF] have investigated revision of beliefs about facts of the world. In our scenario, this would concern for example the truth of token in a given state: the agent believes she has a token, but is wrong about that and might subsequently be forced to revise her beliefs about the current state of affairs. Such belief revision operations do not modify the agent's beliefs about the action laws. In opposition to that, here we are interested exactly in such modifications.

Logical Preliminaries

Our base formalism is Propositional Dynamic Logic (PDL) without the * operator [START_REF] Harel | Dynamic Logic[END_REF].

Action Theories in Dynamic Logic

Let Act = {a 1 , a 2 , . . .} be the set of atomic actions of a given domain. An example of atomic action is buy. To each action a there is associated a modal operator [a]. Prop = {p 1 , p 2 , . . .} denotes the set of propositional constants, also called fluents or atoms. Examples of those are token ("the agent has a token") and coffee ("the agent holds a coffee"). The set of all literals is Lit = {ℓ 1 , ℓ 2 , . . .}, where each ℓ i is either p or ¬p, for some p ∈ Prop. If ℓ = ¬p, then we identify ¬ℓ with p. By |ℓ| we denote the atom in ℓ.

We use ϕ, ψ, . . . to denote Boolean formulas, an example of which is coffee → hot. Fml is the set of all Boolean formulas. A propositional valuation v is a maximally consistent set of literals. We denote by v ϕ the fact that v satisfies ϕ. By val(ϕ) we denote the set of all valuations satisfying ϕ.

|= CPL is the classical consequence relation. Cn(ϕ) denotes all logical consequences of ϕ in classical propositional logic.

With IP(ϕ) we denote the set of prime implicants [START_REF] Quine | The problem of simplifying truth functions[END_REF] of ϕ. By π we denote a prime implicant, and atm(π) is the set of atoms occurring in π. For given ℓ and π, ℓ ∈ π abbreviates 'ℓ is a literal of π'.

We will use Φ, Ψ, . . . to denote complex formulas (formulas with modal operators). An example of a complex formula is ¬coffee → [buy]coffee. a is the dual operator of

[a] ( a Φ = def ¬[a]¬Φ).
A PDL-model is a tuple M = W, R where W is a set of valuations, and R maps action constants a to accessibility relations With PDL we can state laws describing the behavior of actions. Following the tradition in the reasoning about actions community, we here distinguish three types of them.

R a ⊆ W × W. Given M , |= M w p (p is true at world w of model M ) if w p; |= M w [a]Φ if |= M w ′ Φ for every w ′ s.t. (w, w ′ ) ∈ R a ; truth

Static Laws

A static law is a formula ϕ ∈ Fml. It is a formula that characterizes the possible states of the world. An example of static law is coffee → hot: if the agent holds a coffee, then she holds a hot beverage. The set of all static laws of a domain is denoted by S .

Effect Laws An effect law for a is of the form ϕ → [a]ψ, where ϕ, ψ ∈ Fml. Effect laws are formulas relating an action to its effects, which can be conditional. The consequent ψ is the effect that always obtains when a is executed in a state where the antecedent ϕ holds. If a is a nondeterministic action, then ψ is typically a disjunction. An example of such a law is token → [buy]hot: whenever the agent has a token, after buying, she has a hot beverage. If ψ is inconsistent we have a special kind of effect law that we call an inexecutability law. For example, ¬token → [buy]⊥ says that buy cannot be executed if the agent has no token. The set of effect laws of a domain is denoted by E .

Executability Laws

An executability law for a has the form ϕ → a ⊤, with ϕ ∈ Fml. It stipulates the context in which a is guaranteed to be executable. (In PDL, the operator a is used to express executability, a ⊤ thus reads "a's execution is possible".) For instance, token → buy ⊤ says that buying can be executed whenever the agent has a token. The set of all executability laws of a domain is denoted by X .

Given a, E a (resp. X a ) will denote the set of only those effect (resp. executability) laws about a.

Action Theories T = S ∪ E ∪ X is an action theory.

For the sake of clarity, we will here abstract from the frame problem [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intelligence[END_REF] and the ramification problem [START_REF] Finger | Exploiting constraints in design synthesis[END_REF], and assume that the agent's theory contains all frame axioms (cf. [START_REF] Herzig | Elaborating domain descriptions[END_REF]) for a contraction approach within a solution to the frame problem). The action theory of our example will be: Sometimes it will be useful to consider models whose possible worlds are all the possible worlds allowed by S : Definition 1 Let T = S ∪ E ∪ X be an action theory. Then M = W, R is the big model of T if and only if:

T =      coffee → hot,
• W = val(S ); and • R a = {(w, w ′ ) : ∀.ϕ → [a]ψ ∈ E a , if |= M w ϕ then |= M w ′ ψ}.

Elementary Atoms

Given ϕ ∈ Fml, E(ϕ) denotes the elementary atoms actually occurring in ϕ. For example, E(¬p

1 ∧ (¬p 1 ∨ p 2 )) = {p 1 , p 2 }. An atom p is essential to ϕ if and only if p ∈ E(ϕ ′ ) for all ϕ ′ such that |= CPL ϕ ↔ ϕ ′ . For instance, p 1 is essential to ¬p 1 ∧(¬p 1 ∨p 2 ). E!(ϕ) will denote the essential atoms of ϕ. (If ϕ is a tautology or a contradiction, then E!(ϕ) = ∅.) For ϕ ∈ Fml, ϕ * is the set of all ϕ ′ ∈ Fml such that ϕ |= CPL ϕ ′ and E(ϕ ′ ) ⊆ E!(ϕ). For instance, p 1 ∨ p 2 / ∈ p 1 * , as p 1 |= CPL p 1 ∨ p 2 but E(p 1 ∨ p 2 ) ⊆ E!(p 1 ). Clearly, E( ϕ * ) = E!( ϕ * ). Moreover, whenever |= CPL ϕ ↔ ϕ ′ , then E!(ϕ) = E!(ϕ ′
) and also ϕ * = ϕ ′ * .

Theorem 1 (Least atom-set theorem (Parikh 1999))

|= CPL ϕ ↔ ϕ * , and E(ϕ * ) ⊆ E(ϕ ′ ) for every ϕ ′ s.t. |= CPL ϕ ↔ ϕ ′ .
Thus for every ϕ ∈ Fml there is a unique least set of elementary atoms such that ϕ may equivalently be expressed using only atoms from that set. 1 Hence, Cn(ϕ) = Cn(ϕ * ).

Prime Valuations

Given a valuation v, v ′ ⊆ v is a subvaluation. For W a set of valuations, a subvaluation v ′ satisfies ϕ ∈ Fml modulo W (noted v ′ W ϕ) if and only if v ϕ for all v ∈ W such that v ′ ⊆ v. A subvaluation v essentially satisfies ϕ modulo W (v ! W ϕ) if

Closeness Between Models

When contracting a formula from a model, we will perform a change in its structure. Because there can be several different ways of modifying a model (not all of them minimal), we need a notion of distance between models to identify those that are closest to the original one.

As we are going to see in more depth in the sequel, changing a model amounts to modifying its possible worlds or its accessibility relation. Hence, the distance between two PDL-models will depend upon the distance between their sets of worlds and accessibility relations. These here will be based on the symmetric difference between sets, defined as

X -Y = (X \ Y ) ∪ (Y \ X). Definition 3 Let M = W, R be a model. M ′ = W ′ , R ′ is as close to M as M ′′ = W ′′ , R ′′ , noted M ′ M M ′′ , if and only if • either W -W ′ ⊆ W -W ′′ • or W -W ′ = W -W ′′ and R -R ′ ⊆ R -R ′′
(Notice that other distance notions are also possible, like e.g. considering the cardinality of symmetric differences.) 1 The dual notion (redundant atoms) is also addressed in the literature, e.g. in [START_REF] Herzig | Propositional belief base update and minimal change[END_REF], with similar purposes.

Semantics of Contraction

When contracting a law Φ we must ensure that Φ becomes invalid in at least one (possibly new) model of the dynamic domain. Because there can be lots of models to consider, we start with a set M of models in which Φ is (potentially) valid. Thus contracting Φ amounts to make it no longer valid in this set of models. What are the operations that must be carried out to achieve that? Throwing models out of M does not work, since Φ will keep on being valid in all models of the remaining set. Thus we should add new models to M. Which models? Well, models in which Φ is not true. But not any of such models: taking models falsifying Φ that are too different from our original models will certainly violate minimal change.

Hence, we shall take some model M ∈ M as basis and manipulate it to get a new model M ′ in which Φ is not true. In PDL, the removal of a law Φ from a model M amounts to modifying the possible worlds or the accessibility relation in M so that Φ becomes false. Such an operation gives as result a set M - Φ of models, each of which is no longer a model of Φ. But if there are several candidates, which ones should we choose? We shall take those that are minimal modifications of the original M . Note that there can be more than one M ′ that is minimal. Because adding just one of these new models is enough to invalidate Φ, we take all possible combinations M ∪ {M ′ } of expanding our set of models by one minimal model. The result will be a set of sets of models.

In each set of models there will be one M ′ falsifying Φ.

Contraction of Executability Laws

Intuitively, to contract an executability law ϕ → a ⊤ in one model, we remove arrows leaving ϕ-worlds. To success the operation, we have to guarantee that in the resulting model there is at least one ϕ-world with no departing a-arrow.

Definition 4 Let M = W, R be a PDL-model. Then M ′ = W ′ , R ′ ∈ M - ϕ→ a ⊤ if and only if • W ′ = W • R ′ ⊆ R • If (w, w ′ ) ∈ R \ R ′ , then |= M w ϕ • There is w ∈ W ′ s.t. |= M ′ w ϕ → a ⊤
To get minimal change, we want such an operation to be minimal w.r.t. the original model: we should remove a minimum set of arrows sufficient to get the desired result.

Definition 5 Let M be a PDL-model and ϕ → a ⊤ an executability law. Then

contraction(M , ϕ → a ⊤) = min{M - ϕ→ a ⊤ , M }
And now we define the sets of possible models resulting from the contraction of an executability in a set of models:

Definition 6 Let M be a set of models, and ϕ → a ⊤ an executability law. Then

M - ϕ→ a ⊤ = {M ′ : M ′ = M ∪ {M ′ }, M ′ ∈ contraction(M , ϕ → a ⊤), M ∈ M}.
In our example, consider M = {M }, where M is the model in Figure 2. When the agent discovers that even with a token she does not manage to buy a coffee anymore, she has to change her models in order to admit models with states where token is the case but from which there is no buy-transition at all. Because having just one of such worlds in each new model is enough, taking those resulting models whose accessibility relations are maximal guarantees minimal change. Hence we get M - token→ buy ⊤ = {M ∪ {M ′ i } : 1 ≤ i ≤ 3}, where each M ′ i is depicted in Figure 3.

M ′ 1 : t, c, h ¬t, c, h t, ¬c, h ¬t, ¬c, ¬h ¬t, ¬c, h t, ¬c, ¬h b b M ′ 2 : t, c, h ¬t, c, h t, ¬c, h ¬t, ¬c, ¬h ¬t, ¬c, h t, ¬c, ¬h b b M ′ 3 : t, c, h ¬t, c, h t, ¬c, h ¬t, ¬c, ¬h ¬t, ¬c, h t,

Contraction of Effect Laws

When the agent discovers that there may be cases when after buying she gets no hot beverage, she must give up the law token → [buy]hot in her models. This means that token ∧ buy ¬hot shall now be admitted in at least one world of some of her new models of beliefs. Hence, to contract an effect law ϕ → [a]ψ from a given model, we have to put new arrows leaving ϕ-worlds to worlds satisfying ¬ψ.

In our example, when contracting token → [buy]hot in the model of Figure 2, we add arrows from token-worlds to ¬hot-worlds. The challenge in such an operation is in guaranteeing minimal change: because coffee → hot, and then ¬hot → ¬coffee, this should also give buy ¬coffee (¬coffee is relevant to ¬hot). Hence, we can add arrows from token-worlds to ¬hot ∧ ¬coffee ∧ token-worlds, as well as to ¬hot ∧ ¬coffee ∧ ¬token (Figure 4). Pointing the arrow to ¬hot ∧ ¬coffee ∧ token would make us lose the effect ¬token, true after every execution of buy in the original model. How to preserve this law while allowing for the new transition to a ¬hot-world? This means that the only things allowed to change w.r.t. w in the candidate target world are those that are forced to change: they are relevant to ¬ψ or to another effect that applies in w. Every change outside that is not an intended one. Similarly, we want the literals preserved in the target world to be those that are relevant to ¬ψ or to some other effect that applies in w or that are usually preserved in w. Every preservation outside those may make us lose some law.

M : t, c, h ¬t, c, h t, ¬c, h ¬t, ¬c, ¬h ¬t, ¬c, h t, ¬c,
Here is where prime subvaluations play their role: the worlds one should aim the new arrow at are those whose difference w.r.t. w are literals that are relevant, and whose similarity w.r.t. w are literals we know may not change.

Definition 7 Let M = W, R , w, w ′ ∈ W, M be such that M ∈ M, and ϕ → [a]ψ an effect law. Then w ′ is a relevant target world of w w.r.t. ϕ → [a]ψ for M in M if and only if • |= M w ϕ, |= M w ′ ψ • for all ℓ ∈ w ′ \ w -either there is v ∈ base(¬ψ, W) s.t. v ⊆ w ′ and ℓ ∈ v -or there are ψ ′ ∈ Fml, v ′ ∈ base(ψ ′ , W) s.t. v ′ ⊆ w ′ , ℓ ∈ v ′ , and |= Mi w [a]ψ ′ for every M i ∈ M • for all ℓ ∈ w ∩ w ′ -either there is v ∈ base(¬ψ, W) s.t. v ⊆ w ′ and ℓ ∈ v -or there are ψ ′ ∈ Fml, v ′ ∈ base(ψ ′ , W) s.t. v ′ ⊆ w ′ , ℓ ∈ v ′ , and |= Mi w [a]ψ ′ for every M i ∈ M -or there is M i ∈ M such that |= Mi w [a]¬ℓ By RelTgt(w, ϕ → [a]ψ, M , M) we denote the set of all rel- evant target worlds of w w.r.t. ϕ → [a]ψ for M in M.
We need the set of models M (and here we can suppose it contains all models of the theory we want to change) because preserving effects depends on what other effects hold in the other models that interest us. One needs to take them into account in the local operation of changing one model: 2

Definition 8 Let M = W, R be a PDL-model and M be such that M ∈ M. Then M ′ = W ′ , R ′ ∈ M - ϕ→[a]ψ if and only if • W ′ = W • R ⊆ R ′ • (w, w ′ ) ∈ R ′ \ R implies w ′ ∈ RelTgt(w, ϕ → [a]ψ, M , M) • There is w ∈ W ′ s.t. |= M ′ w ϕ → [a]ψ
As having just one world where the law is no longer true in each model is enough, taking those resulting models whose difference w.r.t. the original accessibility relation is minimal guarantees minimal change:

Definition 9 Let M be a PDL-model and ϕ → [a]ψ an effect law. Then contraction(M , ϕ → [a]ψ) = min{M - ϕ→[a]ψ , M }
Now we can define the possible sets of models resulting from contracting an effect law from a set of models:

Definition 10 Let M be a set of models, and ϕ →

[a]ψ an effect law. Then M - ϕ→[a]ψ = {M ′ : M ′ = M ∪ {M ′ }, M ′ ∈ contraction(M , ϕ → [a]ψ), M ∈ M}.
Taking again M = {M }, for M as in Figure 2, after contracting the effect law token → [buy]hot from M, we get

M - token→[buy]hot = {M ∪ {M ′ i } : 1 ≤ i ≤ 3}
, where all M ′ i s are as depicted in Figure 5.

If ϕ is not satisfied by M or ψ is true in M , of course we do not succeed in falsifying ϕ → [a]ψ. In these cases, prior to do that we must change our set of possible states.

Contraction of Static Laws

When contracting a static law in a model, we want to admit at least one possible state falsifying it. Intuitively this means that we should add new worlds to the original model. This is quite easy. A delicate issue however is what to do with the accessibility relation: should new arrows leave/arrive at the new world? If no arrow leaves the new added world, we may lose an executability law. If some arrow leaves it, we may lose an effect law, the same holding if we add an arrow pointing to the new world. If no arrow arrives at the new world, what about the intuition? Do we want to have an unreachable state?

All this discussion shows how drastic a change in the static laws may be: it is a change in the underlying structure (possible states) of the world! Changing it may have as consequence the loss of an effect law or an executability law. 2 We do not need M in the local contraction of executabilities M - ϕ→ a ⊤ as all effects are preserved along the removal of arrows.

M ′ 1 : What we can do is choose which laws we accept to lose and postpone their change (by the other operators).

The tradition in the reasoning about actions community says that executability laws are, in general, more difficult to state than effect laws, and hence are more likely to be incorrect. Relying on this, in [START_REF] Herzig | Elaborating domain descriptions[END_REF] no change in the accessibility relation is made, what means preserving effect laws and postponing correction of executability laws. We here embrace this solution. It is controversial whether this approach is in line with the intuition or not (see (Varzinczak 2008a) for an alternative). Anyway, with the information we have at hand, this is the safest way of contracting static laws.

Definition 11 Let M = W, R be a PDL-model. Then M ′ = W ′ , R ′ ∈ M - ϕ if and only if • W ⊆ W ′ • R = R ′ • There is w ∈ W ′ s.t. |= M ′ w ϕ
The minimal modifications of one model are as expected: Definition 12 Let M be a model and ϕ a static law. Then

contraction(M , ϕ) = min{M - ϕ , M }
And we define the sets of models resulting from contracting a static law from one set of models:

Definition 13 Let M be a set of models, and ϕ a static law. Then M

- ϕ = {M ′ : M ′ = M ∪ {M ′ }, M ′ ∈ contraction(M , ϕ), M ∈ M}.
In our example, contracting the static law coffee → hot from M = {M }, with M as in Figure 2, will give us Notice that by not modifying the accessibility relation all the effect laws are preserved with minimal change. Moreover, our approach is also intuitive: when learning that a new state is now possible, we do not necessarily know all the behavior of the action in the new added state.

M - coffee→hot = {M ∪ {M ′ 1 }, M ∪ {M ′ 2 }},

Syntactic Operators for Contraction

We now turn our attention to the definition of a syntactical counterpart of our semantic operators. As [START_REF] Nebel | A knowledge level analysis of belief revision[END_REF]) says, "[. . . ] finite bases usually represent [. . . ] laws, and when we are forced to change the theory we would like to stay as close as possible to the original [. . . ] base." Hence, besides the definition of syntactical operators, we should also guarantee that they perform minimal change.

By T - Φ we denote in the sequel the result of contracting a law Φ from the set of laws T.

Contracting Executability Laws

For the case of contracting an executability law ϕ → a ⊤ from an action theory, the first thing we do is to ensure that the action a is still executable (if that was so) in all those contexts where ¬ϕ is the case. Second, in order to get minimality, we must make a executable in some contexts where ϕ is true, viz. all ϕ-worlds but one. This means that we can have several action theories as outcome.

Algorithm 1 gives a syntactical operator to achieve this.

Algorithm 1 Contraction of an executability law

input: T, ϕ → a ⊤ output: T - ϕ→ a ⊤ /* a set of theories */ if T |= PDL ϕ → a ⊤ then for all π ∈ IP(S ∧ ϕ) do for all A ⊆ atm(π) do ϕA:= V p i ∈atm(π) p i ∈A p i ∧ V p i ∈atm(π) p i / ∈A ¬p i if S |= CPL (π ∧ ϕA) → ⊥ then T ′ := (T \ X a ) ∪ {(ϕi ∧ ¬(π ∧ ϕA)) → a ⊤ : ϕi → a ⊤ ∈ X a } T - ϕ→ a ⊤ := T - ϕ→ a ⊤ ∪ {T ′ } else T - ϕ→ a ⊤ := {T}
As an example, contracting token → buy ⊤ from our theory T would give us three theories. One of them is:

T ′ 1 =              coffee → hot, ¬coffee → [buy]coffee, token → [buy]¬token, ¬token → [buy]⊥, ¬token → [buy]¬token, coffee → [buy]coffee, hot → [buy]hot, (token ∧ ¬coffee ∧ hot) → buy ⊤, (token ∧ ¬coffee ∧ ¬hot) → buy ⊤             

Contracting Effect Laws

When contracting an effect law ϕ → [a]ψ from a theory T, intuitively we should change some effect laws that preclude ¬ψ in target worlds. In order to cope with minimality, we must change only those laws that are relevant to ϕ → [a]ψ.

Let E ϕ,ψ a denote the minimum subset of the effect laws in E a such that S , E ϕ,ψ a |= PDL ϕ → [a]ψ. In the case where the theory is modular [START_REF] Herzig | On the modularity of theories[END_REF]) (see further), interpolation guarantees that such a set always exists. Moreover, note that there can be more than one such a set, in which case we denote them

(E ϕ,ψ a ) 1 , . . . , (E ϕ,ψ a ) n . Let E - a = 1≤i≤n (E ϕ,ψ a ) i
The laws in E - a will serve as guideline to get rid of ϕ → [a]ψ in the theory.

The first thing that we must do is to ensure that action a still has effect ψ (if that was so) in all those contexts in which ϕ does not hold. This means that we shall weaken the laws in E ϕ,ψ a specializing them to ¬ϕ. Second, we need to preserve all old effects in all ϕ-worlds but one. To achieve that, we specialize the above laws to each possible valuation satisfying ϕ but one. In the left ϕvaluation, we must ensure that action a has either its old effects or ¬ψ as outcome. We achieve that by weakening the consequent of the laws in E - a .

Finally, in order to get minimal change, we must ensure that all literals in this ϕ-valuation that are not forced to change in ¬ψ-worlds should be preserved. We do this by stating an effect law of the form (ϕ k ∧ℓ) → [a](ψ∨ℓ), where ϕ k is the above ϕ-valuation. The reason why this is needed is clear: there can be several ¬ψ-valuations, and as far as we want at most one to be reachable from ϕ k , we should force it to be the one whose difference to ϕ k is minimal.

Again, the result will be a set of theories. Algorithm 2 below gives the operator.

Algorithm 2 Contraction of an effect law

input: T, ϕ → [a]ψ output: T - ϕ→[a]ψ /* a set of theories */ if T |= PDL ϕ → [a]ψ then for all π ∈ IP(S ∧ ϕ) do for all A ⊆ atm(π) do ϕA:= V p i ∈atm(π) p i ∈A p i ∧ V p i ∈atm(π) p i / ∈A ¬p i if S |= CPL (π ∧ ϕA) → ⊥ then for all π ′ ∈ IP(S ∧ ¬ψ) do T ′ := (T \ E - a ) ∪ {(ϕi ∧ ¬(π ∧ ϕA)) → [a]ψi : ϕi → [a]ψi ∈ E - a } ∪ {(ϕi ∧ π ∧ ϕA) → [a](ψi ∨ π ′ ) : ϕi → [a]ψi ∈ E - a } for all L ⊆ Lit do if S |= CPL (π ∧ ϕA) → V ℓ∈L ℓ and S |= CPL (π ′ ∧ V ℓ∈L ℓ) → ⊥ then for all ℓ ∈ L do if T |= PDL (π ∧ ϕA ∧ ℓ) → [a]¬ℓ or ℓ ∈ π ′ then T ′ := T ′ ∪ {(π ∧ ϕA ∧ ℓ) → [a](ψ ∨ ℓ)} T - ϕ→[a]ψ := T - ϕ→[a]ψ ∪ {T ′ } else T - ϕ→[a]ψ := {T}
For instance, contracting the effect law token → [buy]hot from T will give us three resulting theories, one of them is

T ′ 1 =                    coffee → hot, token → buy ⊤, token → [buy]¬token, ¬token → [buy]⊥, ¬token → [buy]¬token, (coffee ∧ ¬(token ∧ coffee ∧ hot)) → [buy]coffee, (hot ∧ ¬(token ∧ coffee ∧ hot)) → [buy]hot, (¬coffee ∧ ¬(token ∧ coffee ∧ hot)) → [buy]coffee, (token ∧ coffee ∧ hot) → [buy](coffee ∨ ¬hot), (token ∧ coffee ∧ hot) → [buy](hot ∨ ¬coffee)                   

Contracting Static Laws

Finally, in order to contract a static law from a theory, we can use any standard contraction/revision operator ⊖ for classical propositional logic to change the set of static laws S . Because contracting static laws means admitting new possible states (cf. the semantics), it may be the case that just modifying S is not enough. Since we in general do not necessarily know the behavior of the actions in a new discovered state of the world, a careful approach is to change the theory so that all action laws remain the same in the contexts where the contracted law is the case. In our example, if when contracting the law coffee → hot we are not sure whether buy is still executable or not, we should weaken our executability laws specializing them to the context coffee → hot, and then make buy a priori inexecutable in all ¬(coffee → hot) contexts.

Algorithm 3 below formalizes such an operation.

T ′ := ((T \ S ) ∪ S -) \ X a ∪ {(ϕi ∧ ϕ) → a ⊤ : ϕi → a ⊤ ∈ X a } ∪ {¬ϕ → [a]⊥} T - ϕ := T - ϕ ∪ {T ′ } else T - ϕ := {T}
In our running example, contracting the law coffee → hot from T produces two theories, one of them is

T ′ 1 =              ¬(¬token ∧ coffee ∧ ¬hot), (token ∧ coffee → hot) → buy ⊤, ¬coffee → [buy]coffee, token → [buy]¬token, ¬token → [buy]⊥, ¬token → [buy]¬token, coffee → [buy]coffee, hot → [buy]hot, (coffee ∧ ¬hot) → [buy]⊥             
Observe that the effect laws are not affected by the change: as far as we do not state executabilities for the new world, all the effect laws remain true in it.

If the knowledge engineer is not happy with the added inexecutability law (coffee∧¬hot) → [buy]⊥, she can contract it from the theory using Algorithm 2.

Correctness of the Operators

Here we show that our algorithms are correct w.r.t. our semantics for action theory contraction. Before doing that, we need a definition.

Definition 14 (Modularity (Herzig and Varzinczak 2005)) An action theory T is modular if and only if for every

ϕ ∈ Fml, if T |= PDL ϕ, then S |= CPL ϕ.
For an example of a non-modular theory, suppose in our action theory T we had stated the law buy ⊤ instead of token → buy ⊤. Then T |= PDL token and S |= CPL token.

In [START_REF] Herzig | On the modularity of theories[END_REF] algorithms are given to check whether T satisfies the principle of modularity and also to make T satisfy it, if that is not the case.

Theorem 3 T is modular if and only if its big model is a model of T.

Modular theories have interesting properties. For example, if T is modular, then its consistency can be checked by just checking consistency of the set of static laws S alone. Deduction of effect laws does not need the executability ones and vice versa. Prediction of an effect of a sequence of actions a 1 ; . . . ; a n does not need the effect laws for actions other than a 1 , . . . , a n . This also applies to plan validation when deciding whether a 1 ; . . . ; a n ϕ is the case. For more results on modularity, see [START_REF] Herzig | Metatheory of actions: beyond consistency[END_REF].

The following theorem (see Appendix A for the proof) establishes that the semantic contraction of the law Φ from the set of models of the action theory T produces models of some contracted theory in T - Φ . Theorem 4 Let T be modular, and Φ be a law. For all

M ′ ∈ M - Φ such that |= M T for every M ∈ M, there is T ′ ∈ T - Φ such that |= M ′ T ′ for every M ′ ∈ M ′ .
The next theorem establishes the other way round: models of theories in T - Φ are all models of the semantical contraction of Φ from models of T. (The proof is in Appendix B.)

Theorem 5 Let T be modular, Φ a law, and

T ′ ∈ T - Φ . For all M ′ such that |= M ′ T ′ , there is M ′ ∈ M - Φ such that M ′ ∈ M ′ and |= M T for every M ∈ M.
Hence our operators are correct w.r.t. the semantics.

Assessment of Postulates for Change

We now analyze our operator's behavior w.r.t. Katsuno and Mendelzon's classical contraction postulates. (Due to space limitations, proofs are omitted here. They are all available at (Varzinczak 2008a).)

Theorem 6 T |= PDL T ′ , for all T ′ ∈ T - Φ . This result means our operators satisfy the PDL-version of Katsuno and Mendelzon's (C1) postulate about monotonicity. Such a postulate is not satisfied by the operators given in [START_REF] Herzig | Elaborating domain descriptions[END_REF]: there, when removing e.g. an executability law ϕ → a ⊤ one may make ϕ → [a]⊥ valid in all models of the resulting theory.

Theorem 7 If T |= PDL Φ, then |= PDL T ↔ T ′ , for all T ′ ∈ T - Φ . This corresponds to Katsuno and Mendelzon's (C2) postulate about preservation. Whenever T |= PDL Φ, then the models of the resulting theory are exactly the models of T, because these are the minimal models falsifying Φ.

Theorem 8 Let T = S ∪ E ∪ X be consistent, and Φ be an executability or an effect law such that S |= PDL Φ. If T is modular, then T ′ |= PDL Φ for every T ′ ∈ T - Φ Thus, under modularity our operators satisfy the success postulate (C3). Still under modularity and the assumption that the classical contraction operator satisfies Katsuno and Mendelzon's (C4) postulate, our operations also satisfy it: and vice-versa. Thanks to modularity, our operators also satisfy Katsuno and Mendelzon's (C5) postulate, recovery: Theorem 10 Let T be modular. T ′ ∪ {Φ} |= PDL T, for all T ′ ∈ T - Φ . Theorem 11 If T is modular, then every T ′ ∈ T - Φ is also modular. Besides satisfying all postulates for contraction, our operators also preserve modularity. This is a nice property, since it means that modularity can be checked/ensured once for all during the theory's evolution.

Theorem 9 Let T 1 and T 2 be modular. If |= PDL T 1 ↔ T 2 and |= PDL Φ 1 ↔ Φ 2 , then for each T ′ 1 ∈ (T 1 ) - Φ2 there is T ′ 2 ∈ (T 2 ) - Φ1 such that |= PDL T ′ 1 ↔ T ′ 2 ,

Related Work

To the best of our knowledge, the first work on updating action theories is that by [START_REF] Li | What is believed is what is explained[END_REF] in a narrativebased action description language [START_REF] Gelfond | Representing action and change by logic programs[END_REF]. Contrary to us, however, they investigate the problem of updating the narrative with new observed facts and (possibly) with occurrences of actions that explain those facts.

This amounts to updating a given state/configuration of the world (in our terms, what is true in a possible world) and focusing on the models of the narrative in which some actions took place (in our terms, the models of the action theory with a particular sequence of action executions). Clearly the models of the action laws remain the same. [START_REF] Liberatore | A framework for belief update[END_REF] proposes an action language in which one can express a given semantics for belief update, like [START_REF] Winslett | Reasoning about action using a possible models approach[END_REF]) and (Katsuno and Mendelzon 1992). Update operations are then expressed as action laws in a theory.

The main difference between Liberatore's work and Li and Pereira's is that Liberatore's framework allows for abductively adding to the action theory new effect propositions (effect laws, in our terms) that consistently explain the occurrence of an event.

The work by [START_REF] Eiter | Updating action domain descriptions[END_REF]) is similar to ours in that they also propose a framework for updating action laws. They mainly investigate the case where e.g. a new effect law shall be added to the description. This problem is the dual of contraction and is then closer to revision.

In Eiter et al.'s approach, action theories are also described in a variant of a narrative-based action language. Like here, the semantics is in terms of transition systems. Contrary to us, the minimality condition on the outcome of the update is in terms of inclusion of sets of laws, which means the approach is more syntax-oriented than ours.

Both their framework and ours can be qualified as constraint-based update, in that the update is carried out relative to a set of laws that one wants to hold in the result.

Here for example, all changes in the action laws are relative to the static laws in S .

One difference between our approach and Eiter et al.'s is that there it is also possible to update a theory relatively to e.g. executability laws: when expanding T with a new effect law, one may want to constrain the change so that the action under concern is guaranteed to be executable in the result. This may of course require the withdrawal of some static law. Hence, in Eiter et al.'s framework, static laws do not have the same status as in ours.

Concluding Remarks

The contributions of the present work are as follows:

• What is the meaning of removing a law Φ from an action theory T? How to get minimal change, i.e., how to keep as much knowledge about other laws as possible? We answered these questions with Definitions 6, 10 and 13. • How to syntactically contract an action theory so that its result corresponds to the intended semantics? We answered this question with Algorithms 1-3 and Theorems 4 and 5. • Is our method closer to update or revision? Does it comply with the standard postulates for classical theory change and what are the differences w.r.t. that? We answered these questions with Theorems 6-11.

We have shown the importance that modularity has in action theory change. Under modularity, our operators satisfy all Katsuno and Mendelzon's postulates for contraction. This shows that our modularity notion is fruitful. Moreover, considering future modifications one should perform on the theory, since modularity is preserved by our operators, it suffices to check/ensure it only once.

Here we presented the case for contraction. We are currently investigating the definition of the revision counterpart of action theory change. The first results on this issue are available in (Varzinczak 2008b).

Our ongoing research is on how to contract not only laws but any PDL-formula. Definitions 4, 8 and 11 show up to be important for better understanding the case of general formulas: the modifications to perform in a given model in order to falsify a general formula will also comprise removal/addition of arrows and worlds. The definition of a more general contraction method will thus benefit from our present constructions. Now let Φ be of the form ϕ → [a]ψ, for ϕ, ψ ∈ Fml. u ′ ψ. Because u ϕ, there is v ∈ base(ϕ, W ′ ) such that v ⊆ u, and as u ′ ¬ψ, there must be v ′ ∈ base(¬ψ, W ′ ) such that v ′ ⊆ u ′ . Let π = ℓ∈v ℓ, ϕ A = ℓ∈u\v ℓ, and π ′ = ℓ∈v ′ ℓ. Clearly π (resp. π ′ ) is a prime implicant of S ∧ ϕ (resp. S ∧ ¬ψ).

Then M ′ = W ′ , R ′ , where W ′ = W, R ′ = R ∪ R ϕ,¬ψ
Now let E - a = 1≤i≤n (E ϕ,ψ a ) i and let the theory Let now Φ be some propositional ϕ. Then M ′ = W ′ , R ′ , where W ⊆ W ′ , R ′ = R, is minimal w.r.t. M , i.e., W ′ is a minimum superset of W such that there is u ∈ W ′ with u ϕ. Because we have assumed the syntactical classical contraction operator is correct w.r.t. its semantics and is moreover minimal, then there must be S -∈ S ⊖ ϕ such that W ′ = val(S -). Hence |= M ′ S -. As R ′ = R, every effect law of T remains true in M ′ . Now, let

T ′ = (T \ E - a ) ∪ {(ϕ i ∧ ¬(π ∧ ϕ A )) → [a]ψ i : ϕ i → [a]ψ i ∈ E - a } ∪ {(ϕ i ∧ π ∧ ϕ A ) → [a](ψ i ∨ π ′ ) : ϕ i → [a]ψ i ∈ E - a } ∪    (π ∧ ϕ A ∧ ℓ) → [
T ′ = ((T \ S ) ∪ S -) \ X a ∪ {(ϕ i ∧ ϕ) → a ⊤ : ϕ i → a ⊤ ∈ X a } ∪ {¬ϕ → [a]⊥}
(Clearly, T ′ is a theory produced by Algorithm 3.)

For every (ϕ i ∧ ϕ) → a ⊤ ∈ T ′ and every w ∈ W ′ , if |=

Figure 2 Figure 2 :

 22 Figure 2: The big model for the coffee machine scenario.

Figure 3 :

 3 Figure 3: Models resulting from contracting the executability law token → buy ⊤ in the model M of Figure 2.

Figure 4 :

 4 Figure 4: Candidate ¬hot-worlds to receive arrows from token-worlds. When pointing a new arrow leaving a world w it is enough to preserve old effects only in w (because the remaining structure of the model keeps unchanged after adding this new arrow). The operation we must carry out is observing what is true in w and in the candidate target world w ′ : what changes from w to w ′ (w ′ \ w) must be what is obliged to do so; what does not change from w to w ′ (w ∩ w ′ ) must be what is either obliged or allowed to do so.This means that the only things allowed to change w.r.t. w in the candidate target world are those that are forced to change: they are relevant to ¬ψ or to another effect that applies in w. Every change outside that is not an intended one. Similarly, we want the literals preserved in the target world to be those that are relevant to ¬ψ or to some other effect that applies in w or that are usually preserved in w. Every preservation outside those may make us lose some law.Here is where prime subvaluations play their role: the worlds one should aim the new arrow at are those whose difference w.r.t. w are literals that are relevant, and whose similarity w.r.t. w are literals we know may not change.

Figure 5 :

 5 Figure 5: Models resulting from contracting the effect law token → [buy]hot in the model M of Figure 2. The new arrows are the dashed ones.

Figure 6 :

 6 Figure 6: Models resulting from contracting the static law coffee → hot in the model M of Figure 2. The new added coffee ∧ ¬hot-worlds are dashed.

Algorithm 3

 3 Contraction of a static law input: T, ϕ output: T - ϕ /* a set of theories */ if S |= CPL ϕ then for all S -∈ S ⊖ ϕ do

  w, w ′ ) : w ′ ∈ RelTgt(w, ϕ → [a]ψ, M , M)} for some M = W, R ∈ M. Let u ∈ W ′ be such that |= M ′ u ϕ → [a]ψ. Then there is u ′ ∈ W ′ such that (u, u ′ ) ∈ R ′ a and |= M ′

  a](ψ ∨ ℓ) : ℓ ∈ L, for L ⊆ Lit s.t. S |= CPL (π ′ ∧ ℓ∈L ℓ) → ⊥, andℓ ∈ π ′ or T |= PDL (π ∧ ϕ A ∧ ℓ) → [a]¬ℓ    (Clearly, T ′ is a theory produced by Algorithm 2.)In order to show that M ′ is a model of T ′ , it is enough to show that it is a model of the added laws. Given(ϕ i ∧ ¬(π ∧ ϕ A )) → [a]ψ i ∈ T ′ , for every w ∈ W ′ , if |= T |= PDL (π ′ ∧ ℓi∈L ′ ℓ i ) → ⊥, and, because T is modular, S |= CPL (π ′ ∧ ℓi∈L ′ ℓ i ) → ⊥, and then Algorithm 2 has not put the law (π ∧ ϕ A ∧ ℓ) → [a](ψ ∨ ℓ) in T ′ , a contradiction. Then u ′′ ∈ W ′ , and moreover u ′′ / ∈ R ϕ,¬ψ a (u), otherwise M ′ is not minimal. As u ′′ \ u ⊂ u ′ \ u, the only reason why u ′′ / ∈ R ϕ,¬ψ a (u) is that there is ℓ ′ ∈ u ∩ u ′′ such that |= Mi ℓj ∈u ℓ j → [a]¬ℓ ′ for every M i ∈ M if and only if ℓ ′ / ∈ v ′ for any v ′ ∈ base(¬ψ, W ′ ) such that v ′ ⊆ u ′′ . Clearly ℓ ′ = ℓ,and because ℓ / ∈ π ′ , we have |= Mi ℓj ∈u ℓ j → [a]¬ℓ for every M i ∈ M. Then T |= PDL (π ∧ ϕ A ∧ ℓ) → [a]¬ℓ, and Algorithm 2 has not put the law (π ∧ ϕ A ∧ ℓ) → [a](ψ ∨ ℓ) in T ′ , contradiction. Hence we have |= M ′ w ′ ψ ∨ ℓ for every w ′ ∈ W ′ such that (w, w ′ ) ∈ R ′ a . Putting the above results together, we get |= M ′ T ′ .

  conditions for the other connectives are as usual. By M we will denote a set of PDL-models. M is a model of Φ (noted |= M Φ) if and only if |= M w Φ for all w ∈ W. M is a model of a set of formulas Σ (noted |=

M Σ) if and only if |= M Φ for every Φ ∈ Σ. Φ is a consequence of the global axioms Σ in all PDL-models (noted Σ |= PDL Φ) if and only if for every M , if |= M Σ, then |= M Φ.

  and only if v W ϕ and {|ℓ| : ℓ ∈ v} ⊆ E!(ϕ).

	Definition 2 Let ϕ ∈ Fml and W be a set of valuations. A
	subvaluation v is a prime subvaluation of ϕ (modulo W) if
	and only if v	! W ϕ and there is no v ′ ⊆ v s.t. v ′ ! W ϕ.
	A prime subvaluation of a formula ϕ is one of the weakest
	states of truth in which ϕ is true. (Notice the similarity with
	the syntactical notion of prime implicant (Quine 1952).)
	By base(ϕ, W) we denote the set of all prime subvalua-
	tions of ϕ modulo W.
	Theorem 2 Let ϕ ∈ Fml and W be a set of valuations. Then
	for all w ∈ W, w ϕ if and only if w	v∈base(ϕ,W) ℓ∈v ℓ.

  where each M ′

					i
	is as depicted in Figure 6.
			¬t, c, h	t, c, ¬h
		b		b
	M ′ 1 :	t, c, h	b	t, ¬c, h
	¬t, ¬c, ¬h	t, ¬c, ¬h	¬t, ¬c, h
			¬t, c, h
	M ′ 2 :	t, c, h		t, ¬c, h
	¬t, ¬c, ¬h	t, ¬c, ¬h	¬t, ¬c, h

case Algorithm 2 has not put the law(π ∧ ϕ A ∧ ℓ) → [a](ψ ∨ ℓ) in T ′ , a contradiction;• or ¬ℓ ∈ u ′ \v ′ . In this case, there is a valuation u ′′ = (u ′ \ {¬ℓ}) ∪ {ℓ} such that u ′′ ψ. We must have u ′′ ∈ W ′ , otherwise there will be L ′ = {ℓ i : ℓ i ∈ u ′′ } such that

Acknowledgements

The author is thankful to Andreas Herzig and Laurent Perrussel for interesting discussions on the subject of this work. He is also grateful to the anonymous referees for their useful comments on an earlier version of this paper. This work has been partially supported by a fellowship from the government of the FEDERATIVE REPUBLIC OF BRAZIL. Grant: CAPES BEX 1389/01-7.

For the proof of this lemma, the reader is invited to check (Varzinczak 2008a).

Proof of Theorem 4

Let M = {M :|= M T}, and M ′ ∈ M -Appendix B: Proof of Theorem 5

Lemma 2 Let Φ be a law. If T is modular, then every T ′ ∈ T - Φ is modular. Proof: Let Φ be nonclassical, and suppose there is

where S ′ is the set of static laws in T ′ . By Lemma 1, T |= PDL T ′ , and then we have T |= PDL ϕ ′ . Because Φ is nonclassical, S ′ = S . Thus S |= CPL ϕ ′ , and hence T is not modular.

Let now Φ be some ϕ ∈ Fml. Then

Suppose T is modular, and let ϕ ′ ∈ Fml be such that

and as T is modular, T |= PDL ϕ ′ . By Lemma 1, T |= PDL T ′ , and we have T ′ |= PDL ϕ ′ , a contradiction. Hence v / ∈ val(S ). Moreover, we must have v ϕ, otherwise ⊖ has not worked as expected.

Let

and then T ′ is modular.

For the proof of the following three lemmas, please refer to (Varzinczak 2008a).

Lemma 4 Let T be modular, and Φ be a law. Then T |= PDL Φ if and only if every

Lemma 5 Let T be modular, Φ a law, and

for some M ′ ∈ M - Φ .

Proof of Theorem 5

From the hypothesis that T is modular and Lemma 2, T ′ is modular. Then M ′ = val(S ′ ), R is a model of T ′ , by Lemma 4. From this and Lemma 5 the result follows.


Ivan José Varzinczak
email: ivan.varzinczak@irit.fr

Action Theory Revision in Dynamic Logic

Like any other logical theory, action theories in reasoning about actions may evolve, and thus need revision methods to adequately accommodate new information about the behavior of actions. Here we give a semantics that complies with minimal change for revising action theories stated in a version of PDL. We give algorithms that are proven correct w.r.t. the semantics for those theories that are modular.

Introduction

In logic-based approaches to reasoning about actions, theories are collections of statements of the form: "if context, then effect after every execution of action" (effect laws); and "if precondition, then action executable" (executability laws). For example, in Propositional Dynamic Logic (PDL) [START_REF] Harel | Dynamic Logic[END_REF], one could have the law (¬p 1 ∧¬p 2 ) → [a]p 1 , saying that in every context where ¬p 1 ∧¬p 2 is the case, after every execution of action a we get the effect p 1 ; and (p 1 ∨ ¬p 2 ) → a ⊤, stating that p 1 ∨ ¬p 2 is a sufficient condition for a's executability.

These are examples of what we call action laws, as they specify the behavior of the actions of a given domain. Besides that we can also have laws mentioning no action at all (static laws). They characterize the underlying structure of the world, i.e., its possible states. For instance, having p 1 → p 2 as a static law would mean p 1 ∧ ¬p 2 is a forbidden state. Action theories will then be collections of laws, each of them seen as a global axiom in PDL.

Well, it may happen that such descriptions have to be revised due e.g. to new incoming information about the behavior of the world. In our example, we may learn that the only valid states are those satisfying p 1 ∧ p 2 , or that action a has always ¬p 2 as outcome in ¬p 2 -contexts, or even that p 1 is enough to guarantee a's executability. Here we are interested in this kind of theory change.

The contributions of the present work are as follows: • What is the semantics of revising an action theory T by a law Φ? How to get minimal change, i.e., how to keep as much knowledge about other laws as possible?

Copyright c 2008, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

• How to syntactically revise an action theory so that its result corresponds to the intended semantics?

Here we answer these questions.

Logical Preliminaries Action Theories in Dynamic Logic

Our base formalism is PDL without the * operator. Let Act = {a 1 , a 2 , . . .} be the set of atomic actions of a domain. To each a there is associated a modal operator [a]. We suppose our multimodal logic is independently axiomatized, i.e., the logic is a fusion and there is no interaction between the modal operators [START_REF] Kracht | Properties of independently axiomatizable bimodal logics[END_REF]. Prop = {p 1 , p 2 , . . .} denotes the set of all propositional constants or atoms. The set of literals is Lit = {ℓ 1 , ℓ 2 , . . .}, where each ℓ i is either p or ¬p, for some p ∈ Prop. In case ℓ = ¬p, we identify ¬ℓ with p. By |ℓ| we will denote the atom in literal ℓ.

By ϕ, ψ, . . . we denote Boolean formulas, examples of which are p 1 → p 2 and ¬p 1 ⊕ p 2 . Fml is the set of all Boolean formulas. A propositional valuation v is a maximally consistent set of literals. We denote v ϕ the fact that v satisfies ϕ. val(ϕ) is the set of all valuations satisfying ϕ. |= CPL denotes the classical consequence relation.

With IP(ϕ) we denote the set of prime implicants [START_REF] Quine | The problem of simplifying truth functions[END_REF] of ϕ. By π we denote a prime implicant, and atm(π) is the set of atoms occurring in π. For given ℓ and π, ℓ ∈ π abbreviates 'ℓ is a literal of π'.

We denote complex formulas (with modal operators) by Φ, Ψ, . . . a is the dual operator of With PDL we can state laws describing the behavior of actions. Following the tradition in the reasoning about actions community, we here distinguish three types of them.

[a], ( a Φ = def ¬[a]¬Φ). An example of a complex formula is (p 1 ∧ (p 2 ∨ ¬p 3 )) → [a](¬p 1 ∨ p 3 ). A PDL-model is a tuple M = W, R where W is a set of valuations, and R maps action constants a to accessibility relations R a ⊆ W × W. Given a model M , |= M w p (p is true at world w of model M ) if w p; |= M w [a]Φ if |= M w ′ Φ for every w ′ s.t. (w, w ′ ) ∈ R a ; truth

Static Laws

A static law is a formula ϕ ∈ Fml. It characterizes the possible states of the world. The set of all static laws of a domain is denoted by S .

Effect Laws An effect law for a is of the form ϕ → [a]ψ, where ϕ, ψ ∈ Fml. Effect laws relate an action to its effects, which can be conditional. The consequent ψ is the effect which always obtains when a is executed in a state where the antecedent ϕ holds. If a is a nondeterministic action, then ψ is typically a disjunction. If ψ is inconsistent we have a special kind of effect law that we call an inexecutability law. For example, (¬p 1 ∧ p 2 ) → [a]⊥ says that a cannot be executed (there is no a-transition) in ¬p 1 ∧ p 2 -contexts. The set of effect laws of a domain is denoted by E .

Executability Laws An executability law for a has the form ϕ → a ⊤, with ϕ ∈ Fml. It stipulates the context in which a is guaranteed to be executable. (In PDL, the operator a is used to express executability, a ⊤ thus reads "a's execution is possible".) The set of all executability laws of a domain is denoted by X .

Action Theories

T = S ∪ E ∪ X is an action theory.
Given an action a, E a (resp. X a ) will denote the set of only those effect (resp. executability) laws about a. For the sake of clarity, we here abstract from the frame and ramification problems, and assume T contains all frame axioms (cf. [START_REF] Herzig | Elaborating domain descriptions[END_REF] for a contraction approach within a solution to the frame problem).

Elementary Atoms and Prime Valuations

Given ϕ ∈ Fml, E(ϕ) denotes the elementary atoms actually occurring in ϕ. For example, E(¬p

1 ∧ (¬p 1 ∨ p 2 )) = {p 1 , p 2 }. An atom p is essential to ϕ if and only if p ∈ E(ϕ ′ ) for every ϕ ′ such that |= CPL ϕ ↔ ϕ ′ . For instance, p 1 is es- sential to ¬p 1 ∧ (¬p 1 ∨ p 2 ). E!(ϕ) will denote the essential atoms of ϕ. (If ϕ is not contingent, i.e., it is a tautology or a contradiction, then E!(ϕ) = ∅.) For ϕ ∈ Fml, ϕ * is the set of all ϕ ′ ∈ Fml such that ϕ |= CPL ϕ ′ and E(ϕ ′ ) ⊆ E!(ϕ). For instance, p 1 ∨ p 2 / ∈ p 1 * , as p 1 |= CPL p 1 ∨ p 2 but E(p 1 ∨ p 2 ) ⊆ E!(p 1 ). Moreover E(ϕ * ) = E!(ϕ * ), and whenever |= CPL ϕ ↔ ϕ ′ , E!(ϕ) = E!(ϕ ′ ) and also ϕ * = ϕ ′ * .
Theorem 1 (Least atom-set theorem (Parikh 1999))

|= CPL ϕ ↔ ϕ * , and E(ϕ * ) ⊆ E(ϕ ′ ) for every ϕ ′ s.t. |= CPL ϕ ↔ ϕ ′ .
Thus for each ϕ ∈ Fml there is a unique least set of elementary atoms such that ϕ may equivalently be expressed using only atoms from that set.1

Given a valuation

v, v ′ ⊆ v is a subvaluation. For W a set of valuations, a subvaluation v ′ satisfies ϕ ∈ Fml modulo W (noted v ′ W ϕ) if and only if v ϕ for all v ∈ W such that v ′ ⊆ v. A subvaluation v essentially satisfies ϕ (modulo W), noted v ! W ϕ, if and only if v W ϕ and {|ℓ| : ℓ ∈ v} ⊆ E!(ϕ). If v ! W ϕ,

Closeness Between Models

When revising a model, we will perform a change in its structure. Because there can be several different ways of modifying a model (not all of them minimal), we need a notion of distance between models to identify those that are closest to the original one.

As we are going to see in more depth in the sequel, changing a model amounts to modifying its possible worlds or its accessibility relation. Hence, the distance between two PDL-models will depend upon the distance between their sets of worlds and accessibility relations. These here will be based on the symmetric difference between sets, defined as

X -Y = (X \ Y ) ∪ (Y \ X). Definition 2 Let M = W, R be a model. M ′ = W ′ , R ′ is as close to M as M ′′ = W ′′ , R ′′ , noted M ′ M M ′′ , if and only if • either W -W ′ ⊆ W -W ′′ • or W -W ′ = W -W ′′ and R -R ′ ⊆ R -R ′′
(Notice that other distance notions are also possible, like e.g. considering the cardinality of symmetric differences.)

Semantics of Revision

Contrary to action theory contraction (Varzinczak 2008a), where we want the negation of some law to become satisfiable, in revision we want to make a new law valid. This means that one has to eliminate all cases satisfying its negation. This depicts the duality between revision and contraction: whereas in the latter one invalidates a formula by making its negation satisfiable, in the former one makes a formula valid by forcing its negation to be unsatisfiable prior to adding the new law to the theory.

The idea behind our semantics is as follows: we initially have a set of models M in which a given formula Φ is (potentially) not valid, i.e., Φ is (possibly) not true in every model in M. In the result we want to have only models of Φ. Adding Φ-models to M is of no help. Moreover, adding models makes us to lose laws: the corresponding resulting theory would be more liberal.

One solution amounts to deleting from M those models that are not Φ-models. Of course removing only some of them does not solve the problem, we must delete every such a model. By doing that, all resulting models will be models of Φ. (This corresponds to theory expansion, when the resulting theory is satisfiable.) However, if M contains no model of Φ, we will end up with ∅. Consequence: the resulting theory is inconsistent. (This is the main revision problem.) In this case the solution is to substitute each model M in M by its nearest modification M * Φ that makes Φ true. This lets us to keep as close as possible to the original models we had. But, what if for one model in M there are several minimal (incomparable) modifications of it validating Φ? In that case we shall consider all of them. The result will also be a list of models M * Φ , all being models of Φ. Before defining revision of sets of models, we present what modifications of (individual) models are.

Revising a Model by a Static Law

Consider the model depicted in Figure 1, and suppose we want to revise it by the Boolean formula p 1 ∨ p 2 , i.e., we want such a formula to be a static law. In such a model, we do not want the formula ¬p 1 ∧ ¬p 2 to be satisfiable, so the first step is to remove all worlds in which it is true. The second step is to guarantee that all the remaining worlds satisfy the new law. Such an issue has been largely addressed in the literature on propositional belief base revision and update [START_REF] Gärdenfors | Knowledge in Flux: Modeling the Dynamics of Epistemic States[END_REF][START_REF] Winslett | Reasoning about action using a possible models approach[END_REF][START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF][START_REF] Herzig | Propositional belief base update and minimal change[END_REF].

M :

p 1 , ¬p 2 ¬p 1 , p 2 ¬p 1 , ¬p 2 a a a
Here we can achieve that with a semantics similar to that of classical operators: basically one shall change the set of possible valuations, by removing or adding worlds.

The delicate point in removing worlds is that we may lose some executability laws: in the example, removing {¬p 1 , ¬p 2 } also removes p 2 → a ⊤. From a semantic point of view, this is intuitive: if the state of the world to which we could move is no longer possible, then we do not have a transition to that state anymore. Hence, if that transition was the only one we had, it is natural to lose it.

Similarly, one could ask what to do with the accessibility relation if new worlds are added (when expansion is not possible): shall new arrows leave/arrive at the new world? If no arrow leaves the new added world, we may lose an executability law. If some arrow leaves it, we may lose an effect law, the same holding if we add an arrow pointing to the new world. If no arrow arrives at this new world, what about the intuition? Do we want to have an unreachable state?

All this discussion shows how drastic a change in the static laws may be: it is a change in the underlying structure (possible states) of the world! Changing it may have as consequence the loss of an effect law or an executability law.

The tradition in the reasoning about actions community says that executability laws are, in general, more difficult to state than effect laws, and hence are more likely to be incorrect. By adding no arrow to the resulting model we here comply with that and postpone correction of executability laws, if needed (cf. [START_REF] Herzig | Elaborating domain descriptions[END_REF]Varzinczak 2008a)).

The semantics for revision of one model by a static law is as follows:

Definition 3 Let M = W, R . M ′ = W ′ , R ′ ∈ M * ϕ if and only if: • W ′ = (W \ val(¬ϕ)) ∪ val(ϕ) • R ′ ⊆ R Clearly |= M ′ ϕ for each M ′ ∈ M * ϕ .
The minimal models resulting from revising a model M by ϕ are those closest to M w.r.t. M :

Definition 4 revise(M , ϕ) = min{M * ϕ , M }

Revising a Model by an Effect Law

Let our language now have three atoms and consider the model M in Figure 2.

M :

p 1 , ¬p 2 , ¬p 3 ¬p 1 , p 2 , p 3 p 1 , p 2 , ¬p 3 a a a Figure 2: A model where p 1 ∧ a p 2 is satisfiable. (Notice that |= M p 2 → p 1 ⊕ p 3 .
) Suppose we want to revise M by p 1 → [a]¬p 2 . This means that we should guarantee the formula p 1 ∧ a p 2 is satisfiable in none of its worlds. To do that, we have to look at the worlds satisfying it (if any) and either make p 1 false, or make a p 2 false by removing a-arrows leading to p 2 -worlds.

In our example, the worlds {p 1 , ¬p 2 , ¬p 3 } and {p 1 , p 2 , ¬p 3 } satisfy p 1 ∧ a p 2 and both have to change. Flipping p 1 would do the job but also has as consequence the loss of a static law: we would violate p 2 → p 1 ⊕p 3 . Here we think that changing action laws should not have as side effect a change in the static laws. Given their special status, these should change only if explicitly required (see above). In this case, each world satisfying p 1 ∧ a p 2 has to be changed so that a p 2 is no longer true in it. In our example, we should remove the arrows

({p 1 , ¬p 2 , ¬p 3 }, {¬p 1 , p 2 , p 3 }) and ({p 1 , p 2 , ¬p 3 }, {p 1 , p 2 , ¬p 3 }).
The semantics of one model revision for the case of a new effect law is:

Definition 5 Let M = W, R . M ′ = W ′ , R ′ ∈ M * ϕ→[a]ψ
if and only if:

• W ′ = W • R ′ ⊆ R • If (w, w ′ ) ∈ R \ R ′ , then |= M w ϕ and |= M w ′ ¬ψ • |= M ′ ϕ → [a]ψ
The minimal models resulting from the revision of a model M by a new effect law are those that are closest to M w.r.t. M :

Definition 6 Let M be a model and ϕ → [a]ψ an effect law. Then revise(M , ϕ → [a]ψ) = min{M * ϕ→[a]ψ , M }.

Revising a Model by an Executability Law

Let the model depicted in Figure 3 and suppose we want to revise it by the new executability law p 1 → a ⊤.

M :

p 1 , p 2 p 1 , ¬p 2 ¬p 1 , p 2 ¬p 1 , ¬p 2 a a a Figure 3: A model where p 1 ∧ [a]⊥ is satisfiable.
Observe that ¬(p 1 → a ⊤) is satisfiable in M , hence we must throw p 1 ∧[a]⊥ away to ensure the new formula is true. To remove p 1 ∧ [a]⊥ we have to look at all worlds satisfying it and modify M so that they no longer satisfy the formula. Given world {p 1 , ¬p 2 }, we have two options: change the interpretation of p 1 or add a new arrow leaving this world. A question that raises is 'what choice is more drastic: change a world or an arrow'? Again, here we think that changing the world's content (the valuation) is more drastic, as the existence of such a world was foreseen by some static law and is hence assumed to be as it is, unless we have information supporting the contrary (see above). Thus we shall add a new a-arrow from {p 1 , ¬p 2 }. Having agreed on that, the issue now is: to which world should the new arrow point? Four options show up: point the arrow to {p 1 , p 2 }, {¬p 1 , p 2 }, {¬p 1 , ¬p 2 } or {p 1 , ¬p 2 } itself. The resulting model is such that the unwanted formula is unsatisfiable and p 1 → a ⊤ holds in all its worlds.

Whereas all these options make the new law true in the resulting model, not all of them comply with minimal change. To witness, putting an a-arrow from {p 1 , ¬p 2 } to {¬p 1 , ¬p 2 } or {p 1 , ¬p 2 } makes us lose the effect law ¬p 2 → [a]p 2 ; and pointing it to {¬p 1 , p 2 } also deletes from the model p 1 → [a]p 1 . Note that these laws are preserved if we point the arrow to {p 1 , p 2 }. What would support the choice for the latter?

When pointing a new arrow leaving a world w we want to preserve as many effects as we had before doing so. To achieve this, it is enough to preserve old effects only in w (because the remaining structure of the model remains unchanged after adding this new arrow). The operation we must carry out is to observe what is true in w and in the candidate target world w ′ :

• What changes from w to w ′ (w ′ \ w) must be what is obliged to do so. • What does not change from w to w ′ (w∩w ′ ) must be what is either obliged or allowed to do so. This means that every change outside what is forced to change is not an intended one. In our example, when putting the a-arrow from {p 1 , ¬p 2 } to {¬p 1 , p 2 }, ¬p 1 becomes a possible effect of a. As far as ¬p 1 is never caused by a, there is no justification for having it in a target world of {p 1 , ¬p 2 }. Similarly, we want the literals preserved in the target world to be at most those that either are consequences of some effect or are usually preserved in that context. Every preservation outside those may make us lose some law. For instance, when putting the new a-arrow from {p 1 , ¬p 2 } to {¬p 1 , ¬p 2 }, ¬p 2 is preserved. Because ¬p 2 is not a necessary effect of a and is moreover never preserved across a's execution (in M ), there is no reason to preserve it in this new a-transition.

This looks like prime implicants, and that is where prime subvaluations play their role: the worlds to which the new arrow shall point are those whose difference w.r.t. the departing world are literals that are relevant, and whose similarity w.r.t. it are literals that we know do not change.

Before giving a formal definition for that, we need to consider two important issues: First, when checking satisfaction of these two conditions, looking just at what is true in the model M we want to modify is not enough. It can be a model in which a contingent, i.e., not true in all models formula is true. Hence we shall consider all the models in M. Second, if a is never executable in w, i.e., R a (w) = ∅ for every M = W, R ∈ M, then lots of effects for a trivially hold in w, and then not all of them should be taken into account in deciding what has to be changed or preserved. In this case, one should instead look at the effects that hold for those worlds w such that R a (w) = ∅ (because everything that holds in these worlds also holds trivially in those worlds with no transition by a). Definition 7 Let M = W, R be a model, w, w ′ ∈ W, M a set of models such that M ∈ M, and ϕ → a ⊤ an executability law. Then w ′ is a relevant target world of w w.r.t. ϕ → a ⊤ for M in M if and only if:

• |= M w ϕ • If there is M ′ = W ′ , R ′ ∈ M such that R ′ a (w) = ∅: -for all ℓ ∈ w ′ \ w, there is ψ ′ ∈ Fml s.t. there is v ′ ∈ base(ψ ′ , W) s.t. v ′ ⊆ w ′ , ℓ ∈ v ′ ,

and for every

M i ∈ M, |= Mi w [a]ψ ′ -for all ℓ ∈ w ∩ w ′ , either there is ψ ′ ∈ Fml s.t. there is v ′ ∈ base(ψ ′ , W) s.t. v ′ ⊆ w ′ , ℓ ∈ v ′ ,

and for all

M i ∈ M, |= Mi w [a]ψ ′ ; or there is M i ∈ M s.t. |= Mi w [a]¬ℓ • If R ′ a (w) = ∅ for every M ′ = W ′ , R ′ ∈ M: -for all ℓ ∈ w ′ \ w, there is M i = W i , R i ∈ M s.t. there is u, v ∈ W i s.t. (u, v) ∈ R ia and ℓ ∈ v \ u -for all ℓ ∈ w ∩ w ′ , there is M i = W i , R i ∈ M s.t. there is u, v ∈ W i s.t. (u, v) ∈ R ia and ℓ ∈ u ∩ v, or for all M i = W i , R i ∈ M, if (u, v) ∈ R ia , then ¬ℓ / ∈ v \ u
By RelTgt(w, ϕ → a ⊤, M , M) we denote the set of all relevant target worlds of w w.r.t. ϕ → a ⊤ for M in M.

The semantics of one model revision by a new executability law is given by:

Definition 8 Let M = W, R . M ′ = W ′ , R ′ ∈ M *
ϕ→ a ⊤ if and only if:

• W ′ = W • R ⊆ R ′ • If (w, w ′ ) ∈ R ′ \ R, then w ′ ∈ RelTgt(w, ϕ → a ⊤, M , M) • |= M ′ ϕ → a ⊤
The minimal models resulting from revising a model M by a new executability law are those closest to M w.r.t. M : Definition 9 Let M be a model and ϕ → a ⊤ be an executability law. Then revise(M , ϕ → a ⊤) = min{M * ϕ→ a ⊤ , M }.

Revising Sets of Models

Now we are ready to define revision of a set of models M by a new law Φ:

Definition 10 Let M be a set of models and Φ a law. Then

M * Φ = M \ {M : |= M Φ}, if there is M ∈ M s.t. |= M Φ
M ∈M revise(M , Φ), otherwise Observe that Definition 10 comprises both expansion and revision: in the first one, simple addition of the new law gives a satisfiable theory; in the latter a deeper change is needed to get rid of inconsistency.

Syntactic Operators for Revision

We now turn our attention to the syntactical counterpart of revision. Suppose we have an action theory T and a law Φ we want to revise T with. If T ∪ {Φ} is satisfiable, adding Φ to T (expansion) will do the job. Otherwise, if T ∪ {Φ} |= PDL ⊥, then we have to modify the laws in T to accommodate with the new incoming law (proper revision). Our endeavor here is to perform minimal change at the syntactical level. By T * Φ we denote the result of revising T with Φ.

Revision by a Static Law

Looking at the semantics of revision by Boolean formulas, we see that revising an action theory by a new static law may conflict with the executability laws: some of them may be lost and thus have to be changed as well. The approach here is to preserve as many executabilities as we can in the old possible states. To do that, we look at each possible valuation that is common to the new S and the old one. Every time an executability used to hold in that state and no inexecutability holds there in the new theory, we make the action executable in such a context. For those contexts not allowed by the old S , we make a inexecutable (cf. the semantics). Algorithm 1 deals with that (S ⋆ ϕ denotes the classical revision of S by ϕ using any standard method from the literature [START_REF] Winslett | Reasoning about action using a possible models approach[END_REF][START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF][START_REF] Herzig | Propositional belief base update and minimal change[END_REF]).

Algorithm 1 Revision by a static law

input: T, ϕ output: T * ϕ if T ∪ {ϕ} |= PDL ⊥ then T * ϕ := T ∪ {ϕ} else S ′ := S ⋆ ϕ, E ′ := E , X ′ := ∅ for all π ∈ IP(S ′ ) do for all A ⊆ atm(π) do ϕA:= V p i ∈atm(π) p i ∈A p i ∧ V p i ∈atm(π) p i / ∈A ¬p i if S ′ |= CPL (π ∧ ϕA) → ⊥ then if S |= CPL (π ∧ ϕA) → ⊥ then if T |= PDL (π ∧ ϕA) → a ⊤ and S ′ , E ′ , X |= PDL ¬(π ∧ ϕA) then X a ′ := {(ϕi ∧ π ∧ ϕA) → a ⊤ : ϕi → a ⊤ ∈ X a } else E ′ := E ′ ∪ {(π ∧ ϕA) → [a]⊥} T * ϕ := S ′ ∪ E ′ ∪ X ′

Revision by an Effect Law

When revising a theory by a new effect law ϕ → [a]ψ, we want to eliminate all possible executions of a leading to ¬ψstates. To achieve that, we look at all ϕ-contexts and every time a transition to some ¬ψ-context is not always the case, i.e., T |= PDL ϕ → a ¬ψ, we can safely force [a]ψ for that context. On the other hand, if in such a context there is always an execution of a to ¬ψ, then we should strengthen the executability laws to make room for the new effect in that context we want to add. Algorithm 2 below does the job.

Revision by an Executability Law

Revising a theory by a new executability law will have as immediate consequence a change in the set of effect laws: all those laws preventing the execution of a shall be weakened. Besides that, in order to comply with minimal change, we shall ensure that in all models of the resulting theory there will be at most one transition by a from those worlds in which T precluded a's execution.

Let E ϕ,⊥ a denote a minimum subset of E a such that S , E ϕ,⊥ a |= PDL ϕ → [a]⊥.
In the case the theory is modular [START_REF] Herzig | On the modularity of theories[END_REF]) (see further), interpolation guarantees that this set always exists. Moreover, note that there can be more than one such a set, in which case we denote them

(E ϕ,⊥ a ) 1 , . . . , (E ϕ,⊥ a ) n . Let E - a = 1≤i≤n (E ϕ,⊥ a ) i
Algorithm 2 Revision by an effect law

input: T, ϕ → [a]ψ output: T * ϕ→[a]ψ if T ∪ {ϕ → [a]ψ} |= PDL ⊥ then T * ϕ→[a]ψ := T ∪ {ϕ → [a]ψ} else T ′ := T for all π ∈ IP(S ∧ ϕ) do for all A ⊆ atm(π) do ϕA:= V p i ∈atm(π) p i ∈A p i ∧ V p i ∈atm(π) p i / ∈A ¬p i if S |= CPL (π ∧ ϕA) → ⊥ then for all π ′ ∈ IP(S ∧ ¬ψ) do if T ′ |= PDL (π ∧ ϕA) → a π ′ then T ′ := (T ′ \ X ′ a ) ∪ {(ϕi ∧ ¬(π ∧ ϕA)) → a ⊤ : ϕi → a ⊤ ∈ X ′ a } T ′ := T ′ ∪ {(π ∧ ϕA) → [a]ψ} if T ′ |= PDL (π ∧ ϕA) → [a]⊥ then T ′ := T ′ ∪{(ϕi ∧π ∧ϕA) → a ⊤ : ϕi → a ⊤ ∈ T} T * ϕ→[a]ψ := T ′
The effect laws in E - a will serve as guidelines to get rid of [a]⊥ in each ϕ-world allowed by the theory: they are the laws to be weakened to allow for a ⊤.

The idea behind our algorithm is as follows: to force ϕ → a ⊤ to be true in all models of the resulting theory, we visit every possible ϕ-context allowed by it and make the following operations to ensure a ⊤ is the case for that context: Given a ϕ-context, if T not always precludes a from being executed in it, we can safely force a ⊤ without modifying other laws. On the other hand, if a is always inexecutable in that context, then we should weaken the laws in E - a . The first thing we must do is to preserve all old effects in all other ϕ-worlds. To achieve that we specialize the above laws to each possible valuation (maximal conjunction of literals) satisfying ϕ but the actual one. Then, in the current ϕ-valuation, we must ensure that action a may have any effect, i.e., from this ϕ-world we can reach any other possible world. We achieve that by weakening the consequent of the laws in E - a to the exclusive disjunction of all possible contexts in T. Finally, to get minimal change, we must ensure that all literals in this ϕ-valuation that are not forced to change are preserved. We do this by stating a conditional frame axiom of the form (ϕ k ∧ ℓ) → [a]ℓ, where ϕ k is the above ϕ-valuation.

Algorithm 3 gives the pseudo-code for that.

Correctness of the Algorithms

Suppose we have two atoms p 1 and p 2 , and only one action a. Let the action theory

T 1 = {¬p 2 , p 1 → [a]p 2 , a ⊤}.
The only model of T 1 is M in Figure 4. Revising such a model by p 1 ∨ p 2 gives us the models 4. This means that the semantic revision produces models (viz. M ′ 2 and M ′ 3 in Figure 4) that are not models of the revised theories. The other way round, the algorithms may produce theories whose models do not result from the semantic revision of some model of the original theory. As an example, consider

M ′ i , 1 ≤ i ≤ 3, in Figure 4. Now, revising T 1 by p 1 ∨ p 2 will give us T 1 * p 1 ∨p 2 = {p 1 ∧ ¬p 2 , p 1 → [a]p 2 }. The only model of T 1 * p 1 ∨p 2 is M ′ 1 Algorithm 3 Revision by an executability law input: T, ϕ → a ⊤ output: T * ϕ→ a ⊤ if T ∪ {ϕ → a ⊤} |= PDL ⊥ then T * ϕ→ a ⊤ := T ∪ {ϕ → a ⊤} else T ′ := T for all π ∈ IP(S ∧ ϕ) do for all A ⊆ atm(π) do ϕA:= V p i ∈atm(π) p i ∈A p i ∧ V p i ∈atm(π) p i / ∈A ¬p i if S |= CPL (π ∧ ϕA) → ⊥ then if T ′ |= PDL (π ∧ ϕA) → [a]⊥ then T ′ := (T ′ \ E ′- a ) ∪ {(ϕi ∧ ¬(π ∧ ϕA)) → [a]ψi : ϕi → [a]ψi ∈ E ′- a } ∪ {(ϕi ∧ π ∧ ϕA) → [a] L π ′ ∈IP(S ) A ′ ⊆atm(π ′ ) (π ′ ∧ ϕ A ′ ) : ϕi → [a]ψi ∈ E ′- a } for all L ⊆ Lit do if S |= CPL (π ∧ ϕA) → V ℓ∈L ℓ then for all ℓ ∈ L do if T |= PDL ℓ → [a]⊥ or (T ⊢ PDL ℓ → [a]¬ℓ and T |= PDL ℓ → [a]ℓ) then T ′ := T ′ ∪ {(π ∧ ϕA ∧ ℓ) → [a]ℓ} T ′ := T ′ ∪ {(π ∧ ϕA) → a ⊤} T * ϕ→ a ⊤ := T ′ in Figure
M : ¬p 1 , ¬p 2 a M ′ 1 : p 1 , ¬p 2 M ′ 2 : ¬p 1 , p 2 M ′ 3 : p 1 , p 2
T 2 = {(p 1 ∨ p 2 ) → [a]⊥, a ⊤}, whose only model is M in Figure 4. The revision of M by p 1 ∨ p 2 is as above. However T 2 * p 1 ∨p 2 = {p 1 ∨ p 2 , (p 1 ∨ p 2 ) → [a]⊥} has a model M ′′ = {{p 1 , p 2 }, {p 1 , ¬p 2 }, {¬p 1 , p 2 }}, ∅ that is not in M *
p 1 ∨p 2 . This happens because the possible states are not completely characterized by the static laws in S . Fortunately we get the right result by requiring S to be 'big enough'. This is connected with the principle of modularity [START_REF] Herzig | On the modularity of theories[END_REF] Under modularity, revision of models of T by a law Φ in the semantics produces models of the output of the algorithms T * Φ : Theorem 3 Let T be modular and Φ be a law. For all models M ′ , if M ′ ∈ M * Φ , for some M = {M :|= M T}, then

|= M ′
T * Φ . Also under modularity, models of T * Φ result from revision of models of T by Φ: Theorem 4 Let T be modular and Φ a law. For every

M ′ , if |= M ′ T * Φ , then M ′ ∈ M * Φ , for some M = {M :|= M T}.
In [START_REF] Herzig | On the modularity of theories[END_REF] algorithms are given to check whether T satisfies the principle of modularity and also to make T satisfy it, if that is not the case.

Modular theories have other interesting properties [START_REF] Herzig | Metatheory of actions: beyond consistency[END_REF]: for example, consistency amounts to that of S ; deduction of effect laws does not need the executability ones and vice versa; prediction of an effect of a sequence of actions a 1 ; . . . ; a n does not need the effect laws for actions other than a 1 , . . . , a n . This also applies to plan validation when deciding whether a 1 ; . . . ; a n ϕ is the case.

Conclusion and Perspectives

Contrary to classical belief change, the problem of action theory change has only recently received attention in the literature, both in action languages [START_REF] Baral | Defeasible specifications in action theories[END_REF][START_REF] Eiter | Updating action domain descriptions[END_REF] and in dynamic logic [START_REF] Herzig | Elaborating domain descriptions[END_REF]Varzinczak 2008a).

Here we have studied what revising action theories by a law means, both in the semantics and at the syntactical level. We have defined a semantics based on distances between models that also captures minimal change w.r.t. the preservation of effects of actions. With our algorithms and the correctness results under modularity we have established the link between the semantics and the syntax, and have also shown that the modularity notion is fruitful. Since modularity is preserved across revision (see Lemma 1 in the appendices), it has to be ensured only once during the evolution of the action theory.

Here we presented the case for revision. In (Varzinczak 2008a) we also define the contraction counterpart of action theory change. There we show that moreover our constructions satisfy all Katsuno and Mendelzon's postulates for contraction [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF].

Our next step on the subject is to define a general framework in which to revise a theory by any formula of the language and not only laws. We believe that such a definition will use as basic operations semantic modifications like those we studied here (addition/removal of arrows and worlds). Hence our constructions will help us in better understanding what revision by a general formula means.

Proof of Theorem 3

Let Φ be a law, M ′ ∈ M * Φ , and let T * Φ be the output of our algorithms on input theory T and law Φ.

If T ∪ {Φ} |= PDL ⊥, then M ′ ∈ M \ {M : |= M Φ} and M ′ is a model of T * Φ = T ∪ {Φ}. Let T ∪ {Φ} |= PDL ⊥. We analyze each case. Let Φ be some ϕ ∈ Fml. Then M ′ = W ′ , R ′ where W ′ = (W\ val(¬ϕ))∪val(ϕ) is minimal w.r.t. W and R ′ ⊆ R is maximal w.r.t. R, for some M = W, R ∈ M.
As we have assumed the syntactical classical revision operator ⋆ is sound and complete w.r.t. its semantics and is moreover minimal, we have |=

M ′ S ⋆ ϕ. Because R ′ ⊆ R, |= M ′ E . Thus it is enough to show that M ′ is a model of the added laws. Given (ϕ i ∧ π ∧ ϕ A ) → a ⊤ ∈ T * ϕ , for every w ∈ W ′ , if |= M ′ w ϕ i ∧π∧ϕ A , then w ∈ W (because S |= CPL (π∧ϕ A ) → ⊥). From w ϕ i and ϕ i → a ⊤ ∈ X a , we have R a (w) = ∅. Suppose R ′ a (w) = ∅. As |= M ′ S ⋆ ϕ ∪ E and R ′ is maximal, every M ′′ = W ′′ , R ′′ s.t. |= M ′′ S ⋆ ϕ ∪ E is s.t. R ′′ a (w) = ∅, and then S ⋆ ϕ ∪ E |= PDL (π ∧ ϕ A ) → [a]⊥. Because T |= PDL (π ∧ ϕ A ) → a ⊤, and S |= CPL (π ∧ ϕ A ) → ⊥ and S ⋆ϕ |= CPL (π ∧ϕ A ) → ⊥, we get S ⋆ϕ, E , X |= PDL ¬(π ∧ϕ A ), and then (ϕ i ∧ π ∧ ϕ A ) → a ⊤ / ∈ T * ϕ . Hence R ′ a (w) = ∅, and |= M ′ (ϕ i ∧ π ∧ ϕ A ) → a ⊤. If (π ∧ ϕ A ) → [a]⊥ ∈ T * ϕ , then S |= CPL (π ∧ ϕ A ) → ⊥. Thus, for every w ∈ W ′ , if |= M ′ w π ∧ ϕ A , R ′ a (w) = ∅ and the result follows. Let Φ now have the form ϕ → [a]ψ, for ϕ, ψ ∈ Fml. Then M ′ = W ′ , R ′ for some M = W, R ∈ M s.t. W ′ = W and R ′ ⊆ R, where R ′ is maximal w.r.t. R. From W ′ = W, |= M ′ S . As R ′ ⊆ R, |= M ′ E . Because S ∪ E ⊆ T * ϕ→[a]ψ , it suffices to show that M ′ is a model of the added laws. By definition, |= M ′ ϕ → [a]ψ, and then |= M ′ (π ∧ ϕ A ) → [a]ψ for every π ∈ IP(S ∧ ϕ). If (ϕ i ∧ π ∧ ϕ A ) → a ⊤ ∈ T * ϕ→[a]ψ , then for every w ∈ W ′ , if w ϕ i ∧ π ∧ ϕ A , we have w ϕ i . As w ∈ W, and ϕ i → a ⊤ ∈ X a , R a (w) = ∅. If R ′ a (w) = ∅, then w ′
¬ψ for every w ′ ∈ R a (w). Thus as far as we added

(π ∧ ϕ A ) → [a]ψ to T * ϕ→[a]ψ , we must have T * ϕ→[a]ψ |= PDL (π ∧ ϕ A ) → [a]⊥. Hence R ′ a (w) = ∅. Let (ϕ i ∧ T|= PDL (π∧ϕA)→ a ¬ψ ¬(π ∧ ϕ A )) → a ⊤ ∈ T * ϕ→[a]ψ . For every w ∈ W ′ , if |= M ′ w ϕ i ∧ T|= PDL (π∧ϕA)→ a ¬ψ ¬(π ∧ ϕ A )
, then w ϕ i , and as

w ∈ W and ϕ i → a ⊤ ∈ X a , we have R a (w) = ∅. If R ′ a (w) = ∅, because |= M ′
S ∧ E and R ′ is maximal, every

M ′′ = W ′′ , R ′′ s.t. |= M ′′ S ∧ E is s.t. R ′′ a (w) = ∅. Then S , E |= PDL ℓ∈w ℓ → [a]⊥. But then T |= PDL ℓ∈w ℓ → [a]⊥, and as ϕ i → a ⊤ ∈ X a , T |= PDL ¬( ℓ∈w ℓ ∧ ϕ i ), and then w / ∈ W, a contradiction. Hence R ′ a (w) = ∅. Finally, let Φ be of the form ϕ → a ⊤, for some ϕ ∈ Fml. Then M ′ = W ′ , R ′ for some M = W, R ∈ M s.t. W ′ = W and R ′ = R ∪ R ϕ,⊤ a , with R ϕ,⊤ a = {(w, w ′ ) : w ′ ∈ RelTgt(w, ϕ → a ⊤, M , M)} such that R ′ is minimal w.r.t. R. From W ′ = W, |= M ′ S . As R ⊆ R ′ , |= M ′ X . As far as S ∪ X ⊆ T * ϕ→ a ⊤ , it is enough to show that M ′ satisfies the added laws. By definition, |= M ′ ϕ → a ⊤, and then |= M ′ (π ∧ ϕ A ) → a ⊤ for every π ∈ IP(S ∧ ϕ). If (ϕ i ∧ π ∧ ϕ A ) → [a](ψ i ∨ π ′ ∈IP(S ) A ′ ⊆atm(π ′ ) (π ′ ∧ ϕ A ′ )) ∈ T * ϕ→ a ⊤ , then for every w ∈ W ′ , if w ϕ i ∧ π ∧ ϕ A , then w ϕ i . Because |= M ϕ i → [a]ψ i , we have |= M w ′ ψ i for all w ′ ∈ W s.t. (w, w ′ ) ∈ R a , and then |= M ′ w ′ ψ i for every w ′ ∈ W ′ s.t. (w, w ′ ) ∈ R ′ a \ R ϕ,⊤ a . Now, given (w, w ′ ) ∈ R ϕ,⊤ a , we have |= M ′ w ′ π ′ ∈IP(S ) A ′ ⊆atm(π ′ ) (π ′ ∧ ϕ A ′ ),

Proof of Theorem 4

Lemma

Figure 1 :

 1 Figure1: A model where ¬p 1 ∧ ¬p 2 is satisfiable.

Figure 4 :

 4 Figure 4: The model M of T and the semantic revision of M by p 1 ∨ p 2 .

  and the result follows.Let (ϕ i ∧ T|= PDL (π∧ϕA)→[a]⊥ ¬(π ∧ ϕ A )) → [a]ψ i ∈ T * ϕ→ a ⊤ .For every w ∈ W ′ , if |= →[a]⊥ ¬(π∧ϕ A ), then w ϕ i , and as|= M ϕ i → [a]ψ i , we have |= M w ′ ψ i for all w ′ ∈ W s.t. (w, w ′ ) ∈ R a . Thus |= M ′ w ′ ψ i for every w ′ ∈ W ′ s.t. (w, w ′ ) ∈ R ′ a \ R ϕ,⊤ a . Now, if w ϕ, then R ϕ,⊤ a = ∅ and the result follows. Otherwise, if w ϕ, then T |= PDL (π ∧ ϕ A ) → [a]⊥, and then (ϕ i ∧ T|= PDL (π∧ϕA)→[a]⊥ ¬(π ∧ ϕ A )) → [a]ψ i has not been put in T * ϕ→ a ⊤ , a contradiction. Let now (π ∧ ϕ A ∧ ℓ) → [a]ℓ ∈ T * ϕ→ a ⊤ . For every w ∈ W ′ , if |= M ′ w π ∧ ϕ A ∧ ℓ, then |= M ′ w ℓ, and then |= M w ℓ. From (π ∧ ϕ A ∧ ℓ) → [a]ℓ ∈ T * ϕ→ a ⊤ , we have T |= PDL ℓ → [a]⊥ or T |= PDL ℓ → [a]¬ℓ and T |= PDL ℓ → [a]ℓ. In both cases, |= M w ′ ℓ for every w ′ ∈ R a (w), and then |= M ′ w ′ ℓ for every w ′ s.t. (w, w ′ ) ∈ R ′ \ R ϕ,⊤ a . It remains to show that |= M ′ w ′ ℓ for every w ′ ∈ W ′ s.t. (w, w ′ ) ∈ R ϕ,⊤ a . Suppose |= M ′ w ′ ℓ. Then ¬ℓ ∈ w ′ \ w. From the construction of M ′ , there is M ′′ = W ′′ , R ′′ ∈ M s.t. there is (u, v) ∈ R ′′ a and ¬ℓ ∈ v\u, i.e., |= M ′′ u ℓ and |= M ′′ v ¬ℓ. From (u, v) ∈ R ′′ a , we do not have T |= PDL ℓ → [a]⊥. From |= M ′′ v ¬ℓ, we do not have T |= PDL ℓ → [a]ℓ. Thus the algorithm has not put (π ∧ ϕ A ∧ ℓ) → [a]ℓ in T * ϕ→ a ⊤ , a contradiction.

  conditions for the other connectives are as usual. By M we will denote a set of PDL-models. M is a model of Φ (noted |=

	M w Φ for all w ∈ W. M is a model of a set of formulas Σ (noted |= M Σ)
	if and only if |=

M Φ) if and only if |= M Φ for every Φ ∈ Σ. Φ is a consequence of the global axioms Σ in all PDL-models (noted Σ |= PDL Φ) if and only if for every M , if |= M Σ, then |= M Φ.

  we call v an essential subvaluation of ϕ (modulo W).

	Definition 1 Let ϕ ∈ Fml and W be a set of valuations. v is
	a prime subvaluation of ϕ (modulo W) if and only if v and there is no v ′ ⊆ v s.t. v ′ ! W ϕ.	! W ϕ
	Prime subvaluations of a formula ϕ are the weakest states
	of truth in which ϕ is true. They are just another way of
	seeing prime implicants of ϕ. By base(ϕ, W) we denote the
	set of all prime subvaluations of ϕ modulo W.
	Theorem 2 Let ϕ ∈ Fml and W be a set of valuations. Then
	for all w ∈ W, w ϕ if and only if w	v∈base(ϕ,W) ℓ∈v ℓ.

: Definition 11 (Modularity (Herzig and Varzinczak 2005))

  T is modular if and only if for every ϕ ∈ Fml, if T |= PDL ϕ, then S |= CPL ϕ.

1

  Let Φ be a law. If T is modular and T ∪ {Φ} |= PDL ⊥, then T * Φ is modular. Proof: Let Φ be nonclassical. Suppose T * Φ is not modular. Then there is ϕ′ ∈ Fml s.t. T * ϕ |= PDL ϕ ′ and S ′ |= CPL ϕ ′ , where S ′ is static laws in T * Φ . Suppose T |= PDL ϕ ′ . Then we must have T * Φ |= PDL ¬ϕ ′ → [a]⊥ and T * Φ |= PDL ¬ϕ ′ → a ⊤. Suppose Φ has the form ϕ → [a]ψ, for ϕ, ψ ∈ Fml.Then for all ϕ∧¬ϕ ′ -contexts, as far asT * Φ |= PDL (ϕ∧¬ϕ ′ ) → [a]⊥, (ϕ ∧ ¬ϕ ′ ) → a ⊤ / ∈ T * Φ . Then T * Φ |= PDL ϕ ′ if and only if S ′ |= CPL ϕ ′ , a contradiction. Suppose Φ is of the form ϕ → a ⊤, for ϕ ∈ Fml. Then for all ϕ∧¬ϕ ′ -contexts such that T * Φ |= PDL (ϕ∧¬ϕ ′ ) → a ⊤, T * Φ |= PDL (ϕ ∧ ¬ϕ ′ ) → [a]⊥is impossible as far as E - a has been weakened. Then T * Φ |= PDL ϕ ′ if and only if S ′ |= CPL ϕ ′ , a contradiction. Hence we have T |= PDL ϕ ′ . Because Φ is nonclassical, S ′ = S . Then T |= PDL ϕ ′ and S |= CPL ϕ ′ , and hence T is not modular. Let now Φ be some ϕ ∈ Fml. Suppose T * ϕ is not modular, i.e., there is ϕ ′′ ∈ Fml s.t. T * ϕ |= PDL ϕ ′′ and S ′ = S ⋆ ϕ |= CPL ϕ ′′ . From S ′ |= CPL ϕ ′′ , there is v ∈ val(S ′ ) s.t. v ϕ ′′ . If v ∈ val(S ), as T is modular, T |= PDL ϕ ′′ . From this and T * ϕ |= PDL ϕ ′′ , we must have T * ϕ |= PDL ¬ϕ ′′ → [a]⊥ and T * ϕ |= PDL ¬ϕ ′′ → a ⊤. From the latter, we get T |= PDL ¬ϕ ′′ → a ⊤, and from the first we have T |= PDL ¬ϕ ′′ → [a]⊥. Putting both results together we get T |= PDL ϕ ′′ . As S |= CPL ϕ ′′ , we have a contradiction. If v / ∈ val(S ), then T * ϕ |= PDL ¬ϕ ′′ → a ⊤, as no executability for context ¬ϕ ′′ has been put into T *

The dual notion (redundant atoms) is addressed in[START_REF] Herzig | Propositional belief base update and minimal change[END_REF], with similar purposes.

Acknowledgements

The author is thankful to Andreas Herzig and Laurent Perrussel for interesting discussions on the subject of this work.

This work has been partially supported by the government of the FEDERATIVE REPUBLIC OF BRAZIL. Grant: CAPES BEX 1389/01-7.