Non-Determinism and the Dynamics of Knowledge

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

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 Kwix be shorthand for Kix∨Ki¬x, and x:=⊥ (respectively, ⊤) stands for the action of setting variable x to false (respectively, true):

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:

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 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.

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. vRw}.

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.

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. EMdenotes 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 wRu and wRu. 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 ↦→ 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 visionthat 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).

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:

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

• wRiu 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 , preV , tglV 〉 as follows:

• WV =W; preV = pre; tglV = tgl;
• wRVi u iff (wRiu 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 wRiu and wRVi 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 wRiv then there is a v′ ∈ W ′ such that w′R′i v′ and (v, v′ ) ∈ Z; Back For all v′ ∈W ′ , if w′R′i v′ then there is a v ∈W such that wRiv 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 → KjVix, 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 ∈VisM(χV → ∧wRVi u Ki[M V , 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 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 ⊎ ⊤!]¬Kw2x while for standard choice M,w |= [�x ∪ ⊤!]Kw2x. And for agent 1 that 'sees' x we have M, w |= [�x ⊎ ⊤!]Kw1x ∧ [�x ∪ ⊤!]Kw1x.

This example demonstrates that both directions of validity (1) fail for opaque choice. Indeed, we have M,w |= [�x]Kw2x ∧ [⊤!]Kw2x but M,w |= ¬[�x ⊎ ⊤!]Kw2x, and similarly M,w |= [�x ⊎ ⊤!]¬Kw2x but M,w |= ¬[�x]¬Kw2x. 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:

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 vjRivk 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 MVa;b , SVa;b = 〈W, R, pre, tgl〉, S where: W = Wa × Wb, S = Sa × Sb,

• (w,w′ )Ri(v, v′ ) iff wRVai v & w′RVbi v′ ;
• 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 RVai 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 inM.

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 ∪ ⊤!); ;⊤!]Kw2x, while M, w |= [�x ∪ ⊤!][⊤!]Kw2x.

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) = ∅.

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 : σ(��) ↦→ µ(���) 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. vEw}.

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 uR′′ z iff wRv 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 (uR′′ z), if and only if the origin worlds were indistinguishable to begin with (wRv) 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)), thenN(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 wEav 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

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.

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(ϕ)}.

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〉 = ⊔ 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 ′ , wEai v′ 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 wEav 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 wEav. 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:

Theorem 6 Let M, w ∈ σ(DEM) as above and ϕ ∈ LPDLVE. Let t : LPDLVE ↦→ 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.