Appendix G: More on action models and the Logic of Epistemic Actions

In this Appendix, we examine three key topics in the Logic of Epistemic Actions: a notion of action model equivalence known as action emulation, how to extend action models so as to allow “factual change” via valuation-changing substitutions, and how to add common knowledge to the Logic of Epistemic Actions.

• 1. Action emulation
• 2. Incorporating factual change
• 3. Adding common knowledge

---

1. Action emulation

Two different pointed Kripke models can satisfy exactly the same (ML)-formulas, making them semantically equivalent. This lead to the study of a notion of structural equivalence for pointed Kripke models that would hold if and only if semantic equivalence holds as well, thereby allowing us to determine if two pointed Kripke models are semantically equivalent by examining only their structure. An often-used notion of structural equivalence is bisimulation

Notice that the Bisimulation Theorem does not give us an exact correspondence between bisimulation and (ML)-semantic equivalence: the second item of the theorem requires the models be image finite. A more complicated version of the Bisimulation Theorem makes it possible to avoid the issue of image finiteness; see Blackburn et al. (2002) for details.

Similar to the way in which different pointed Kripke models can be (ML)-semantically equivalent, different actions \((A_1,e_1)\) and \((A_2,e_2)\) can also be “equivalent”. Following van Eijck, Ruan, and Sadzik (2012), action equivalence is defined in terms of bisimulation: to say that two actions are “equivalent” means that the actions can be executed in the same situations and, furthermore, whenever the actions are both executable, they yield bisimilar (and hence (ML)-indistinguishable) results.

Figure G1 provides an example of equivalent actions. Examining this figure, it is clear that \(A_1\) and \(A_2\) are executable in the same situations: each is executable in situations satisfying p and in situations satisfying \(\lnot p\). Further, these two action models produce bisimilar results: events \(e_1\) and \(f_1\) execute in the same situations and events \(f_2\) and \(f_3\) effectively “simulate” the always-executable event \(e_2\). This “simulation” works as follows: any situation at which \(e_2\) is executable satisfies either p or \(\lnot p\) and so may be matched up with one of \(f_2\) or \(f_3\). Since all events are interconnected in both action models, the connections between \(e_2\)-produced worlds match up with the connections between the corresponding \(f_2\)- or \(f_3\)-produced worlds in a way that ensures bisimilar results. For example, for a sequence of three worlds w, x, y, z connected in order using \(R_a\)-arrows and respectively satisfying p, p, \(\lnot p\), and p in the original model:

• the \(A_1\)-produced \((w,e_1)\), \((x,e_2)\), \((y,e_2)\), and \((z,e_1)\) are connected in order using \(R_a\)-arrows; and
• the \(A_2\)-produced final model will have the worlds \((w,f_1)\), \((x,f_2)\), \((y,f_3)\), and \((z,f_2)\) are connected in order using \(R_a\)-arrows.

Sietsma and van Eijck (2012) provide a full proof that these actions are equivalent.

It is possible to define a notion of bisimulation for actions, but it turns out that there are equivalent actions that are not bisimilar (van Eijck, Ruan, and Sadzik 2012; Sietsma and van Eijck 2012). This led to the search for a structural relationship between actions that hold if and only if the actions are equivalent. A notion of parameterized action emulation was proposed by van Eijck, Ruan, and Sadzik (2012), and a variant called action emulation was later proposed by Sietsma and van Eijck (2012). To introduce these, we first need the following preliminary definitions.

The single negation of a formula strips any outermost negation that is present or, if none is present, adds one. The single negation of a set just performs the single negation of each formula in the set. The closure of a set expands the set by repeatedly adding subformulas and performing single negations on the formulas present until no further expansion is possible. In essence, the closure if a set of formulas is the collection of all formulas that are “relevant” when it comes to determining whether a formula in the set is true at a pointed Kripke model. An atom over a set of formulas is a subset whose formulas can all be made true at a pointed Kripke model and, further, any larger subset would violate this property (see, e.g., Blackburn, de Rijke, and Venema 2002). In effect, choosing an atom of a set S is the same as choosing a pointed Kripke model that makes true the formulas in the atom and makes false the other formulas in S that are not in the atom. By choosing the set \(S=\pre(A_1)\cup\pre(A_2)\) to be the collection of all precondition formulas in either the action model \(A_1\) or the action model \(A_2\), an atom \(\sigma\in\At(S)\) over S identifies a maximal collection of preconditions in these action models that can simultaneously be made true: these are just the actions e having \(\pre(e)\in\sigma\). These ideas lead to the following notion of structural equivalence between action models.

