# nondeterminism_and_the_dynamics_of_knowledge__92439cb7.pdf

Non-Determinism and the Dynamics of Knowledge

Davide Grossi1, Andreas Herzig2, Wiebe van der Hoek1, Christos Moyzes1

1University of Liverpool, UK 2Universit e Paul Sabatier, IRIT, CNRS, France 1{dgrossi, wiebe, cmoyzes}@liverpool.ac.uk

In this paper we attempt to shed light on the concept of an agent s knowledge after a non-deterministic action is executed. We start by making a comparison between notions of non-deterministic choice, and between notions of sequential composition, of settings with dynamic and/or epistemic character; namely Propositional Dynamic Logic (PDL), Dynamic Epistemic Logic (DEL), and the more recent logic of Semi-Public Environments (SPE). These logics represent two different approaches for defining the aforementioned actions, and in order to provide unified frameworks that encompass both, we define the logics DELVO (DEL+Vision+Ontic change) and

PDLVE (PDL+Vision+Epistemic operators). DELVO is given a sound and complete axiomatisation.

1 Introduction The paper focuses on the dynamics of knowledge in environments where agents are aware of (possibly non-deterministic) actions that are executed, but data is distributed privately: Semi-Public Environments as they are called, more recently in [Grossi et al., 2016] and earlier in [van der Hoek et al., 2011]. By data being distributed privately we mean that the agents may or may not have constant, real-time knowledge, of the value of the variables involved. The paper sets out to investigate how non-deterministic choice in this type of environments affects the knowledge of an agent after an action is executed. Non-deterministic choice is a central action composition operator for most logics of action. In this paper our starting points will be Propositional Dynamic Logic (PDL, [Harel et al., 2000]), Dynamic Epistemic Logic with Action Models (DEL, [van Ditmarsch et al., 2007], [Baltag and Moss, 2004; Baltag et al., 1998]) and the aforementioned logic for Semi-Public Environments (SPE, [Grossi et al., 2016]). For the presentation to follow, the reader is assumed to be familiar with DEL. In DEL and PDL, for any actions a and b of the respective language, we have the validity ([a]ϕ [b]ϕ) [a b]ϕ. (1) If ϕ expresses knowledge, e.g. is Kiψ, the scheme expresses a strong relation between knowledge and non-determinism: an agent knows ψ after non-deterministically executing a or

b, if and only if he knows ψ after executing just a and after executing just b. In DEL, an instance of (1) is [x!](Kix Kiy) [y!](Kix Kiy) [x! y!](Kix Kiy). This property makes perfect sense; after being announced that x, or being announced that y, the agent at least knows one of the two to be true. Another interesting instance of (1), however, should arguably fail. That is what happens in