Intuitively, an emulation between actions links events e and f via \(eE_\sigma f\) only if the preconditions of these events can be made simultaneously true in a situation that makes true all formulas in the atom \(\sigma\). Further, this linkage his bisimulation-like Back and Forth properties that respect consistency of the linking atoms: a link made between events via \(E_\sigma\) gives rise to another link made between events via \(E_\sigma\) only if it is consistent for a situation satisfying the formulas in \(\sigma\) to lead via an a-arrow to a situation satisfying the formulas in \(\sigma'\) (i.e., \(\bigwedge\sigma\land\langle a\rangle\bigwedge\sigma'\) is consistent). In this way, the Back and Forth conditions come with built-in guarantees of consistency, and this is leveraged in proving the following result.

This gives a direct correspondence between a parameterized structural relationship over actions and the semantic notion of action equivalence. However, the parameterization makes this notion complex. A simpler, non-parameterized structural relationship that gets close to providing a similar direct correspondence was recently proposed by Sietsma and van Eijck (2012). This relationship and the related results are formulated in terms of multi-pointed action models.

An action emulation connects events only if their preconditions are consistent. Further, for events e and f linked via \(eEf\), an event reachable from one of e and f via a-arrows is linked up with a set of events reachable from the other via a-arrows in such a way that the preconditions of e and f together imply that a-accessible worlds must satisfy a precondition from an event in the set whenever the precondition from the a-accessible event is satisfied. As it turns out, this is just what is needed to show that emulation implies equivalence. The converse (i.e., the statement that equivalence implies emulation) is an open question. However, a weaker version of the converse has been proved. This version makes use of the following result.

An action model that is canonical over a set S of formulas is an action model whose preconditions are conjunctions of atoms over S. Therefore, each precondition describes a situation in which the formulas in the corresponding atom over S are all true and the other formulas in S are all false. This gives important information that is exploited in proof of the following result.

Non-parameterized action emulation provides a procedure for determining whether two actions \((A_1,e_1)\) and \((A_2,e_2)\) are equivalent: construct the equivalent canonical multi-actions \((A_1^c,e_1^c)\) and \((A_2^c,e_2^c)\) and determine whether \[ (A_1^c,e_1^c)\leftrightarrows(A_2^c,e_a^c). \] Since \(A_1^c\) and \(A_2^c\) are both finite and computable from \(A_1\) and \(A_2\), it follows that the overall procedure is computable as well.

It is an open question whether the canonicity condition can be dropped in the second part of the Action Emulation Theorem. If this condition cannot be dropped, then it is possible that there may be a variant of the above-defined notion of non-parameterized action emulation that would correspond directly with action equivalence (as in the Parameterized Action Emulation Theorem except without the parameterization).

2. Incorporating factual change

As a consequence of the (EAL) semantics presented in the main article, an executable action \((A,e)\) transforms an initial world w into a resultant world \((w,e)\) in a manner that preserves the valuation. That is, a propositional letter p is true at the resultant world \((w,e)\) if and only if p was true at the initial world w. By the soundness of the axiomatic system \(\EAL\), the preservation of propositional valuation must be reflected in the axiomatics as well. And indeed, this is so: the \(\EAL\) reduction axiom for propositional letters \[ [A,e]p\leftrightarrow(\pre(e)\to p) \text{ for letters } p\in\sP \] implies the scheme \[ \pre(e)\to([A,e]p\leftrightarrow p) \text{ for letters }p\in\sP, \] which says that whenever \((A,e)\) is executable, p is true after the occurrence of \((A,e)\) if and only if p was true before the occurrence. Since this is true of all propositional letters, it follows that all actions are valuation-preserving. Thinking of propositional letters as the “basic facts” of the situations that we reason about using \(\EAL\), the preservation of valuations is sometimes described as “preserving (basic) facts” or as “leaving (basic) facts unchanged”.

Sometimes we want to reason about fact-changing actions. For example, if we use the letter q to represent the statement that “the light is on” and this is true in an initial world w, then the action of “flipping the light switch” should bring about a resultant world \((w,e)\) in which q is false. That is, the valuation should change: the basic fact q goes from being true in w to being false in \((w,e)\).

Incorporating factual change into the theory of action models requires two modifications: one syntactical-semantical and one axiomatic. For the syntactical-semantical modification, we add an extra component to action models that allows us to specify changes in the valuation of various letters.

We then define the language \eqref{EAL+S} of Epistemic Action Logic with substitution along with the set \(\AMS_*\) of pointed action models with substitution having preconditions in the language \eqref{EAL+S} much as we did for (EAL) and \(\AM_*\) but with a slightly different recursive grammar (in which pointed action models come from \(\AMS_*\) instead of from \(\AM_*\)):

\[\begin{gather*}\taglabel{EAL+S} F \ccoloneqq p \mid F\land F\mid \lnot F \mid [a]F \mid [A,e]F \\ \small p\in\sP,\; a\in\sA,\; (A,e)\in\AMS_* \end{gather*}\]

A substitution \(\sub\) specifies substitutions for propositional letters: to have \(\sub(e,p)=F\) means that we are to reassign the truth value of p so that it is like F as per the occurrence of event e. That is, at any world w at which e can occur (i.e., at which the precondition \(\pre(e)\) holds), the execution of e yields a world \((w,e)\) at which p is true if and only if F was true before in w. As a result, p is essentially replaced with F during the occurrence of the event. Formally, this works as follows:

• \(M,w\models[A,e]G\) holds if and only if \(M,w\not\models\pre(e)\) or \(M[A],(w,e)\models G\), where the model \[ M[A]=(W[A],R[A],V[A]) \] is the result of the product update (with substitution) \(M\mapsto M[A]\) defined by:
  • \(W[A]\coloneqq\{(v,g)\in W\times E \mid M,v\models\pre(g)\}\) — pair worlds with events whose preconditions they satisfy,
  • \((w_1,e_1)R[A]_a(w_2,e_2)\) if and only if there is an a-arrow from \(w_1\) to \(w_2\) in M and an a-arrow from \(e_1\) to \(e_2\) in A, and
  • \((v,g)\in V[A](p)\) if and only if \(M,v\models\sub(g,p)\) — make the truth of p at \((v,g)\) like that of the formula \(\sub(g,p)\) at v.

So if \(\sub(e,p)=F\), then the letter p is true after the occurrence of e if and only if F was true before the occurrence of e. Therefore, \(\sub(e,p)=p\) implies that the valuation of p is left unchanged, which is how the semantics worked before we introduced substitutions. Our assumption that we have \(\sub(e,p)=p\) for all but finitely many pairs \((e,p)\) ensures that the valuation changes for at most finitely many letters. The reason for this restriction is that we want action models to be finite objects: it should be possible in principle to write down a sequence of symbols (or draw a picture) that completely specifies any given action model in our language.

The axiomatic theory \(\EALS\) of Epistemic Action Logic with substitutions is identical to the theory \(\EAL\) except that the reduction axiom for propositional letters is changed to the following:

1. \([A,e]p \leftrightarrow (\pre(e)\to \sub(e,p))\) for letters \(p\in\sP\)
   “After a non-executable action, every letter holds—a contradiction. After an executable action, the substitution sets truth values.”

An example utilizing an action model with substitution is given in Figure G2, where the action \(\mathsf{Flip}(q)\) implements our light-switch action: the occurrence of this action toggles the truth value of q between “on” (i.e., true) and “off” (i.e., false) in a manner that is common knowledge to all.

Almost all results about action model logics carry through mutatis mutandis upon addition of valuation-changing substitutions. So in the interest of simplicity, we assume in what follows that, unless stated otherwise, our action models do not contain valuation-changing substitutions. It is worth noting that this assumption is often made in the DEL literature and, in light of how simple it is to include valuation-changing substitutions if they are desired, this assumption should not be viewed as a genuine limitation to a given piece of work.

3. Adding common knowledge

To study the effect of common knowledge on action models, we define the language \eqref{EAL+C} of (EAL) with common knowledge along with the set \(\AMC_*\) of pointed action models with preconditions in the language \eqref{EAL+C} according to the following recursive grammar:

\[\begin{gather*}\taglabel{EAL+C} F \ccoloneqq p \mid F\land F \mid \lnot F \mid [a]F \mid [A,e]F \mid [B*]F \\ \small p\in\sP,\; a\in\sA,\; (A,e)\in\AMC_*,\; B\subseteq\sA \end{gather*}\]

The semantics of this language over pointed Kripke models is defined above. There are a number of interesting fragments of \eqref{EAL+C} obtained by restricting the action model modalities \([A,e]\) to have certain communicative forms. Here are a few examples.

• (PUB+C) is the fragment of \eqref{EAL+C} obtained by requiring that any action model modality \([A,e]\) used in the formation of a formula be a public announcement modality \([\Pub(F),e]\). See Figure 4 (main article) for a picture of the action model \(\Pub(p)\).
• (PRI+C) is the fragment of \eqref{EAL+C} obtained by requiring that any action model modality \([A,e]\) used in the formation of a formula be a private announcement modality \([\Pri(F),e]\) Figure 3 (main article) depicts the action model \(\Pri(p)\).

We now examine the axiomatic theory of EAL with common knowledge.

Just like for \(\PALC\), there can be no reduction theorem for \(\EALC\). This makes for a more intricate completeness proof.

We summarize some of the known expressive relationships between various fragments of \eqref{EAL+C} over the class of all pointed Kripke models. Relationships over various other classes are reported by van Ditmarsch, van der Hoek, and Kooi (2007).

In closing, we note two alternative approaches to reasoning about action models and common knowledge.

• van Benthem, van Eijck, and Kooi (2006) extend (ML) to an “Epistemic Propositional Dynamic Logic” that can express common knowledge (and relativized common knowledge). It is shown via a Reduction Theorem that adding action model modalities does not increase expressivity of the language.
• Van Benthem and Ikegami (2008) show that modal \(\mu\)-calculus, which can express common knowledge, is closed under the product update. That is, a Reduction Theorem implies that adding action model modalities does not increase expressivity of the language.

← beginning of main article