SPE, where the following formula is not valid (let Kw ix be shorthand for Kix Ki x, and x:= (respectively, ) stands for the action of setting variable x to false (respectively, true): [x:= ]Kw ix [x:= ]Kw ix [x:= x:= ]Kw ix. The failure of (1) in SPE also has an intuitive appeal: some part of a non-deterministic action is executed, but which part is actually performed is not necessarily revealed to the agent. So, in contrast to what happens in DEL (or PDL extended with epistemic operators), it is not the case that if the agent knows ψ after executing a and after executing b, that he necessarily knows ψ after the execution of the non-deterministic choice between them. A similar analysis applies to sequential composition. In the same fashion as before, we have the validity that essentially defines sequential composition in PDL: [a; b]ϕ [a][b]ϕ. (2) And in DEL, we have that formula [x!; y!]Ki(x y) [x!][y!]Ki(x y) is a validity, for x, y being atoms. This is again intuitive: announcing x y ought to be the same as announcing x and then announcing y. But also this schema is not valid in SPE; we very briefly refer to an example from [Grossi et al., 2016] below. In its perspective the failure of (2) should not come as a surprise.

Example 1 The agent can see only variable x, and we execute the action where we non-deterministically toggle the values of x and y, or just y. After this action, we also nondeterministically toggle the value of x, or of y.

In both steps the agent can distinguish between the two possible actions; one changes x, the other does not. Consider that the agent has the opportunity to observe the impact of the first action, before the second starts, and then the impact of the second. As a result, he can distinguish between any of the four total alternatives (where both x and y, or just x, or just y, or nothing, was changed; for later use let us denote the four individual actions with v1, v2, v3, v4 respectively). But

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

what if the agent has no opportunity to observe what happened in-between? Then he can only observe what happened at the very end, and in our example, he will not be able to distinguish between all possibilities, particularly those with same truth value for x, but different for y. The paper introduces and studies a logic that integrates both the above approaches to choice and composition, defining two novel action operators which we call opaque choice and composition. The proposed logic is a generalisation of both SPE and DEL and is called DELVO: DEL plus vision plus ontic change, which are features of SPE. Logic DELVO is then compared with an extension of PDL with vision and epistemic modalities we also introduce (called PDLVE). This logic can be considered the natural abstraction of DELVO in PDL style, in the sense that the actions involved will be arbitrary connections between possible worlds (as opposed to the other dynamic logic, DL-PA [Balbiani et al., 2013], that uses assignments). The relationship between DELVO and PDLVE is studied in detail. The drawing below recapitulates the relations among the investigated logics.

Th. 2 Th. 3

2 Preliminaries

Throughout the paper, we will be dealing with a finite set Ag = {1, . . . , m} of agents, and a countable set of propositional variables Var = {x1, x2, . . . }. A valuation θ : Var {true, false} assigns a truth value to each variable x Var. The set of all valuations is denoted by Θ. Given a relation R A A, R is its reflexive, symmetric, and transitive closure. For S A, R(S) = {w A | v S s.t. v Rw}. Let us next give a summary of the notation for the different classes of models we will be using, given that several logics are involved in this study.

DEL SPE DELVO PDL PDLVE Static Models EM EMV EMV DM DEM Dynamic Models A model M from any of the above classes, has a set of worlds/points W. We then have single-pointed models to be pairs of the form (M, w), for w W, and multi-pointed models to be pairs of the form (M, S), for S W. We will use the prefix σ or µ, and the name of a class in brackets, to denote the corresponding classes of single-pointed and multi-pointed models (e.g., µ( ) stands for multi-pointed action models). To justify the abbreviations: EM stands for Epistemic Models, EMV for the Epistemic Models with Vision, DM for Dynamic Models and DEM for Dynamic Epistemic Models, for Action Models, for Action Models with Toggle sets, for Program Models. We recapitulate the basic notions of DEL, we refer the reader to [van Ditmarsch et al., 2007, Ch. 6] for a comprehensive exposition. Let L be a logical language for given parameters Ag and Var. An action model M is a tuple W, R, pre such that W is a finite set, R : Ag 2(W W) assigns an equivalence relation to each agent i Ag, and pre : W L. We will denote the class of action models for LDEL with . Language LDEL

is given by syntax ϕ ::= x | ϕ | ϕ ϕ | Kiϕ | [a]ϕ, where x Var, i Ag and a ::= (M, w) | (a a) where w W. An epistemic model for LDEL is M = W, R, f , where W is a (possibly empty) set, the set of states; f : W Θ assigns a valuation θ to each state in W; R : Ag 2(W W ) assigns an equivalence relation to each agent i Ag. EM denotes the class of epistemic models. The model resulting from the application of an action model M to an epistemic model M, referred to here as model product, is the model M M = W , R , f such that W = {(w, w) W W | M, w |= pre(w)}, (w, w)R (u, u) iff w Ru and w Ru. and f(w, w) = f(w). Actions of DEL are defined by syntax a ::= (M, w) | a a. Finally, for each action a, we have the induced relation [|a|]: for M, w σ( ) we have (M, w)[|M, w|](M , w ) iff M, w |= pre(w) and (M , w ) = (M M, (w, w)), while [|a b|] = [|a|] [|b|]. We have M, w |= [a]ϕ iff for all M , w [|a|](M, w) we have M , w |= ϕ. The rest of the truth definitions are as usual. Let us denote the actions of DEL with LAct 1 . In the remainder of the section we define an equivalent presentation of DEL based on multi-pointed action models. This allows us to have a unified model structure to handle all actions of LAct 1 , which facilitates later comparison with SPE. So let us consider the language LAct 2 where actions are only multi-pointed action models, that is, a ::= M, S where M, S µ( ); and the language of DEL using LAct 2 denoted by L DEL . Now the induced relation is defined as [|M, S|](M, w) = {M M, (w, w) | w S}. In what follows, denotes the disjoint union of two action models, whose sets of worlds are, for simplicity, already assumed to be disjoint. Definition 1 (Translation to µ( )) We define function t : LAct 1 7 LAct 2 = µ( ) as follows: If M, w σ( ), then t(M, w) = M, {w}. If a, b LAct 1 and t(a) = Ma, Sa, t(b) = Mb, Sb, then t(a b) = Ma Mb, Sa Sb. The fact that this translation is truth-preserving is formally stated in the following Theorem. Theorem 1 For all ϕ LDEL let t(ϕ) denote the formula that is ϕ but for each action a all its occurrences in ϕ are replaced by t(a). For all M, w σ(EM) and ϕ LDEL, we have M, w |= ϕ iff M, w |= t(ϕ). 3 The Logic DELVO The first traditional setting on which we would like to expand and incorporate both alternative versions of choice and composition mentioned in the introductory section is DEL. The difference in behaviour we have observed relies on vision that is, what agents can observe and ontic change that is, the factual differences among points of evaluation in the model. It thus seems reasonable to introduce a DEL-style logic, with epistemic models enriched with vision, and action models that allow for ontic change. Definition 2 (Toggling values) Let θ Θ and S Var. The toggling of values for the variables in S in θ, notation (S)(θ), is the atomic valuation (member of Θ) defined as (S)(θ)(x) = not θ(x) if x S, otherwise (S)(θ)(x) = θ(x). Given two sets of variables S1 and S2, we denote their symmetric difference by S1 S2 , i.e., S1 S2 = (S1 S2) \ (S1 S2).

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

Definition 3 (DELVO Action Models) A (DELVO) action model is a tuple M = W, R, pre, tgl , where W = is finite, R : Ag 2(W W) assigns an equivalence relation to each agent i Ag, pre : W L, tgl : W P(Var) and each tgl(w) is finite. A pair (M, S), where M is an action model and S W, is called a (Multi-)Pointed Action Model. When clear from context, instead of M, {w} we may also write M, w. The class of all action models is denoted by .

In comparison with the standard manifestation of postcondition effects in DEL, which uses assignments (see for example [van Benthem et al., 2006]), our action models use toggle sets, as in [Grossi et al., 2016]. The reason is that it allows for a more elegant handling of the notion of vision, since the agent successfully resolves uncertainty based on the difference in ontic changes caused by the actions. The two formulations are technically equivalent: one can simulate assignments to variables using toggle sets [Grossi et al., 2016]. Pairs (M, S) now are essentially the multi-pointed action models of DEL, but with each point w carrying additional information about a finite toggle set tgl(w). Finally the syntax of formulas ϕ LDELVO is: ϕ ::= | x | Vix | ϕ | ϕ ϕ | [M, S]ϕ | Kiϕ where x Var, i Ag, (M, S) µ( ).

Definition 4 (DELVO models) An epistemic model (with vision) M for LDELVO is a tuple M = W, R, V, f where W, R, f EM, V : Ag 2Var, and w Riu implies (f(w) f(u)) V (i) = . EMV denotes the class of epistemic models with vision. The set of all vision functions V is denoted by Vis.

So the models of DELVO are standard epistemic models enhanced with a vision function recording information about which propositional variables each agent observes. If an agent considers two worlds indistinguishable, then it must be the case that he cannot observe a difference in their valuation. There exists the possibility that the indistinguishability relation of an action model is not compatible with the vision function of an epistemic model. The way we address these cases when trying to calculate a model product, is by rewiring the action models to be in sync with the agents vision, but without them hiding any information at all, or giving information not acquired by vision.

Definition 5 Let V Vis and M . We define the action model MV = WV , RV , pre V , tgl V as follows: WV = W; pre V = pre; tgl V = tgl; w RV i u iff w Riu and tgl(w) tgl(u) V (i) = .

Now that we have everything else in place, we proceed to define the semantics of formulas and actions in DELVO.

Definition 6 Let M = W, R, V, f EMV. The truth conditions are as for DEL, plus (M, w) |= Vix iff x V (i). Relation [|M, S|] σ(EMV) σ(EMV) is defined again as in DEL: [|M, S|](M, w) = {M M, (w, w) | w S}, while (M M) is now the epistemic model M = W , R , V , f defined as: W = {(w, w) | w W, w W & (M, w) |= pre(w)}; (w, w)R i(u, u) iff w Riu and w RV i u;

V = V , f ((w, w)) = tgl(w) f(w) . We conclude the section thus far by introducing a notion of bisimulation between DELVO models [Blackburn et al., 2001]. Definition 7 Let M, M EMV. A non-empty relation Z W W is a bisimulation iff for all (w, w ) Z and i Ag: Atoms For all x V ar, x f(w) iff x f (w ), and x V (i) iff x V (i); Forth For all v W, if w Riv then there is a v W such that w R iv and (v, v ) Z; Back For all v W , if w R iv then there is a v W such that w Riv and (v, v ) Z. Two multi-pointed action models (M, S) and (M , S ) are bisimilar (written (M, S) (M , S )) iff there is a bisimulation Z between M and M , such that for any w S, there is a w S with (w, w ) Z, and vice versa.

Axiomatisation The axiomatisation for DELVO is comprised of the axioms and rules for logic S5, axioms for vision Vix (Kix Ki x) and Vix Kj Vix, and reduction axioms that allow any formula that includes dynamic modalities to be reduced to one that does not. These reduction axioms are identical to those of SPE [Grossi et al., 2016], except the slightly changed reduction action for knowledge: [M, w]Kiϕ pre(w) V V Vis M(χV V w RV i u Ki[MV, u]ϕ) , with χV being a characteristic formula of vision function V over the variables that appear in M. Soundness is derived easily from the definitions, and completeness is proven along the lines of

DEL and SPE via the standard reduction technique; completeness is then further reduced to that of logic S5+V, that is, the multi-agent epistemic logic S5n [Fagin et al., 1995], with the two additional axioms for vision.

Opaque Choice and Composition The logic DELVO provides us with a setting in which to properly capture not only the traditional forms of choice and composition (cf. Theorem 1) but also their opaque variants opaque choice and composition we motivated in the introductory section. Let the set of actions Act be defined inductively as: Act a ::= ϕ! | ϕ? | x | a a | a T a | a; a | a; ; a, where ϕ L, x Var and T Ag. The constructs T and ; ; denote the opaque variants of the standard and ;. For T = Ag we write omitting the subscript. Each of the above actions we recursively define in terms of suitable DELVO action models. By writing action a in a formula we will mean the multi-pointed action model that corresponds to a. Definition 8 1. (Announcement) Let Mϕ! = W, R, pre, tgl , where W = {e}, Ri = {(e, e)}, pre(e) = ϕ and tgl(e) = {}. The multi-pointed action model for ϕ! is Mϕ!, {e}. 2. (Toggle) Let M x = W, R, pre, tgl , where W = {t}, Ri = {(t, t)}, pre(t) = and tgl(t) = {x}. The multipointed action model for x is M x, {t}. 3. (Test) Let Mϕ? = W, R, pre, tgl , where W = {w, v}, Ri = W W, pre(w) = ϕ, pre(v) = ϕ and tgl(w) = tgl(v) = {}. The multi-pointed action model for ϕ? is Mϕ?, {w}. In order to define test as a multi-pointed action model, we have based ourselves on the archetype that the test relation

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

Figure 1: Epistemic model M (left) for which x V (1), x / V (2), action models ( x !) (top) and ( x !) (bottom), and the resulting model products (right).

represents, in PDL models. Specifically, given a PDL model M, then [|ϕ?|] = {(w, w) M M | M, w |= ϕ}. The relation induced by action models (in our case Def. 6) is not between worlds of the same model, but between the original epistemic model, and the model product. The reader can check that with the action model for test in Definition 8, we have, given M, w σ(EMV), if M, w |= ϕ then [|ϕ?|](M, w) = , and if M, w |= ϕ then [|ϕ?|](M, w) = M Mϕ?, (w, w), and M, w is isomorphic to M Mϕ?, (w, w). The action model for standard non-deterministic choice is a disjoint union of action models, as in DEL (Def. 1).

Definition 9 (Opaque Non-det. Choice) Let a, b Act. The action model for a T b is Ma T b, Sa T b = W , R , pre , tgl , S where, if Ma b, Sa b = W, R, pre, tgl , S : W = W; pre = pre; tgl = tgl; S = S For i T, R i = ( Ri (S S ) ) . For i / T, R i = Ri.

The intuition behind opaque choice compared to standard choice, is that, for agents in T, it overrides any information gained by the distinction between points in S. It can be read as non-deterministically execute one of the action points in S, but, after execution you will only be able to tell between them if your vision allows it . To do this, we simply take the action model of the standard non-deterministic choice, and then connect, for the agents in T, the worlds in S. As mentioned earlier, an agent s uncertainty is bound by the information it acquires by vision (recall M M in Def. 6). Example 2 Consider the epistemic model M with a single world w with x V (1), x / V (2). In Figure 1 we compare the action models x ! and x !, along with the resulting model products. Note that for opaque choice, M, w |= [ x !] Kw 2x while for standard choice M, w |= [ x !]Kw 2x. And for agent 1 that sees x we have M, w |= [ x !]Kw 1x [ x !]Kw 1x. This example demonstrates that both directions of validity (1) fail for opaque choice. Indeed, we have M, w |= [ x]Kw 2x [ !]Kw 2x but M, w |= [ x !]Kw 2x, and similarly M, w |= [ x !] Kw 2x but M, w |= [ x] Kw 2x. The uncertainty of the agent described by the intuition above and portrayed by this example can be described more generally by the following formula: let (M, w), (M , w ) µ( ) and V be the vision function for which agent i can see none of the variables in tgl(w) tgl(w ). Then we have: χV [M, w]x [M , w ] x (pre(w) pre(w ))

[M, w M , w ] Kw ix

We now move on to the subject of sequential composition, which poses some more difficulties. It becomes evident that it is not possible to define regular composition only as a function

of the models Ma, Mb, without vision as a parameter; this is in contrast with the action models and the other constructs defined so far. As proof recall the actions of Example 1: if V (i) = then vj Rivk for 1 j, k 4 in the action model, and for the resulting worlds also (w, vj)Ri(w, vk). If we set V (i) = {x} then the action model would be the same but it should not be the case e.g. that (w, v2)Ri(w, v3). We are therefore led to the following definition.

Definition 10 (Composition) Let V Vis, Ma = Wa, Ra , prea, tgla , Sa and Mb = Wb, Rb, preb, tglb, , Sb. Their composition w.r.t. V is the pointed action model MV a;b, SV a;b = W, R, pre, tgl , S where: W = Wa Wb, S = Sa Sb, (w, w )Ri(v, v ) iff w RV aiv & w RV biv ; pre(w, v) = Ma, w preb(v), tgl(w, v) = tgla(w) tglb(v)

We need not advocate the correctness of the definition regarding W, pre, tgl, and S, as they are what is expected for the composition of two action models in DEL as well as SPE. Vision influences only the accessibility relation R, and regarding that we need only note that it is again the one normally expected, with the exception that the agent has the opportunity to apply his vision after execution of actions a and b. Hence RV ai is used (Def. 5) and not Rai. Finally, let us point out that with this definition a vision function V is linked to an action model directly, and an epistemic model M may have a vision function V = V . In that case, a formula using such an action model cannot be interpreted in M. We do not run into the same kind of problem with opaque composition as it uses the same idea behind opaque choice: it disregards previous connections (or more precisely, the lack thereof) in the model. Intuitively speaking, the agent is absent while actions a and then b are executed, missing any announcements made and also the opportunity to apply his vision as changes occur to the variables.

Definition 11 (Opaque Composition) Let a, b A. The pointed action model for a; ; b is Ma;;b, Sa;;b = W, R, pre, tgl , S defined as in Definition 10 but Ri = W W.

We can now see how to falsify property (2) from the introduction. Consider again the epistemic model of Example 2. Action model for ( x !); ; ! is the action model of ( x !), found in the first row of Figure 1, while in the second row we have the action model of ( x !) and the resulting epistemic model. Applying action ! does not change anything, and so M, w |= [( x !); ; !]Kw 2x, while M, w |= [ x !][ !]Kw 2x.

Relation to DEL and SPE Not coincidentally, the class of

DELVO (static) models i.e. epistemic models with vision is exactly the class of models of SPE, and subsumes the class of standard epistemic models (without vision, that is, where vision is empty), which are the models of DEL. In this section we define the relevant translations among these classes of models and state, without proof, and state the two truth-preserving embeddings.

Definition 12 We define function h : EM EMV as follows: Let M = W, R, f EM. Then h(M) = W, R, V, f , where V is such that for all i AG, V (i) = .

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

Definition 13 Let M, S = W, R, pre , S. We define g : µ( ) µ( ) as g(M, S) = W, R, pre, tgl , S, where tgl is the function such that for all w W, tgl(w) = . Theorem 2 For all ϕ L DEL let g(ϕ) denote the formula that is ϕ but for each action a all its occurrences in ϕ are replaced by g(a). Let M, w σ(EM) and ϕ L DEL. We have M, w |= ϕ iff h(M), w |= g(ϕ). We work similarly for SPE; its models are exactly those of

DELVO, and its action models can be seen as a special case of

DELVO action models. Definition 14 We define function g : σ( ) 7 µ( ) as follows: Let M = {w1 = (ϕ1, X1), . . . , wn = (ϕn, Xn)} and w M. Then g(M, w) = W, R, pre, tgl , {w} where W = {w1, . . . , wn}, pre(wi) = ϕi, tgl(wi) = Xi and Rj = W W. Theorem 3 For all ϕ LSPE let g(ϕ) denote the formula that is ϕ but for each action M, w all its occurrences in ϕ are replaced by g(M, w). Let M, w σ(EMV) and ϕ LSPE. We have M, w |= ϕ iff M, w |= g(ϕ).

4 The Logic PDLVE We now attempt a generalisation of opaque choice and composition to a more abstract PDL-like setting. For DELVO, a large part of the intuitions and formal techniques stem from the use of action models. The latter do not exist in PDL and it is interesting to examine how it would be possible to circumvent their use. Furthermore, actions of PDL are strictly more general; to see this consider that an atomic PDL action can connect a finite component of worlds to an infinite one - this cannot be achieved by any [|M, w|] as action models are finite. Therefore with PDLVE we attempt not only to represent the opaque constructs in the PDL paradigm, but also extent their use to a richer class of actions. In addition to sets Ag and Var, let also a countable set of atomic actions Atom = {a1, a2, . . . } be given. The language of PDLVE is defined by the following syntax: ϕ ::= | x | Vix | ϕ | ϕ ϕ | [a]ϕ | Kiϕ where a ::= π Atom | a a | a a | a; a | a; ; a and x Var, i Ag. We avoid the generalisation for T Ag consciously, so as to not further encumber notation. To capture opaque choice in PDLVE we rely on the basic intuition behind it. Given actions a, b, and world w, either a or b is executed at w, but the agent does not know which, unless his vision allows him to do that . Based on the above, we first give an auxiliary definition: given M EMV and relations for a, b Act, this definition describes a representation of the epistemic model that should be the image of a b. So let M = W, R, V, f EMV. For S W let N(S) denote the epistemic submodel generated by S, and Nw(S) the worlds of that model. We remind that for E W W, E(S) = {w W | v S s.t. v Ew}. Definition 15 Let M = W, R, V, f EMV, and E W W. Let M = N(E(W)) = W , R , V , f . Finally let E be injective and E(W) = W . We then define g(M, E) = W , R , V , f such that: W = W , V = V , f = f , for u E(w), z E(v), we have u R z iff w Rv and (f(w) f (u)) (f(v) f (z)) V (i) =

In words, given a model M and an injective relation E (that is later to play the role of choice or composition between two actions), we first get the epistemic submodel generated by worlds that are an image through E, namely M . Note also that E is such that its co-domain is exactly the set of worlds of M . Then we tinker M to get the model g(M, E), that is the same as M but the agents cannot distinguish between worlds that are images through E (u R z), if and only if the origin worlds were indistinguishable to begin with (w Rv) and their vision does not help them notice a difference in the changes caused among the possible executions; that is, (f(w) f (u)) (f(v) f (z)) V (i) = }. We can now define the class of PDLVE models (denoted by DEM). For brevity, let denote either regular choice or composition, and their opaque variant. Also let (g(M, E), E(w)) = g(M, w, E).

Definition 16 (PDLVE Models) Let M = W, R, E, V, f where W, R, V, f EMV (Def. 4) and E is a family of relations Ea W W, where a is either atomic or of the form b c or b; ; c . Furthermore, E is such that: for a = b c, if Eb c is an injection and Eb c(W) = Nw(Eb c(W)), then N(Ea(w)), Ea(w) g(M, w, Eb c), otherwise Ea = ;

We interpret formulas at pointed dynamic models as usual. And regarding standard choice and composition we define Ea b = Ea Eb and Ea;b = Eb Ea, again as normal. In contrast to what happens with relations Ea b and Ea;b, relations Ea b and Ea;;b are not necessarily expressed only in terms of the source world w, Ea(w), or Eb(w). Different worlds whose names we cannot dictate beforehand may be involved. What we do is therefore require that these worlds are correct , in the sense that they are bisimilar to the corresponding set of worlds in the model that would be the representation (Def. 15) of opaque choice or opaque composition. Is this representation we have chosen a correct one? The next theorem shows that at least as far as a special subset of

DELVO actions is concerned, this is indeed the case. Let, for M EMV, PM = {M, w | w M}.

Theorem 4 Let M, w σ(EMV) and (Ma, Sa), (Mb, Sb) µ( ) such that Ma, Mb are disjoint, [|Ma b, Sa b|](PM) = PM Ma b. Let M = M (M Ma b). Define w Eav iff (M, w)[|Ma, Sa|](M Ma b, v) and similarly for b. Also let M = M g(M , Ea b). Assume that for the disjoint union, every w g(M , Ea b) was renamed to w . Finally, for w M let Ea b(w) = {v | v Ea b(w)}. Then [|Ma b, Sa b|](M, w) M , Ea b(w).

Relation to DELVO We now have two logics for describing knowledge, and epistemic & ontic change. A natural question is whether the actions of PDLVE are more general than those of

DELVO. We find that, under mild restrictions, they are not. As one would expect, the transition from DELVO to PDLVE can be done simply enough. After all DELVO can be reduced to S5+V, and epistemic models with vision are part of PDLVE models. To evaluate a given DELVO formula ϕ in a model M, w σ(EMV), one would have to potentially evaluate subformulas of ϕ in M and in the respective model products.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

The idea for the transition from DELVO to PDLVE, is to define a single PDLVE model by putting together all such models.

Definition 17 Let M σ(EMV) and ϕ LDELVO (M may be omitted when clear from context) by induction on the complexity of ϕ as follows: T1( ) = T1(x) = T1(Vix) = {M}, T1( ϕ) = T1(Kiϕ) = T1(ϕ), T1(ϕ ψ) = T1(ϕ) T1(ψ), T1([M, S]ϕ) = {N M | N T1(ϕ)}. We then define T M 2 (ϕ) = {M EMV | n 0 and M1, . . . , Mn µ( ) s.t. M M1 Mn T1(ϕ)}

T M 2 (ϕ) therefore contains a tree with all the models involved in the process of evaluating ϕ in some w M. This idea is not new, see e.g. [van Benthem and Pacuit, 2006].

Theorem 5 Let ϕ LDELVO and M, w σ(EMV). Let T M 3 (ϕ) = W, R, E, V, f such that W, R, V, f = F T M 2 (ϕ) and regarding E, for all multi-pointed action models Mi, Si that appear in ϕ it holds that, for w M and w M , w Eaiv iff (M, w)[|Mi, Si|](M , w ). Finally let T M 4 (ϕ) be a model that has T M 3 (ϕ) as a submodel but contains appropriate definitions for opaque choice and composition, so that T M 4 (ϕ) DEM. Let t : LDELVO LPDLVE be a function such that t(ϕ) is ϕ, but for all action models Mi, Si that appear in ϕ, all its occurrences are replaced with ai. Then it holds that M, w |= ϕ iff T M 4 (ϕ), w |= t(ϕ).

For the direction PDLVE to DELVO , the problem we will be trying to solve is, given M, w σ(DEM) and ϕ LPDLVE, is there a translation t for ϕ, where actions of PDL have been translated into multi-pointed action models, such that N(w), w |= t(ϕ)? Such a translation is impossible to define homogeneously for all models of PDLVE, as action a changes depending on its relation, in each PDLVE model M. So let M DEM, and a Act. Action a is perhaps executable in a number of worlds, and for each such world, the action may have a number of different possible executions. When focusing on the case where a single world w is connected through a with a world v, then the question is: is there a multi-pointed action model to transform N(w), w into N(v), v? This question relates to epistemic planning, which is undecidable for the multi-agent case [Aucher and Bolander, 2013], and it has been answered in [van Ditmarsch and Kooi, 2008] for finite S5 models (and other models under certain restrictions) and using action models with assignment to achieve ontic change. Our construct will follow the same idea, but we will be focusing on PDLVE models that (i) have finite W, (ii) are an epistemic bisimulation contraction (cf. [Blackburn et al., 2007]), and (iii) for which w Eav implies that for all v Nw(v), f(w) f(v ) is finite. Note that for any M, w σ(DEM) satisfying (i)-(ii), there exists a characteristic formula ϕw LDELVO [Barwise and Moss, 1996], i.e., for v M we have M, v |= ϕw iff v = w.

Definition 18 Let M, w σ(DEM), satisfying (i)-(iii) and w Eav. We define h(M, w, v) = W, R, pre, tgl as: W = Nw(v), R = R|Nw(v); for all w W, pre(w) = ϕw, tgl(w) = f(w) f(w).

Back to the more general problem; action a can lead a world w to a multitude of worlds vi, finite in number. A way to get an equivalent result by using action models, is to put side by

side , via disjoint union, models h(M, w, vi). Furthermore, we can have the case where action a is executable in a multitude of worlds wj, again finite in number. Again, this can be solved by taking the disjoint union of h(M, wj, v). Definition 19 Let M, w σ(DEM), ϕ LPDLVE and a an action that appears in ϕ. Let M satisfy (i)-(iii). Define: Ma, Sa = F w M F v Ea(w) h(M, w, v), v.

Theorem 6 Let M, w σ(DEM) as above and ϕ LPDLVE. Let t : LPDLVE 7 LDELVO be a function such that t(ϕ) is ϕ, but for all actions a that appear in ϕ, all its occurrences are replaced with Ma, Sa. Then it holds that M, w |= ϕ iff N(w), w |= t(ϕ).

5 Conclusion We pointed to two different ways to understand the interaction between knowledge dynamics and non-determinism, starting from logics DEL, PDL, and SPE. We presented a multi-pointed action model formulation of DEL to express non-deterministic choice. We defined the logic DELVO, which is capable of handling epistemic and ontic change (for DEL-based work that also combines epistemic and ontic change see [van Eijck, 2004a; 2004b], [van Benthem et al., 2006], and [van Ditmarsch and Kooi, 2008]), along with the notion of vision, and allows for a richer set of actions than those of DEL and SPE. Within DELVO, we defined both standard and opaque forms of choice and composition. We also provided a sound and complete axiomatisation for it, and a number of embedding results situating it among its related formalisms. We also explored a more abstract logic, capable of epistemic and ontic change, with an even richer class of actions: PDLVE. Its semantics are based on PDL models with epistemic relations and vision atoms. Here, our contribution is the definition of opaque non-deterministic choice and composition in this PDLlike setting. Finally, we provided theorems that compare DELVO and PDLVE, thus also investigating the relation between action models, and atomic actions defined arbitrarily. Several opportunities for future work exist; we briefly mention that for DELVO we would like vision atoms to exist for other formulas as well, not only variables. For PDLVE there is the obvious need for a proof system. Furthermore, two papers that in our opinion are especially relevant are [van Eijck, 2012] and [Charrier et al., 2016]. The former distinguishes between actual use of vision and the capability to use it. In the latter, vision is necessarily common knowledge and the notions of higher order and joint vision are introduced. One may also consider the agents not being aware of the actions being executed or some of the variables [van Ditmarsch et al., 2012]. Another worthwhile endeavour would be a systematic comparison between our framework and the Situation Calculus (cf. [Scherl and Levesque, 2003; van Ditmarsch et al., 2011]) and the standard and opaque variants. The difference between the variants is demonstrated by the difference between MDP and POMDP (see for example [Boutilier et al., 2000; Delgrande and Levesque, 2013] and [Bacchus et al., 1999]).

Acknowledgements We wish to thank the anonymous reviewers for many helpful and constructive comments.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

References [Aucher and Bolander, 2013] Guillaume Aucher and Thomas Bolander. Undecidability in epistemic planning. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence IJCAI 2013, pages 3 9, 2013. [Bacchus et al., 1999] Fahiem Bacchus, Joseph Y. Halpern, and Hector J. Levesque. Reasoning about noisy sensors and effectors in the situation calculus. Artificial Intelligence, 111(1):171 208, 1999. [Balbiani et al., 2013] Philippe Balbiani, Andreas Herzig, and Nicolas Troquard. Dynamic logic of propositional assignments: A well-behaved variant of PDL. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 13, pages 143 152, Washington, DC, USA, 2013. IEEE Computer Society. [Baltag and Moss, 2004] Alexandru Baltag and Lawrence S. Moss. Logics for epistemic programs. Synthese, 139:165 224, 2004. Knowledge, Rationality & Action 1 60. [Baltag et al., 1998] Alexandru Baltag, Lawrence S. Moss, and Stawomir Solecki. The logic of common knowledge, public announcements, and private suspicions. In Itzhak Gilboa, editor, Proceedings of the 7th conference on theoretical aspects of rationality and knowledge (TARK 98), pages 43 56, 1998. [Barwise and Moss, 1996] Jon Barwise and Lawrence Moss. Vicious circles : on the mathematics of non-wellfounded phenomena. CSLI Publications, Stanford, 1996. [Blackburn et al., 2001] Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press: Cambridge, England, 2001. [Blackburn et al., 2007] Patrick Blackburn, Johan F.A.K. van Benthem, and Frank Wolter. Handbook of Modal Logic. Studies in logic and practical reasoning. Elsevier, 2007. [Boutilier et al., 2000] Craig Boutilier, Ray Reiter, Mikhail Soutchanski, and Sebastian Thrun. Decision-theoretic, high-level agent programming in the situation calculus. In Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, pages 355 362. AAAI Press, 2000. [Charrier et al., 2016] Tristan Charrier, Andreas Herzig, Emiliano Lorini, Faustine Maffre, and Franois Schwarzentruber. Building epistemic logic from observations and public announcements. In International Conference on Principles of Knowledge Representation and Reasoning (KR), Capetown, 25/04/2016-29/04/2016, pages 268 277, http://www.aaai.org/Press/press.php, 2016. AAAI Press. [Delgrande and Levesque, 2013] James P. Delgrande and Hector J. Levesque. A formal account of nondeterministic and failed actions. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI 13, pages 861 868. AAAI Press, 2013. [Fagin et al., 1995] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. The MIT Press: Cambridge, MA, 1995.

[Grossi et al., 2016] Davide Grossi, Wiebe van der Hoek, Christos Moyzes, and Michael Wooldridge. Program models and semi-public environments. Journal of Logic and Computation, 2016. [Harel et al., 2000] David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. The MIT Press: Cambridge, MA, 2000. [Scherl and Levesque, 2003] Richard B. Scherl and Hector J. Levesque. Knowledge, action, and the frame problem. Artificial Intelligence, 144(1):1 39, 2003. [van Benthem and Pacuit, 2006] Johan van Benthem and Eric Pacuit. The tree of knowledge in action: Towards a common perspective. In Advances in Modal Logic (Ai ML), 2006. [van Benthem et al., 2006] Johan van Benthem, Jan van Eijck, and Barteld Kooi. Logics of communications and change. Information and Computation, 204:1620 1662, 2006. [van der Hoek et al., 2011] Wiebe van der Hoek, Petar Iliev, and Michael Wooldridge. Knowledge and action in semipublic environments. In Jerome Lang, Hans van Ditmarsch, and Shier Ju, editors, Logic, Rationality, and Interaction (LORI), volume 6953 of LNCS, pages 97 110, 2011. [van Ditmarsch and Kooi, 2008] Hans P. van Ditmarsch and Barteld P. Kooi. Semantic results for ontic and epistemic change. In Giacomo Bonanno, Wiebe van der Hoek, and Michael Wooldridge, editors, Logic and the Foundations of Game and Decision Theory, pages 87 117. Amsterdam University Press, 2008. [van Ditmarsch et al., 2007] Hans P. van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic. Springer-Verlag: Berlin, Germany, 2007. [van Ditmarsch et al., 2011] Hans van Ditmarsch, Andreas Herzig, and Tiago De Lima. From situation calculus to dynamic epistemic logic. Journal of Logic and Computation, 21(2):179, 2011. [van Ditmarsch et al., 2012] Hans van Ditmarsch, Tim French, and Fernando R. Vel azquez-Quesada. Action models for knowledge and awareness. In Wiebe van der Hoek, Lin Padgham, Vincent Conitzer, and Michael Winikoff, editors, International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2012, Valencia, Spain, June 4-8, 2012 (3 Volumes), pages 1091 1098. IFAAMAS, 2012. [van Eijck, 2004a] Jan van Eijck. Dynamic epistemic modelling, 2004. Technical Report SEN-E0424. [van Eijck, 2004b] Jan van Eijck. Guarded actions, 2004. Technical Report SEN-E0424. [van Eijck, 2012] Jan van Eijck. Perception and change in update logic. In Jan Eijck and Rineke Verbrugge, editors, Games, Actions and Social Software, pages 119 140. Springer-Verlag, Berlin, Heidelberg, 2012.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)