# Logics for Epistemic Actions:
Completeness, Decidability, Expressivity

$\begin{array}[]{c}\mbox{Alexandru Baltag}\\\ \mbox{ILLC, University of
Amsterdam}\\\ \mbox{1090 GE Amsterdam}\\\ \mbox{Netherlands}\\\ \mbox{\tt
<EMAIL_ADDRESS>\end{array}$
$\begin{array}[]{c}\mbox{Lawrence S.~{}Moss}\\\ \mbox{Mathematics
Department}\\\ \mbox{Indiana University}\\\ \mbox{Bloomington, IN 47405-7106
USA}\\\ \mbox{\tt<EMAIL_ADDRESS>\end{array}$
$\begin{array}[]{c}\mbox{S{\l}awomir Solecki}\\\ \mbox{Mathematics
Department}\\\ \mbox{Cornell University}\\\ \mbox{Ithaca, New York 14853
USA}\\\ \mbox{\tt<EMAIL_ADDRESS>\end{array}$

###### Abstract

We consider dynamic versions of epistemic logic as formulated in [4]. That
paper proposed a family of logical languages ${\cal L}({\mathbf{\Sigma}})$
parameterized by action signatures. In addition to ${\cal
L}({\mathbf{\Sigma}})$, we consider two fragments ${\cal
L}_{0}({\mathbf{\Sigma}})$ and ${\cal L}_{1}({\mathbf{\Sigma}})$ of it. We
review the syntax and semantics of these languages ${\cal
L}_{0}({\mathbf{\Sigma}}),{\cal L}_{1}({\mathbf{\Sigma}})$, and ${\cal
L}({\mathbf{\Sigma}})$, as well as the sound proof systems for the validities
in them. It was shown in [16] that validity in ${\cal L}({\mathbf{\Sigma}})$
is $\Pi^{1}_{1}$-complete, so there are no recursively axiomatized complete
logical systems for it. On the positive side, this paper proves the strong
completeness of the axiomatization of ${\cal L}_{0}({\mathbf{\Sigma}})$ and
the weak completeness of ${\cal L}_{1}({\mathbf{\Sigma}})$. The work involve a
detour into term rewriting theory. And since at the heart of the argument is
modal filtration, it gives the finite model property and hence decidability.
We also give a translation of ${\cal L}_{1}({\mathbf{\Sigma}})$ into PDL,
hence we obtain a second proof of the decidability of ${\cal
L}_{1}({\mathbf{\Sigma}})$. The paper closes with some results on expressive
power. These are mostly concerned with comparing ${\cal
L}_{1}({\mathbf{\Sigma}})$ with modal logic together with transitive closure
operators. We also answer a natural question about the languages we get by
varying the action signature. In particular, we prove that a logical language
with operators for private announcements is more expressive than one for
public announcements.

This paper was intended to be the “journal” version of our 1998 paper “The
logic of common knowledge, public announcements, and private suspicions.” It
was mainly written in 2004, with a few bibliographic additions coming a few
years later.

###### Contents

  1. 1 Introduction
  2. 2 Definitions
    1. 2.1 State models and propositions
    2. 2.2 Updates
    3. 2.3 Action models and program models
    4. 2.4 The update product
    5. 2.5 Updates induced by program models
    6. 2.6 Operations on program models
    7. 2.7 Action signatures
    8. 2.8 Bisimulation-based notions of equivalence
  3. 3 The languages ${\cal L}({\mathbf{\Sigma}})$
    1. 3.1 The syntax and semantics of ${\cal L}({\mathbf{\Sigma}})$
    2. 3.2 Examples
    3. 3.3 Basic properties
  4. 4 The logical system for validity of ${\cal L}({\mathbf{\Sigma}})$ sentences
    1. 4.1 Soundness of the axioms
  5. 5 The Action Rule
    1. 5.1 The canonical action model ${\mathbf{\Omega}}$
    2. 5.2 The main result about ${\mathbf{\Omega}}$
    3. 5.3 Soundness of the Action Rule
    4. 5.4 Syntactic Facts
  6. 6 Completeness theorems
    1. 6.1 Proofs of the main facts on normal forms and the well-order $<$
    2. 6.2 Strong completeness for ${\cal L}_{0}({\mathbf{\Sigma}})$
    3. 6.3 Weak completeness for ${\cal L}_{1}({\mathbf{\Sigma}})$
    4. 6.4 Extensions to the completeness theorem
  7. 7 Results on expressive power
    1. 7.1 Translation of ${\cal L}_{1}({\mathbf{\Sigma}})$ into PDL
    2. 7.2 ${\cal L}_{1}({\mathbf{\Sigma}}{\mbox{\scriptsize pub}})$ is more expressive than ${\cal L}_{1}$
    3. 7.3 ${\cal L}_{1}({\mathbf{\Sigma}}{\mbox{\scriptsize pri}})$ is more expressive than ${\cal L}_{1}({\mathbf{\Sigma}}{\mbox{\scriptsize pub}})$
    4. 7.4 ${\cal L}({\mathbf{\Sigma}}{\mbox{\scriptsize pub}})$ lacks the finite model property
  8. References

##  1 Introduction

One of the goals of dynamic epistemic logic is to construct logical languages
which allow one to represent a variety of possible types of changes affecting
the information states of agents in a multi-agent setting. One wants (formal)
logical systems with primitive operations corresponding to (informal) notions
such as public announcement, completely private announcement, private
announcement to one agent with suspicion by another, etc. And then after the
logics are formulated, one would ideally want technical tools to use in their
study and application.

The full formulation of such logics is somewhat of a complicated story. In the
first place, one needs a reasonable syntax. On the semantic side, there is an
unusual feature in that the truth of a sentence at a point in one model often
depends on the truth of a related sentence in a different model. In effect,
the kinds of actions we are interested in give rise to functions, or relations
more generally, on the class of all possible models.

There have been some proposals on logical systems for dynamic epistemic logic
beginning with the work of Plaza [17], Gerbrandy [12, 13], and Gerbrandy and
Groeneveld [14]. These papers formulated logical systems for the informal
notions of public announcement and completely private announcement. They left
open the matter of axiomatizing the logics in the presence of common knowledge
operators. (Without the common knowledge operators, the systems are seen to be
variants on standard multi-model logic.) And they also left open the question
of the decidability of these systems. Our work began with complete
axiomatizations for these systems and for more general systems. Our results
were presented in [5]. As it happens, the logics which we constructed in [5]
did not have the friendliest syntax. The first two authors pursued this matter
for some time and eventually came to the proposals in [4]. The logical systems
for the validities of the ultimate languages are certainly related to those in
[5]. But due to the different formulation of the overall syntax and semantics,
all of the work on soundness and completeness had to be completely reworked.
The main purpose of the present paper is to present these results.
Secondarily, we present some technical results on the systems such as results
on expressive power.

#### Contents of this paper: a high level view

This paper is a long technical development, and for this reason we did not
include a full-scale motivation of the logical systems themselves. For a great
deal of motivational material, one should see [5]. Section 2 formulates all of
the definitions needed in the paper. The presentation is based closely on the
work in [4], so readers familiar with that paper may use Section 2 as a
review. Other readers of this paper could take the logical systems here to
simply be extensions of propositional dynamic logic which allow one to make
“transitions from model to model” in addition to transitions “inside a given
model.” In addition, Section 2.8 is new in this paper.

The logical languages studied in this paper are presented in Section 3.
Section 3.2 presents some examples of the semantics, chosen to foreshadow work
in Section 7 on expressive power. The logical system is presented in Section
4, along with a soundness result for most of the system. One especially
significant inference rule, called the _Action Rule_ is studied in Section 5.
The completeness theorem for the logic comes in Section 6. The final section
deals with questions of expressive power, and it may be read after Section 4.

Two aspects of our overall machinery are worth pointing out. The first is the
use of the _canonical action model_. This is a semantic object built from
syntactic objects (sequences of _simple actions_ , terms in our language
${\cal L}({\mathbf{\Sigma}})$). We would like to think that the use of the
canonical model makes for a more elegant presentation than one would otherwise
have.

The second feature is a _term rewriting system_ for dealing with assertions in
the language. The semantic equivalences in dynamic epistemic logic are
sufficiently complicated that the ‘subsentence’ relation is not the most
natural or useful one for many purposes. Instead, one needs to handcraft
various ordering relations for use in inductive proofs, or in defining
translations. For just one example, in the logic of public announcements one
has an _announcement-knowledge axiom_ in a form such as

$[!\varphi]\Box\psi\leftrightarrow(\varphi\rightarrow\Box[!\varphi]\psi).$
(1.1)

This is for a logic with just one agent, and in this discussion we are
forgetting about common knowledge. To prove that the logic has a translation
$t$ back to ordinary modal logic, one wants to use the equivalence in (1.1)
above as the key step in the translation, defining $([\varphi]\Box]\psi)^{t}$
to be $\varphi^{t}\rightarrow(\Box[!\varphi]\psi)^{t}$. But then one needs to
have some reason to say that both $\varphi$ and (more critically)
$\Box[!\varphi]\psi$ are of _lower complexity_ than the original formula
$[\varphi]\Box\psi$. There are several ways to make this precise. One is to
directly assign an element of some well-founded set to each formula and then
use this as a measure of complexity. This is done in [9], and the well-founded
set is the natural numbers. Our treatment is different, mainly because it goes
via term rewriting. In effect, one takes the well-founded set to be the
sentences themselves, with the order given by substitution using laws such as
(1.1), but oriented in a specified direction (left-to-right, for example).
Then the fact that we have a well-founded relation is a result one proves
about oriented sets of laws (term rewriting systems). In our case, we use an
interpretation constructed by hand.

Our term rewriting system is presented and studied in Section 6.1. It actually
deals not with ${\cal L}({\mathbf{\Sigma}})$ but with a different language
called ${\cal L}_{1}({\mathbf{\Sigma}})$. An important by-product of our
completeness proof via rewriting is a Normal Form Theorem for ${\cal
L}_{1}({\mathbf{\Sigma}})$. This is an interesting result in itself, and it
does not follow from other completeness proofs such as those in [9], or in the
paper [9], which we discuss next. In order to use the rewriting system. one
needs to know that substitution of “equivalent” objects preserves
“equivalence” and that the proof system itself is strong enough to reduce
sentences to normal form. Unfortunately, this “obvious” point takes a great
deal of work. The details are all in this paper, and to our knowledge no other
source presents complete proofs on these matters.

#### Comparison with some other work

The first version of this paper is our 1998 conference publication [5]. We
ourselves had several versions of this paper issued as technical reports or
posted on web sites, and so in some sense the results here are _public_ but
not _published_. In the past ten years, the subject of dynamic epistemic logic
has taken off in a serious way. It sees several papers a year. But it seems
fair to say that the overall topics of investigation are not the logical
systems presented in the any of the original papers but rather are adaptations
of the logics to settings involving probability, belief revision, quantum
information, and the like. Still, the work reported here has been the subject
of several existing publications. And so it makes sense for us to make the
case that the results in this paper are still relevant and do not follow from
previously published results.

The book _Dynamic Epistemic Logic_ by Hans van Ditmarsch, Wiebe van der Hoek,
and Barteld Kooi [9] is a textbook presentation containing some of the content
of this paper and [4], with additional material on model checking, belief
revision, and other topics. Section 6.4 presents the syntax of what it calls
_action model logic_ and writes as ${\cal L}^{\rm act}_{KC\otimes}(A,P)$. At
first glance, the syntax of ${\cal L}^{\rm act}_{KC\otimes}(A,P)$ seems fairly
close to the language ${\cal L}({\mathbf{\Sigma}})$ presented in [4] and
reviewed in Section 3 of this paper. A relatively small difference concerns
the _action models_ in ${\cal L}^{\rm act}_{KC\otimes}(A,P)$. (In general,
action models are like Kripke models together with a “precondition” function
mapping worlds to sentences.) These are required to have the property that
each agent’s accessibility relation is an equivalence relation; our treatment
is more general and hence can present logics for epistemic actions such as
“cheating” in games. But the main difference is that our language ${\cal
L}({\mathbf{\Sigma}})$ uses what everyone would take to be a bona fide syntax:
sentences and program expressions are linearly ordered strings of symbols. In
contrast, the syntax of ${\cal L}^{\rm act}_{KC\otimes}(A,P)$ employs action
models _directly_. Structured but unordered objects occur inside of sentences.
In a different context, it would be like studying formal language and their
connection to automata by studying something that was like a regular
expression but allowed finite automata to directly occur inside some syntactic
object.

We have no objection ourselves to this move. In fact, this was the
presentation we chose in our first version [5] of this paper. But over the
years we have found quite a lot of resistance to this presentation on the
grounds that one is “mixing syntax and semantics.” Again, we do not assert
this objection, but we _address_ it by employing the large technical machinery
that we see in [4] and also Sections 2 and 3. (We are keenly aware of the
irony of our being criticized for “mixing syntax and semantics” in the ten-
year-old publication [5], and after we “un-mixed” them in [4], we find others
making the same natural move.)

We would also like to mention the paper “Logics of Communication and Change”,
van Benthem, van Eijck and Kooi [7]. This paper presents completeness theorem
for a logical system in the same family as ours. But as it happens, the paper
studies a different system. To see the differences, it is worthwhile to note
that the source of much of the work in this area concerns assertions of common
knowledge following an action of some sort. In our setting, these would be
written $[\alpha]\Box^{*}\varphi$. It turns out that there is no equivalence
of the form (1.1) for assertions like this. This leads us to our Action Rule,
an inference rule allowing the derivation of sentences of the kind under
discussion. The idea in [7] is to start with propositional dynamic logic,
called E-PDL in the paper (‘E’ for ‘epistemic’). Then one adds modalities
corresponding to update models $[{\sf U},e]$; this modality would be like our
$[\alpha]$, but in [7] as in [5] and [9], this U is an action model rather
than a bona fide syntactic object. Then one proves that the addition can be
translated away. This very interesting and suggestive result is not available
in our setting. The paper [7] notes that “Indeed, reduction axioms are not
available, as the logic with epistemic updates is more expressive than the
logic without them. We think this is an infelicity of design.” This is
somewhat debatable, since the additional expressive power in E-PDL is not
something in wide use. “We have found no practical use for these [complex
combinations of agent acessibility relations] at present, but they are the
price that we cheerfully pay for having a language living in expressive
harmony with its dynamic superstructure $\ldots$.” It also holds that “it’s
completeness theorem [from [5]] is correspondingly mess.” This extra “mess” is
due partly to the strictly “syntactic syntax”, partly to the explicit
rewriting work (taken for granted in [7]), and partly to the noted
“disharmony”. It is not known whether E-PDL is actually stronger than the
logical systems in this paper. If it is, then this would show that the
completeness result here is definitely not a special case of that in [7]. But
again, the matter is open at this time: one cannot derive our result from [7]
since the systems are prima facie different.

##  2 Definitions

This section provides all of our definitions. It is short on motivation, and
we have situated the examples in Section 3.2, following all the definitions.
See also Sections 1 and 2 of [4] for the motivation from epistemic logic and
for a more leisurely presentation.

###  2.1 State models and propositions

We fix a set ${\sf AtSen}$ of atomic sentences and also a set ${\cal A}$ of
agents. All of our definitions are relative to these sets.

A state model  is a triple ${{\mathbf{S}}}=(S,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$}_{\\!\\!{\mathbf{S}}},\|\cdot\|_{{\mathbf{S}}})$
consisting of a set $S$ of “states”; a family $\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}_{\\!\\!{\mathbf{S}}}$ of binary accessibility relations $\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}_{\\!\\!{\mathbf{S}}}\subseteq S\times S$, one for each agent
$A\in{\cal A}$; and a “valuation” (or a “truth” map)
${\|.\|}_{{\mathbf{S}}}\,:{\sf AtSen}\rightarrow{\cal P}(S)$, assigning to
each atomic sentence $p$ a set $\|p\|_{{\mathbf{S}}}$ of states. These are
exactly Kripke models generalized by having one accessibility relation for
each agent. We use the terminology of state models because there are other
kinds of models, action models and program models, in our study. When dealing
with a single fixed state model ${\mathbf{S}}$, we often drop the subscript
${\mathbf{S}}$ from all the notation.

Definition  Let SMod be the collection of all state models. An epistemic
proposition is an operation $\varphi$ defined on SMod such that for all
${\mathbf{S}}\in\mbox{\sf SMod}$,
${\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}}\subseteq S$.

The collection of epistemic propositions is closed in various ways.

  1. 1.

For each atomic sentence $p$ we have an atomic proposition $p$ with
${\mbox{\boldmath$p$\unboldmath}}_{{\mathbf{S}}}=\|p\|_{{\mathbf{S}}}$.

  2. 2.

If $\varphi$ is an epistemic proposition, then so is
$\neg{\mbox{\boldmath$\varphi$\unboldmath}}$, where
$(\neg{\mbox{\boldmath$\varphi$\unboldmath}})_{{\mathbf{S}}}=S\setminus{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}}$.

  3. 3.

If $C$ is a set or class of epistemic propositions, then $\bigwedge C$ is an
epistemic proposition, where

$(\bigwedge
C)_{\scriptstyle{\mathbf{S}}}\quad=\quad\bigcap\\{{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}}:{\mbox{\boldmath$\varphi$\unboldmath}}\in
C\\}.$

  4. 4.

Taking $C$ above to be empty, we have an “always true” epistemic proposition
tr, with $\mbox{\sf\bf tr}_{{\mathbf{S}}}=S$.

  5. 5.

We also may take $C$ in part 3 to be a two-element set
$\\{{\mbox{\boldmath$\varphi$\unboldmath}},{\mbox{\boldmath$\psi$\unboldmath}}\\}$;
here we write
${\mbox{\boldmath$\varphi$\unboldmath}}\wedge{\mbox{\boldmath$\psi$\unboldmath}}$
instead of
$\bigwedge\\{{\mbox{\boldmath$\varphi$\unboldmath}},{\mbox{\boldmath$\psi$\unboldmath}}\\}$.
We see that if $\varphi$ and $\psi$ are epistemic propositions, then so is
${\mbox{\boldmath$\varphi$\unboldmath}}\wedge{\mbox{\boldmath$\psi$\unboldmath}}$,
with
$({\mbox{\boldmath$\varphi$\unboldmath}}\wedge{\mbox{\boldmath$\psi$\unboldmath}})_{\scriptstyle{\mathbf{S}}}={\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}}\cap{\mbox{\boldmath$\psi$\unboldmath}}_{{\mathbf{S}}}$.

  6. 6.

If $\varphi$ is an epistemic proposition and $A\in{\cal A}$, then
$\Box_{A}{\mbox{\boldmath$\varphi$\unboldmath}}$ is an epistemic proposition,
with

$(\Box_{A}{\mbox{\boldmath$\varphi$\unboldmath}})_{\scriptstyle{\mathbf{S}}}\quad=\quad\\{s\in
S:\mbox{if $s\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}t$, then
$t\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}}$}\\}.$ (2.2)

  7. 7.

If $\varphi$ is an epistemic proposition and ${\cal B}\subseteq{\cal A}$, then
$\Box^{*}_{{\cal B}}{\mbox{\boldmath$\varphi$\unboldmath}}$ is an epistemic
proposition, with

$(\Box^{*}_{{\cal
B}}{\mbox{\boldmath$\varphi$\unboldmath}})_{\scriptstyle{\mathbf{S}}}\quad=\quad\\{s\in
S:\mbox{if $s\lower
1.0pt\hbox{$\longrightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{\\!\\!{\cal
B}^{*}}$}\hskip 7.22743pt\\!\\!$}t$, then
$t\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}}$}\\}.$

Here $s\lower
1.0pt\hbox{$\longrightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{\\!\\!{\cal
B}^{*}}$}\hskip 7.22743pt\\!\\!$}t$ iff there is a sequence

$s=u_{0}\quad\stackrel{{\scriptstyle A_{1}}}{{\rightarrow}}\quad
u_{1}\quad\stackrel{{\scriptstyle
A_{2}}}{{\rightarrow}}\quad\cdots\stackrel{{\scriptstyle
A_{n}}}{{\rightarrow}}\quad u_{n+1}=t$

where $A_{1},\ldots,A_{n}\in{\cal B}$. In other words, there is a sequence of
arrows labelled with agents from the set ${\cal B}$ taking $s$ to $t$. We
allow $n=0$ here, so
$\longrightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{\\!\\!{\cal
B}^{*}}$}\hskip 7.22743pt\\!\\!$ includes the identity relation on $S$.

#### Syntactic and semantic notions

It will be important for us to make a sharp distinction between syntactic and
semantic notions. We have already begun to do this, speaking of atomic
sentences and atomic propositions. The difference for us is that atomic
sentences are entirely syntactic objects: we won’t treat an atomic sentence
$p$ as anything except an unanalyzed mathematical object. On the other hand,
this atomic sentence $p$ also has associated with it the atomic proposition
$p$. As defined in point 1, $p$ will be a function whose domain is the (proper
class of) state models, and it is defined by

${\mbox{\boldmath$p$\unboldmath}}_{{\mathbf{S}}}\quad=\quad\\{s\in
S:s\in\|p\|_{{\mathbf{S}}}\\}.$ (2.3)

This difference may seem pedantic at first, and surely there are times when it
is sensible to blur it. But for various reasons that will hopefully become
clear, we need to insist on it.

Up until now, the only syntactic objects have been the atomic sentences
$p\in{\sf AtSen}$. But we can build the collections of finitary and infinitary
sentences by the same definitions that we have seen, and then the work of the
past section is the semantics of our logical languages. For example, we have
sentences $p\wedge q$, $\Box_{A}\neg p$, and $\Box^{*}_{{\cal B}}q$. These
then have corresponding epistemic propositions as their semantics:
${\mbox{\boldmath$p$\unboldmath}}\wedge{\mbox{\boldmath$q$\unboldmath}}$,
$\Box_{A}\neg{\mbox{\boldmath$p$\unboldmath}}$, and $\Box^{*}_{{\cal
B}}{\mbox{\boldmath$q$\unboldmath}}$, respectively. Note that the latter is a
properly infinitary proposition (and so $\Box^{*}_{{\cal B}}q$ is a properly
infinitary sentence); it abbreviates an infinite conjunction.

###  2.2 Updates

A transition relation between state models ${\mathbf{S}}$ and ${\mathbf{T}}$
is a relation between the sets $S$ and $T$; i.e., a subset of $S\times T$. An
update ${\bf r}$ is a pair of operations

$\mbox{\bf r}\quad=\quad({\mathbf{S}}\mapsto{\mathbf{S}}(\mbox{\bf
r}),{\mathbf{S}}\mapsto\mbox{\bf r}_{{\mathbf{S}}}),$

where for each ${\mathbf{S}}\in\mbox{\sf SMod}$, $\mbox{\bf
r}_{{\mathbf{S}}}\,:{\mathbf{S}}\rightarrow{\mathbf{S}}(\mbox{\bf r})$ is a
transition relation. We call ${\mathbf{S}}\mapsto{\mathbf{S}}(\mbox{\bf r})$
the update map, and ${\mathbf{S}}\mapsto\mbox{\bf r}_{{\mathbf{S}}}$ the
update relation.

We continue our general discussion by noting that the collection of updates is
closed in various ways.

  1. 1.

Skip: there is an update called “Skip” and denoted $1$, with
${\mathbf{S}}({\mbox{\boldmath$1$\unboldmath}})={\mathbf{S}}$, and
${{\mbox{\boldmath$1$\unboldmath}}}_{\mathbf{S}}$ is the identity relation on
${\mathbf{S}}$.

  2. 2.

Sequential Composition: if r and s are epistemic updates, then their
composition $\mbox{\bf r};\mbox{\bf s}$ is again an epistemic update, where
${\mathbf{S}}(\mbox{\bf r};\mbox{\bf s})={\mathbf{S}}(\mbox{\bf r})(\mbox{\bf
s})$, and $(\mbox{\bf r};\mbox{\bf s})_{\mathbf{S}}=\mbox{\bf
r}_{{\mathbf{S}}};{\mbox{\bf s}}_{{\mathbf{S}}(\mbox{\bf r})}$. Here, we use
on the right side the usual composition ; of relations.111We are writing
relational composition in left-to-right order in this paper.

  3. 3.

Union (or Non-deterministic choice): If $X$ is any set of epistemic updates,
then the union $\bigsqcup X$ is an epistemic update, defined as follows. For
each ${\mathbf{S}}$, the set of states of the model ${\mathbf{S}}(\bigsqcup
X)$ is the disjoint union of all the sets of states in each model
${\mathbf{S}}(\mbox{\bf r})$ for $\mbox{\bf r}\in X$:

$\\{(s,\mbox{\bf r}):\mbox{\bf r}\in X\mbox{ and }s\in{\mathbf{S}}(\mbox{\bf
r})\\}.$

Similarly, each accessibility relation
$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip 7.22743pt$ is
defined as the disjoint union of the corresponding accessibility relations in
each model:

$(t,\mbox{\bf r})\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(u,\mbox{\bf s})\quad\mbox{iff}\quad\mbox{ if $\mbox{\bf
r}=\mbox{\bf s}$ and $t\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}u$ in ${\mathbf{S}}(\mbox{\bf r})$}.$

The valuation $\|p\|_{{\mathbf{S}}(\bigsqcup X)}$ in ${\mathbf{S}}(\bigsqcup
X)$ is the disjoint union of the valuations in each state model:

$\|p\|_{{\mathbf{S}}(\bigsqcup X)}\quad=\quad\\{(s,\mbox{\bf r}):\mbox{\bf
r}\in X\mbox{ and }s\in\|p\|_{{\mathbf{S}}(\mbox{\bf r})}\\}.$

Finally, the update relation $(\bigsqcup X)_{{\mathbf{S}}}$ between
${\mathbf{S}}$ and ${\mathbf{S}}(\bigsqcup X)$ is the union of all the update
relations $\mbox{\bf r}_{{\mathbf{S}}}$:

$t\ (\bigsqcup X)_{{\mathbf{S}}}\ (u,\mbox{\bf r})\quad\mbox{iff}\quad t\
\mbox{\bf r}_{{\mathbf{S}}}\ u.$

  4. 4.

Special case: binary union. The (disjoint) union of two epistemic updates r
and s is an update $\mbox{\bf r}\sqcup\mbox{\bf s}$, given by $\mbox{\bf
r}\sqcup\mbox{\bf s}=\bigsqcup\\{\mbox{\bf r},\mbox{\bf s}\\}$.

  5. 5.

Another special case: Kleene star (iteration). We have the operation of Kleene
star on updates:

$\mbox{\bf
r}^{*}\quad=\quad\bigsqcup\\{{\mbox{\boldmath$1$\unboldmath}},\mbox{\bf
r},\mbox{\bf r}\cdot\mbox{\bf r},\ldots,\mbox{\bf r}^{n},\ldots\\}$

where $\mbox{\bf r}^{n}$ is recursively defined by $\mbox{\bf
r}^{0}={\mbox{\boldmath$1$\unboldmath}}$, $\mbox{\bf r}^{n+1}=\mbox{\bf
r}^{n};\mbox{\bf r}$.

  6. 6.

Crash: We can also take $X=\emptyset$ in part 3. This gives an update called
“Crash” and denoted $0$ such that
${\mathbf{S}}({\mbox{\boldmath$0$\unboldmath}})$ is the empty model for each
${\mathbf{S}}$, and ${{\mbox{\boldmath$0$\unboldmath}}}_{{\mathbf{S}}}$ is the
empty relation.

The operations $\mbox{\bf r};\mbox{\bf s}$, $\mbox{\bf r}\sqcup\mbox{\bf s}$
and $\mbox{\bf r}^{*}$ are the natural analogues of the operations of union of
relations, relational composition and iteration, and of the regular operations
on programs in PDL. The intended meanings are: for $\mbox{\bf r};\mbox{\bf
s}$, sequential composition (do r, then do s); for $\mbox{\bf
r}\sqcup\mbox{\bf s}$, non-deterministic choice (do either r or s); for
$\mbox{\bf r}^{*}$, iteration (repeat r some finite number of times).

#### Standard updates

An update a is standard if for all state models ${\mathbf{S}}$, $(\mbox{\bf
a}_{{\mathbf{S}}})^{-1}$ is a partial function. (The relation $(\mbox{\bf
a}_{{\mathbf{S}}})^{-1}$ the inverse of the update relation; it is a subset of
${\mathbf{S}}(\mbox{\bf a})\times{\mathbf{S}}$.)

###### Proposition 2.1

The update $1$ is standard. The composition of standard updates is standard,
as is any union of standard updates.

#### Updates Determine Dynamic Modalities

If $\varphi$ is an epistemic proposition and r an update, then $[\mbox{\bf
r}]{\mbox{\boldmath$\varphi$\unboldmath}}$ is an epistemic proposition defined
by

$([\mbox{\bf
r}]{\mbox{\boldmath$\varphi$\unboldmath}})_{\scriptstyle{\mathbf{S}}}\quad=\quad\\{s\in
S:\mbox{for all $t$ such that $s\ \mbox{\bf r}_{{\mathbf{S}}}\ t$,
$t\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf
r})}$}\\}.$ (2.4)

We should compare (2.4) and (2.2). The point is that we may treat updates in a
similar manner to other box-like modalities; the structure given by an update
allows us to do this.

We also define the dual proposition $\langle\mbox{\bf
r}\rangle{\mbox{\boldmath$\varphi$\unboldmath}}$ by

$(\langle\mbox{\bf
r}\rangle{\mbox{\boldmath$\varphi$\unboldmath}})_{\scriptstyle{\mathbf{S}}}\quad=\quad\\{s\in
S:\mbox{for some $t$ such that $s\ \mbox{\bf r}_{{\mathbf{S}}}\ t$,
$t\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf
r})}$}\\}.$

###  2.3 Action models and program models

Let $\Phi$ be the collection of all epistemic propositions. An (epistemic)
action model is a triple ${\mathbf{\Sigma}}=(\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre})$, where $\Sigma$ is a set of simple
actions, $\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$ is an ${\cal A}$-indexed family of binary relations on
$\Sigma$, and $\mbox{pre}\,:\Sigma\rightarrow\Phi$.

To model non-deterministic actions and non-simple actions (whose appearances
to agents are not uniform on states), we define epistemic program models. In
effect, this means that we decompose complex actions (‘programs’) into
“simple” ones: they correspond to sets of simple, deterministic actions from a
given action model.

A program model is defined as a pair $\pi=({\mathbf{\Sigma}},\Gamma)$
consisting of an action model ${\mathbf{\Sigma}}$ and a set
$\Gamma\subseteq\Sigma$ of _designated simple actions_. Each of the simple
actions $\gamma\in\Gamma$ may be thought of as a possible “deterministic
resolution” of the non-deterministic action $\pi$. As announced above, the
intuition about the map called pre is that an action is executable in a given
state only if all its preconditions hold at that state. We often spell out an
epistemic program model as $(\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre},\Gamma)$ rather than $((\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre}),\Gamma)$. Also, we usually drop the word
“epistemic” and just refer to these as program models.

###  2.4 The update product

Given a state model ${\mathbf{S}}=(S,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$}_{\\!\\!{\mathbf{S}}},\|\cdot\|_{{\mathbf{S}}})$ and an
action model ${\mathbf{\Sigma}}=(\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre})$, we define their update product to be the
state model

${\mathbf{S}}\otimes{\mathbf{\Sigma}}\quad=\quad(S\otimes\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\|.\|_{{\mathbf{S}}\otimes{\mathbf{\Sigma}}}),$

given by the following: the new states are pairs of old states $s$ and simple
actions $\sigma$ which are “consistent”, in the sense that all preconditions
of the action $\sigma$ “hold” at the state $s$

$S\otimes\Sigma\quad=\quad\\{(s,\sigma)\in
S\times\Sigma:s\in\mbox{pre}(\sigma)_{{\mathbf{S}}}\\}.$ (2.5)

The new accessibility relations are taken to be the “products” of the
corresponding accessibility relations in the two frames; i.e., for
$(s,\sigma),(s^{\prime},\sigma^{\prime})\in{\mathbf{S}}\otimes{\mathbf{\Sigma}}$
we put

$(s,\sigma)\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(s^{\prime},\sigma^{\prime})\quad\mbox{iff}\quad s\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}s^{\prime}\mbox{ and }\sigma\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma^{\prime},$ (2.6)

and the new valuation map
${\|.\|}_{{\mathbf{S}}\otimes{\mathbf{\Sigma}}}\,:{\sf AtSen}\rightarrow{\cal
P}(S\otimes\Sigma)$ is essentially given by the old valuation:

$\|p\|_{{\mathbf{S}}\otimes{\mathbf{\Sigma}}}\quad=\quad\\{(s,\sigma)\in
S\otimes\Sigma:s\in\|p\|_{{\mathbf{S}}}\\}.$ (2.7)

###  2.5 Updates induced by program models

Recall that we defined updates in Section 2.2. And above, in Section 2.3, we
defined epistemic program models. Note that there is a big difference: the
updates are pairs of operations on the class of all state models, and the
program models are typically finite structures. We think of program models as
capturing specific mechanisms, or algorithms, for inducing updates. This
connection is made precise in the following definition.

Definition  Let $({\mathbf{\Sigma}},\Gamma)$ be a program model. We define an
update which we also denote $({\mathbf{\Sigma}},\Gamma)$ as follows:

  1. 1.

${\mathbf{S}}({\mathbf{\Sigma}},\Gamma)={\mathbf{S}}\otimes{\mathbf{\Sigma}}$.

  2. 2.

$s\ ({\mathbf{\Sigma}},\Gamma)_{{\mathbf{S}}}\ (t,\sigma)$ iff $s=t$ and
$\sigma\in\Gamma$.

We call this the update induced by $({\mathbf{\Sigma}},\Gamma)$.

Note that updates of the form $({\mathbf{\Sigma}},\Gamma)$ have the property
that for all state models ${\mathbf{S}}$, the inverse of the update relation
$({\mathbf{\Sigma}},\Gamma)_{{\mathbf{S}}}$ is a partial function. That is,
these updates are standard.

###  2.6 Operations on program models

####  $1$ and $0$

We define program models $1$ and $0$ as follows: $1$ is a one-action set
$\\{\sigma\\}$ with $\sigma\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma$ for all $A$, $\mbox{\sc Pre}(\sigma)=\mbox{\sf\bf tr}$, and
with distinguished set $\\{\sigma\\}$. The point here is that the update
induced by this program model is exactly the update $1$ from Section 2.2. We
purposely use the same notation. Similarly, we let $0$ be the empty program
model. Then its induced update is what we called $0$ in Section 2.2.

#### Sequential Composition

In all settings involving “actions” in some sense or other, sequential
composition is a natural operation. In our setting, we would like to define a
composition operation on program models, corresponding to the sequential
composition of updates. Here is the relevant definition.

Let ${\mathbf{\Sigma}}=(\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre}_{\Sigma},\Gamma_{{\mathbf{\Sigma}}})$ and
${\mathbf{\Delta}}=(\Delta,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre}_{\Delta},\Gamma_{{\mathbf{\Delta}}})$ be
program models. We define the composition

${\mathbf{\Sigma}};{\mathbf{\Delta}}\quad=\quad(\Sigma\times\Delta,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre}_{\Sigma;\Delta},\Gamma_{\Sigma;\Delta})$

to be the following program model:

  1. 1.

$\Sigma\times\Delta$ is the cartesian product of the sets $\Sigma$ and
$\Delta$.

  2. 2.

$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal A}}$}\hskip
7.22743pt$ in the composition ${\mathbf{\Sigma}};{\mathbf{\Delta}}$ is the
family of product relations, in the natural way:

$(\sigma,\delta)\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(\sigma^{\prime},\delta^{\prime})\quad\mbox{iff}\quad\sigma\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma^{\prime}\mbox{ and }\delta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\delta^{\prime}.$

  3. 3.

$\mbox{pre}_{\Sigma;\Delta}(\sigma,\delta)=\langle({\mathbf{\Sigma}},\sigma)\rangle\mbox{pre}_{\Delta}(\delta)$.

  4. 4.

$\Gamma_{\Sigma;\Delta}=\Gamma_{{\mathbf{\Sigma}}}\times\Gamma_{{\mathbf{\Delta}}}$.

In the definition of pre, $({\mathbf{\Sigma}},\sigma)$ is an abbreviation for
the induced update $({\mathbf{\Sigma}},\\{\sigma\\})$ as defined in Section
2.5.

#### Unions

If ${\mathbf{\Sigma}}=(\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre}_{\Sigma},\Gamma_{{\mathbf{\Sigma}}})$ and
${\mathbf{\Delta}}=(\Delta,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre}_{\Delta},\Gamma_{{\mathbf{\Delta}}})$, we
take ${\mathbf{\Sigma}}\sqcup{\mathbf{\Delta}}$ to be the disjoint union of
the models, with union of the distinguished actions. The intended meaning is
the non-deterministic choice between the programs represented by
${\mathbf{\Sigma}}$ and ${\mathbf{\Delta}}$. Here is the definition in more
detail, generalized to arbitrary (possibly infinite) disjoint unions: let
$\\{{\mathbf{\Sigma}}_{i}\\}_{i\in I}$ be a family of program models, with
${\mathbf{\Sigma}}_{i}=(\Sigma_{i},\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre}_{i},\Gamma_{i})$; we define their
(disjoint) union

$\bigsqcup_{i\in I}{{\mathbf{\Sigma}}_{i}}\quad=\quad\biggl{(}\bigsqcup_{i\in
I}\Sigma_{i},\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre},\Gamma\biggr{)}$

to be the model given by:

  1. 1.

$\bigsqcup_{i\in I}\Sigma_{i}$ is $\bigcup_{i\in I}(\Sigma_{i}\times\\{i\\})$,
the disjoint union of the sets $\Sigma_{i}$.

  2. 2.

$(\sigma,i)\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(\tau,j)$ iff $i=j$ and $\sigma\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}_{i}\tau$.

  3. 3.

$\mbox{pre}(\sigma,i)=\mbox{pre}_{i}(\sigma)$.

  4. 4.

$\Gamma=\bigcup_{i\in I}(\Gamma_{i}\times\\{i\\})$.

#### Iteration

Finally, we define an iteration operation by
${\mathbf{\Sigma}}^{*}=\bigsqcup\\{{\mathbf{\Sigma}}^{n}:n\in N\\}$. Here
${\mathbf{\Sigma}}^{0}={\mbox{\boldmath$1$\unboldmath}}$, and
${\mathbf{\Sigma}}^{n+1}={\mathbf{\Sigma}}^{n};{\mathbf{\Sigma}}$.

Our definition of the operations on program models are faithful to the
corresponding operations on updates from Section 2.2.

######  Proposition 2.2 ([4])

The update induced by a composition of program models is isomorphic to the
composition of the induced updates. Similarly for sums and iteration, mutatis
mutandis.

Since we shall not use this result, we omit the proof.

###  2.7 Action signatures

Definition  An action signature is a structure

${\mathbf{\Sigma}}\quad=\quad(\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},(\sigma_{1},\sigma_{2},\ldots,\sigma_{n}))$

where ${\mathbf{\Sigma}}=(\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$})$ is a finite Kripke frame, and
$\sigma_{1},\sigma_{2},\ldots,\sigma_{n}$ is an enumeration of $\Sigma$ in a
list without repetitions. We call the elements of $\Sigma$ action types. When
we deal with an action signature, our notation for the action types usually
includes a subscript (even though this is occasionally redundant); thus the
action types come with a number that indicates their poisition in the fixed
enumeration of the action signature.

An action signature ${\mathbf{\Sigma}}$ together with an assignment of
epistemic propositions to the action types in $\Sigma$ gives us a full-fledged
action model. And this is the exact sense in which an _action signature_ is an
abstraction of the notion of _action model_. We shall use action signatures in
constructing logical languages.

#### Signature-based program models

Let ${\mathbf{\Sigma}}$ be an action signature, let $n$ be the number of
action types in $\Sigma$, let $\Gamma\subseteq\Sigma$, and let
$\vec{{\mbox{\boldmath$\psi$\unboldmath}}}={\mbox{\boldmath$\psi$\unboldmath}}_{1},\ldots,{\mbox{\boldmath$\psi$\unboldmath}}_{n}$
be a list of epistemic propositions. We obtain a program model
$({\mathbf{\Sigma}},\Gamma,\vec{{\mbox{\boldmath$\psi$\unboldmath}}})$ in the
following way:

  1. 1.

The set of simple actions is $\Sigma$, and the accessibility relations are
those given by the action signature.

  2. 2.

For $j=1,\ldots,n$,
$\mbox{pre}(\sigma_{j})={\mbox{\boldmath$\psi$\unboldmath}}_{j}$.

  3. 3.

The set of distinguished actions is $\Gamma$.

In the special case that $\Gamma$ is the singleton set $\\{\sigma_{i}\\}$, we
write the resulting signature-based program model as
$({\mathbf{\Sigma}},\sigma_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})$.

Finally, recall from Section 2.5 that every signature-based program model
induces an update.

To summarize: every action signature, set of distinguished action types in it,
and tuple of epistemic propositions gives a program model in a canonical way.
Every program model induces a standard update.

###  2.8 Bisimulation-based notions of equivalence

In this section, we discuss natural notions of equivalence for some of the
definitions which we have already seen. We begin by recalling the most
important notion of equivalence for state models, bisimulation.

Definition  Let ${\mathbf{S}}$ and ${\mathbf{T}}$ be state models. A
bisimulation between ${\mathbf{S}}$ and ${\mathbf{T}}$ is a relation
$R\subseteq S\times T$ such that whenever $s\ R\ t$, the following three
properties hold:

  1. 1.

$s\in\|p\|_{{\mathbf{S}}}$ iff $t\in\|p\|_{{\mathbf{T}}}$ for all atomic
sentences $p$.

  2. 2.

For $A\in{\cal A}$ and $s^{\prime}$ such that $s\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}s^{\prime}$, there is some $t^{\prime}$ such that $t\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}t^{\prime}$ and $s^{\prime}\ R\ t^{\prime}$.

  3. 3.

For $A\in{\cal A}$ and $t^{\prime}$ such that $t\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}t^{\prime}$, there is some $s^{\prime}$ such that $s\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}s^{\prime}$ and $s^{\prime}\ R\ t^{\prime}$.

$R$ is a total bisimulation if it is a bisimulation and in addition: for all
$s\in S$ there is some $t\in T$ such that $s\ R\ t$; and vice-versa.

###### Proposition 2.3

If there is a bisimulation $R$ such that $s\ R\ t$, then $s$ and $t$ agree on
all sentences $\varphi$ in infinitary modal logic:
$s\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$ iff
$t\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{T}}}$.

Recall that SMod is the class of all state models. We have spoken of states as
the elements of state models, but we also use the term states to refer to the
pairs $({\mathbf{S}},s)$ with ${\mathbf{S}}\in\mbox{\sf SMod}$ and $s\in S$.
The class of all states is itself a state model, except that its collection of
states is a proper class rather than a set. Still, it makes sense to talk
about bisimulation relations on the class of all states. The largest such is
given by

$({\mathbf{S}},s)\equiv({\mathbf{T}},t)\quad\mbox{iff}\quad\mbox{there is a
bisimulation $R$ between ${\mathbf{S}}$ and ${\mathbf{T}}$ such that $s\ R\
t$}.$

This relation $\equiv$ is indeed an equivalence relation.

When ${\mathbf{S}}$ and ${\mathbf{T}}$ are clear from the context, we write
$s\equiv t$ instead of $({\mathbf{S}},s)\equiv({\mathbf{T}},t)$.

#### Equivalence and preservation by bisimulation

Since we are discussing notions of equivalence here, it makes sense to also
think about epistemic propositions. Two propositions $\varphi$ and $\psi$ are
equal if they are the same operation on SMod. That is, for all ${\mathbf{S}}$,
${\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}}={\mbox{\boldmath$\psi$\unboldmath}}_{{\mathbf{S}}}$.
Later we shall introduce syntactically defined languages and also proof
systems to go with them; in due course we shall see other interesting notions
of equivalence.

Moving towards a connection of propositions with bisimulation. we say that a
proposition $\varphi$ is preserved by bisimulations if whenever
$({\mathbf{S}},s)\equiv({\mathbf{T}},t)$, then
$s\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}}$ iff
$t\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{T}}}$.

######  Proposition 2.4 ([4])

The propositions which are preserved by bisimulation include tr and the atomic
propositions $p$, and they are closed under all of the (infinitary) operations
on propositions from Section 2.1.

#### Equivalence of updates

We continue our discussion of equivalence with the relevant notion for
updates.

Definition  Updates a and b are _equivalent_ if for all state models
${\mathbf{S}}$ and ${\mathbf{T}}$ and all total bisimulations $R$ between
${\mathbf{S}}$ and ${\mathbf{T}}$, $(\mbox{\bf
a}_{{\mathbf{S}}})^{-1};R;\mbox{\bf b}_{{\mathbf{T}}}$ is a total bisimulation
between ${\mathbf{S}}(\mbox{\bf a})$ and ${\mathbf{T}}(\mbox{\bf b})$. We
write $\mbox{\bf a}\sim\mbox{\bf b}$ for this relation.

###### Proposition 2.5

Let $\mbox{\bf a}\sim\mbox{\bf b}$ and $\mbox{\bf c}\sim\mbox{\bf d}$. Then
$\mbox{\bf a};\mbox{\bf c}\sim\mbox{\bf b};\mbox{\bf d}$, and also $\mbox{\bf
a}\sqcup\mbox{\bf c}\sim\mbox{\bf b}\sqcup\mbox{\bf d}$.

Proof Fix ${\mathbf{S}}$, ${\mathbf{T}}$ and $R$. Then

$\begin{array}[]{lcl}(\mbox{\bf a};\mbox{\bf
c})_{{\mathbf{S}}}^{-1};R;(\mbox{\bf b};\mbox{\bf
d})_{{\mathbf{T}}}&\quad=&(\mbox{\bf a}_{{\mathbf{S}}};\mbox{\bf
c}_{{\mathbf{S}}(\mbox{\bf a})})^{-1};R;(\mbox{\bf b}_{{\mathbf{T}}};\mbox{\bf
d}_{{\mathbf{T}}(\mbox{\bf b})})\\\ &\quad=&(\mbox{\bf
c}_{{\mathbf{S}}(\mbox{\bf a})})^{-1};(\mbox{\bf
a}_{{\mathbf{S}}})^{-1};R;\mbox{\bf b}_{{\mathbf{T}}};\mbox{\bf
d}_{{\mathbf{T}}(\mbox{\bf b})}\end{array}$

Since $(\mbox{\bf a}_{{\mathbf{S}}})^{-1};R;\mbox{\bf b}_{{\mathbf{T}}}$ is a
total bisimulation between ${\mathbf{S}}(\mbox{\bf a})$ and
${\mathbf{T}}(\mbox{\bf b})$, we have the first assertion.

For the second, note that $(\mbox{\bf a}\sqcup\mbox{\bf
c})_{{\mathbf{S}}}^{-1};R;(\mbox{\bf b}\sqcup\mbox{\bf d})_{{\mathbf{T}}}$ is
the disjoint union of the total bisimulations $(\mbox{\bf
a}_{{\mathbf{S}}})^{-1};R;\mbox{\bf b}_{{\mathbf{T}}}$ and $(\mbox{\bf
c}_{{\mathbf{S}}})^{-1};R;\mbox{\bf d}_{{\mathbf{T}}}$.  $\dashv$

###### Proposition 2.6

Let a and b be standard updates. If $\varphi$ is preserved by bisimulations
and $\mbox{\bf a}\sim\mbox{\bf b}$, then $[\mbox{\bf
a}]{\mbox{\boldmath$\varphi$\unboldmath}}=[\mbox{\bf
b}]{\mbox{\boldmath$\varphi$\unboldmath}}$, and also $\langle\mbox{\bf
a}\rangle{\mbox{\boldmath$\varphi$\unboldmath}}=\langle\mbox{\bf
b}\rangle{\mbox{\boldmath$\varphi$\unboldmath}}$.

Proof We check the first assertion only. Fix ${\mathbf{S}}$, and let $s\in S$
be such that that $s\in([\mbox{\bf
a}]{\mbox{\boldmath$\varphi$\unboldmath}})_{{\mathbf{S}}}$. Let
$t\in{\mathbf{S}}(\mbox{\bf b})$ be such that $s\ \mbox{\bf b}_{{\mathbf{S}}}\
t$. We must show that
$t\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf b})}$.

The identity relation $I_{{\mathbf{S}}}$ is a total bisimulation on
${\mathbf{S}}$. Let $R=(\mbox{\bf
a}_{{\mathbf{S}}})^{-1};I_{{\mathbf{S}}};\mbox{\bf b}_{{\mathbf{S}}}$. The
definition of action equivalence $\sim$ implies that $R$ is a total
bisimulation between ${\mathbf{S}}(\mbox{\bf a})$ and ${\mathbf{S}}(\mbox{\bf
b})$. Let $u\in{\mathbf{S}}(\mbox{\bf a})$ be such that $u\ R\ t$. Thus there
is some $s^{\prime}\in S$ such that $u\ (\mbox{\bf a}_{{\mathbf{S}}})^{-1}\
s^{\prime}\ \mbox{\bf b}_{{\mathbf{S}}}\ t$. Since $(\mbox{\bf
a}_{{\mathbf{S}}})^{-1}$ is a partial function, we have $s^{\prime}=s$. Thus
$s\ \mbox{\bf a}_{{\mathbf{S}}}\ u$. Since $s\in([\mbox{\bf
a}]{\mbox{\boldmath$\varphi$\unboldmath}})_{{\mathbf{S}}}$, we have
$u\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf a})}$. And
as $\varphi$ is preserved by the bisimulation $R$, we have the desired
conclusion:
$t\in{\mbox{\boldmath$\varphi$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf b})}$.
$\dashv$

###### Proposition 2.7

Let a and b be standard. If $\mbox{\bf a}\sim\mbox{\bf b}$, then a and b have
the same domain. That is, for all state models ${\mathbf{S}}$, ${\it
dom}(\mbox{\bf a}_{{\mathbf{S}}})={\it dom}(\mbox{\bf b}_{{\mathbf{S}}})$.

Proof The domains are $(\langle\mbox{\bf a}\rangle\mbox{\sf\bf
tr})_{{\mathbf{S}}}$ and $(\langle\mbox{\bf b}\rangle\mbox{\sf\bf
tr})_{{\mathbf{S}}}$. So the result follows from Proposition 2.6 and the fact
that tr is preserved by bisimulations.  $\dashv$

Definition  An update r preserves bisimulations if the following two
conditions hold:

  1. 1.

If $s\ \mbox{\bf r}_{{\mathbf{S}}}\ s^{\prime}$ and
$({\mathbf{S}},s)\equiv({\mathbf{T}},t)$, then there is some $t^{\prime}$ such
that $t\ \mbox{\bf r}_{{\mathbf{T}}}\ t^{\prime}$ and $({\mathbf{S}}(\mbox{\bf
r}),s^{\prime})\equiv({\mathbf{T}}(\mbox{\bf r}),t^{\prime})$.

  2. 2.

If $t\ \mbox{\bf r}_{{\mathbf{T}}}\ t^{\prime}$ and
$({\mathbf{S}},s)\equiv({\mathbf{T}},t)$, then there is some $s^{\prime}$ such
that $s\ \mbox{\bf r}_{{\mathbf{S}}}\ s^{\prime}$ and $({\mathbf{S}}(\mbox{\bf
r}),s^{\prime})\equiv({\mathbf{T}}(\mbox{\bf r}),t^{\prime})$.

An action model ${\mathbf{\Sigma}}$ _preserves bisimulations_ if
$\mbox{pre}(\sigma)$ is preserved under bisimulations for all
$\sigma\in\Sigma$.

######  Proposition 2.8 ([4])

Concerning bisimulation preservation:

  1. 1.

The bisimulation preserving updates are closed under composition and
(infinitary) unions.

  2. 2.

If $\varphi$ is preserved by bisimulations and r preserves bisimulations, then
$[\mbox{\bf r}]{\mbox{\boldmath$\varphi$\unboldmath}}$ is preserved by
bisimulations.

######  Proposition 2.9 ([4])

Let ${\mathbf{\Sigma}}$ be a bisimulation-preserving action model. Let
$\Gamma\subseteq\Sigma$ be arbitrary. Then the update induced by
$({\mathbf{\Sigma}},\Gamma)$ preserves bisimulation.

Definition  Let ${\mathbf{\Sigma}}=(\Sigma,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre})$ and ${\mathbf{\Delta}}=(\Delta,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre})$ be action models. As this notation
indicates, we shall not introduce additional notation to differentiate the
arrows and the pre functions on these action models. A bisimulation between
${\mathbf{\Sigma}}$ and ${\mathbf{\Delta}}$ is a relation
$R\subseteq\Sigma\times\Delta$ such that whenever $\sigma\ R\ \delta$, the
following three properties hold:

  1. 1.

$\mbox{pre}(\sigma)=\mbox{pre}(\delta)$.

  2. 2.

For $A\in{\cal A}$ and $\sigma^{\prime}$ such that $\sigma\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma^{\prime}$, there is some $\delta^{\prime}$ such that
$\delta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\delta^{\prime}$ and $\sigma^{\prime}\ R\ \delta^{\prime}$.

  3. 3.

For $A\in{\cal A}$ and $\delta^{\prime}$ such that $\delta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\delta^{\prime}$, there is some $\sigma^{\prime}$ such that
$\sigma\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma^{\prime}$ and $\sigma^{\prime}\ R\ \delta^{\prime}$.

We write $\sigma\sim\delta$ if there is a bisimulation $R$ between
${\mathbf{\Sigma}}$ and ${\mathbf{\Delta}}$ such that $\sigma\ R\ \delta$.

Let $\pi=({\mathbf{\Sigma}},\Gamma)$ and $\rho=({\mathbf{\Delta}},B)$ be
program models. We write $\pi\sim\rho$ if there is a bisimulation between
${\mathbf{\Sigma}}$ and ${\mathbf{\Delta}}$ such that the following hold:

  1. 1.

Each $\sigma\in\Gamma$ belongs to the domain of $R$, and each $\delta\in B$
belongs to the image of $R$.

  2. 2.

If $\sigma\in\Gamma$ and $\sigma\ R\ \delta$, then $\delta\in B$.

  3. 3.

If $\delta\in B$ and $\sigma\ R\ \delta$, then $\sigma\in\Gamma$.

We write $\pi\sim\rho$ in this case.

###### Proposition 2.10

Equivalent bisimulation-preserving program models induce equivalent updates.

Proof Suppose that $R$ is a bisimulation showing that
$({\mathbf{\Sigma}},\Gamma)\sim({\mathbf{\Delta}},B)$. To check that the
induced updates are equivalent, let ${\mathbf{S}}$ and ${\mathbf{T}}$ be state
models, and let $R^{\prime}$ be a total bisimulation between them. We check
that
$(({\mathbf{\Sigma}},\Gamma)_{{\mathbf{S}}})^{-1};R^{\prime};({\mathbf{\Delta}},B)_{{\mathbf{T}}}$
is a total bisimulation between ${\mathbf{S}}({\mathbf{\Sigma}},\Gamma)$ and
${\mathbf{T}}({\mathbf{\Delta}},B)$. To save on some notation, call this
relation $Q$.

We verify the bisimulation properties of $Q$. Let $(s,\sigma)\ Q\ (t,\delta)$.
Recall that the updates induced by program models are standard. Hence we have

$(s,\sigma)\ (({\mathbf{\Sigma}},\Gamma)_{{\mathbf{S}}})^{-1}\ s\ R^{\prime}\
t\ ({\mathbf{\Delta}},B)_{{\mathbf{T}}}\ (t,\delta).$

It is clear from this that $(s,\sigma)$ and $(t,\delta)$ satisfy the same
atomic sentences. Suppose next that
$(s^{\prime},\sigma^{\prime})\in{\mathbf{S}}({\mathbf{\Sigma}},\Gamma)$ and
$(s,\sigma)\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(s^{\prime},\sigma^{\prime})$. Note that since
$(s^{\prime},\sigma^{\prime})\in{\mathbf{S}}({\mathbf{\Sigma}},\Gamma)$, we
also have $\sigma^{\prime}\in\Gamma$. Let $t^{\prime}$ be such that $t\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}t^{\prime}$ and $s^{\prime}\ R^{\prime}\ t^{\prime}$. Let
$\delta^{\prime}$ be such that $\delta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\delta^{\prime}$ and $\sigma^{\prime}\ R\ \delta^{\prime}$. We have
$\delta^{\prime}\in B$ by one of the conditions in the definition of
equivalence. Thus

$(s^{\prime},\sigma^{\prime})\
(({\mathbf{\Sigma}},\Gamma)_{{\mathbf{S}}})^{-1}\ s^{\prime}\ R^{\prime}\
t^{\prime}\ ({\mathbf{\Delta}},B)_{{\mathbf{T}}}\
(t^{\prime},\delta^{\prime}).$

And $(t,\delta)\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(t^{\prime},\delta^{\prime})$. This shows the second bisimulation
condition, and the third is similar.

For the totality of $Q$, let $(s,\sigma)\in S\otimes\Sigma$. Let $t\in T$ and
$\delta\in B$ be such that $s\ R^{\prime}\ t$ and $\sigma\ R\ \delta$. Then
$(t,\delta)\in T\otimes\Delta$ since $\mbox{pre}(\sigma)=\mbox{pre}(\delta)$,
and since this proposition is preserved by bisimulations. We have $(s,\sigma)\
Q\ (t,\delta)$ because

$(s,\sigma)\ (({\mathbf{\Sigma}},\Gamma)_{{\mathbf{S}}})^{-1}\ s\ R^{\prime}\
t\ ({\mathbf{\Delta}},B)_{{\mathbf{T}}}\ (t,\delta).$

This completes the verification that $Q$ is a total bisimulation.  $\dashv$

##  3 The languages ${\cal L}({\mathbf{\Sigma}})$

At this point, we have enough general definitions to present the syntax and
semantics of the language ${\cal L}({\mathbf{\Sigma}})$. Most of the remaining
parts of this paper study these languages.

###  3.1 The syntax and semantics of ${\cal L}({\mathbf{\Sigma}})$

Fix a action signature ${\mathbf{\Sigma}}$. We present in Figure 1 a logical
language ${\cal L}({\mathbf{\Sigma}})$ which we study in the remainder of this
paper. Actually, we have three languages there, the full language ${\cal
L}({\mathbf{\Sigma}})$ and the smaller fragments ${\cal
L}_{0}({\mathbf{\Sigma}})$ and ${\cal L}_{1}({\mathbf{\Sigma}})$.

The number $n$ which figures into the syntax is the number of action types in
$\Sigma$. In the programs of the form $\sigma\psi_{1}\cdots\psi_{n}$ we have
sentences $\vec{\psi}$ rather than epistemic propositions (which we had
written using boldface letters
${\mbox{\boldmath$\psi$\unboldmath}}_{1},\dots,{\mbox{\boldmath$\psi$\unboldmath}}_{n}$
in Section 2.2). Also, the signature ${\mathbf{\Sigma}}$ figures into the
semantics exactly in those programs $\sigma\psi_{1}\cdots\psi_{n}$; in those
we require that $\sigma\in\Sigma$.

The second thing to note is that, as in $PDL$, we have two sorts of syntactic
objects: sentences and programs. We call programs of the form
$\sigma\psi_{1}\cdots\psi_{n}$ basic actions. Note that they might not be
“atomic” in the sense that the sentences $\psi_{j}$ might themselves contain
programs.

$\begin{array}[]{lcc|c|c|c|c|c|c}\mbox{\bf sentences $\varphi$}&&{\sf
true}&p_{i}&\neg\varphi&\varphi\wedge\psi&\Box_{A}\varphi&\Box_{{\cal
B}}^{*}\varphi&[\pi]\varphi\\\ \mbox{\bf programs $\pi$}&&\mbox{\em
skip}&\mbox{\em
crash}&\sigma_{i}\psi_{1}\cdots\psi_{n}&\pi\sqcup\rho&\pi;\rho&\pi^{*}\end{array}$
$\begin{array}[]{lcl}[\\![{\sf true}]\\!]&\quad=&\mbox{\sf\bf tr}\\\
[\\![p]\\!]&\quad=&{\mbox{\boldmath$p$\unboldmath}}\\\
[\\![\varphi\wedge\psi]\\!]&\quad=&[\\![\varphi]\\!]\wedge[\\![\psi]\\!]\\\
[\\![\neg\varphi]\\!]&\quad=&\neg[\\![\varphi]\\!]\\\
[\\![\Box_{A}\varphi]\\!]&\quad=&\Box_{A}[\\![\varphi]\\!]\\\
[\\![\Box^{*}_{{\cal B}}\varphi]\\!]&\quad=&\Box^{*}_{{\cal
B}}[\\![\varphi]\\!]\\\
[\\![[\pi]\varphi]\\!]&\quad=&[[\\![\pi]\\!]][\\![\varphi]\\!]\\\
\end{array}\qquad\begin{array}[]{lcl}[\\![\mbox{\em
skip}]\\!]&\quad=&{\mbox{\boldmath$1$\unboldmath}}\\\ [\\![\mbox{\em
crash}]\\!]&\quad=&{\mbox{\boldmath$0$\unboldmath}}\\\
[\\![\sigma_{i}\psi_{1}\ldots\psi_{n}]\\!]&\quad=&({\mathbf{\Sigma}},\sigma_{i},[\\![\psi_{1}]\\!]\cdots[\\![\psi_{n}]\\!])\\\
[\\![\pi;\rho]\\!]&\quad=&[\\![\pi]\\!];[\\![\rho]\\!]\\\
[\\![\pi\sqcup\rho]\\!]&\quad=&[\\![\pi]\\!]\sqcup[\\![\rho]\\!]\\\
[\\![\pi^{*}]\\!]&\quad=&[\\![\pi]\\!]^{*}\\\ \\\ \end{array}$ For ${\cal
L}_{1}({\mathbf{\Sigma}})$, we drop the $\pi^{*}$ construct. For ${\cal
L}_{0}({\mathbf{\Sigma}})$, we drop the $\pi^{*}$ and $\Box^{*}_{{\cal B}}$
constructs.

Figure 1: The language ${\cal L}({\mathbf{\Sigma}})$ and its semantics, and
the fragments ${\cal L}_{0}({\mathbf{\Sigma}})$, and ${\cal
L}_{1}({\mathbf{\Sigma}})$.

We use the following standard abbreviations: ${\sf false}=\neg{\sf true}$,
$\varphi\vee\psi=\neg(\neg\varphi\wedge\neg\psi)$,
$\varphi\rightarrow\psi=\neg(\varphi\wedge\neg\psi)$,
$\Diamond_{A}\varphi=\neg\Box_{A}\neg\varphi$, $\Diamond^{*}_{{\cal
B}}=\neg\Box^{*}_{{\cal B}}\neg\varphi$, and
$\langle\pi\rangle\varphi=\neg[\pi]\neg\varphi$.

#### The semantics

defines two operations by simultaneous recursion on ${\cal
L}({\mathbf{\Sigma}})$:

  1. 1.

$\varphi\mapsto[\\![\varphi]\\!]$, taking the sentences of ${\cal
L}({\mathbf{\Sigma}})$ into epistemic propositions; and

  2. 2.

$\pi\mapsto[\\![\pi]\\!]$, taking the programs of ${\cal
L}({\mathbf{\Sigma}})$ into program models (and hence into induced updates).

The formal definition is given in Figure 1. The first map
$\varphi\mapsto[\\![\varphi]\\!]$ might be called the truth map for the
language. When we began our study of state models, we started with a
“valuation” (or a “truth” map) ${\|.\|}_{{\mathbf{S}}}\,:{\sf
AtSen}\rightarrow{\cal P}(S)$, assigning to each atomic sentence $p$ a set
$\|p\|_{{\mathbf{S}}}$ of states. The truth map here extends this to sentences
and actions of ${\cal L}({\mathbf{\Sigma}})$. The overall definition is by
simultaneous recursion on the ${\cal L}({\mathbf{\Sigma}})$. We employ the
standard device of speaking of the definition in terms of a temporal metaphor.
That is, we think of the definition of the semantics of a sentence or action
as coming “after” the definitions of its subsentences and subactions.

With one key exception, the operations on the right-hand sides are immediate
applications of our general definitions of the closure conditions on epistemic
propositions from Section 2.1 and the operations on program models from
Section 2.6. A good example to explain this is the clause for the semantics of
sentences $[\pi]\varphi$. Assuming that we have a program model
$[\\![\pi]\\!]$, we get an induced update in Section 2.5 which we again denote
$[\\![\pi]\\!]$. We also have an epistemic proposition $[\\![\varphi]\\!]$. We
can therefore form the epistemic proposition
$[[\\![\pi]\\!]][\\![\varphi]\\!]$ (see equation (2.4) in Section 2.2). Note
that we have overloaded the square bracket notation; this is intentional, and
we have done the same with other notation as well.

Similarly, the semantics of skip and crash are the program models $1$ and $0$
of Section 2.6.

We also discuss the definition of the semantics for basic actions
$\sigma_{i}\vec{\psi}$. For this, recall that we have a general definition of
a signature-based program model
$({\mathbf{\Sigma}},\Gamma,{\mbox{\boldmath$\psi$\unboldmath}}_{1},\ldots,{\mbox{\boldmath$\psi$\unboldmath}}_{n})$,
where $\Gamma\subseteq\Sigma$ and the $\psi$’s are any epistemic propositions.
What we have in the semantics of $\sigma_{i}\vec{\psi}$ is the special case of
this where $\Gamma$ is the singleton $\\{\sigma_{i}\\}$ and
${\mbox{\boldmath$\psi$\unboldmath}}_{i}$ is $[\\![\psi_{i}]\\!]$, a
proposition which we already have defined when we come to define
$[\\![\sigma_{i}\vec{\psi}]\\!]$.

###  3.2 Examples

In this section, we provide examples of the concepts from Sections 2.1–3.1.
These examples are chosen with an eye towards one of the inexpressivity
results in Sections 7.2 and 7.3 near the end of the paper. So we know that
they may appear artificial. Still, we trust that having a suitably detailed
example may help the reader.

In these examples, our set ${\sf AtSen}$ of atomic sentences is a two-element
set $\\{p,q\\}$, and the set ${\cal A}$ of agents is the two-element set
$\\{A,B\\}$.

First, here is a family of state models $C_{n}$ for even positive numbers $n$.
$C_{n}$ is a cycle of $5n$ points $a_{1},\ldots,a_{5n}$ arranged as follows:

$\textstyle{a_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{a_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{B}$$\textstyle{a_{3}}$$\textstyle{\cdots}$$\textstyle{a_{5n-1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{a_{5n}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{B}$$\textstyle{a_{1}}$

Since $n$ is even, for $1\leq i\leq 5$, the connection is $a_{in-1}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}a_{in}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{B}$}\hskip
7.22743pt$}a_{in+1}$. (We are taking subscripts modulo $5n$ here.) We also
specify that $p$ is true at all points except $a_{1}$ and $a_{2n+1}$, and $q$
is true only at $a_{4n+1}$.

Let ${\mathbf{\Sigma}}{\mbox{\scriptsize pub}}$ be the action signature given
by $\Sigma=\\{\mbox{\em Pub}\\}$, Pub
$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip 7.22743pt$Pub,
and Pub $\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{B}$}\hskip
7.22743pt$Pub. This action signature is one of the most important in the
applications since it is used in the representation of public announcements.

Then we have ${\cal L}({\mathbf{\Sigma}}{\mbox{\scriptsize pub}})$ and its
sublanguages ${\cal L}_{0}({\mathbf{\Sigma}}{\mbox{\scriptsize pub}})$ and
${\cal L}_{1}({\mathbf{\Sigma}}{\mbox{\scriptsize pub}})$. One example of a
sentence of ${\cal L}_{1}({\mathbf{\Sigma}}{\mbox{\scriptsize pub}})$ is
$\langle\mbox{\em Pub}\ p\rangle\Diamond_{A,B}^{*}q$. (Without abbreviations,
this would be $\neg[\mbox{\em Pub}\ p]\Box_{A,B}^{*}\neg q$.) The point of
this first example is to calculate $[\\![\langle\mbox{\em Pub}\
p\rangle\Diamond_{A,B}^{*}q]\\!]_{\scriptstyle C_{n}}$. This takes a few
steps.

The definitions tell us that $[\\![p]\\!]={\mbox{\boldmath$p$\unboldmath}}$,
and so

$[\\![p]\\!]_{\scriptstyle
C_{n}}\quad=\quad{\mbox{\boldmath$p$\unboldmath}}_{C_{n}}\quad=\quad\|p\|_{C_{n}}\quad=\quad\\{a_{i}:i\neq
1,2n+1\\}.$

We have a signature-based program model $({\mathbf{\Sigma}}{\mbox{\scriptsize
pub}},\mbox{\em Pub},{\mbox{\boldmath$p$\unboldmath}})$. (In more detail,
${\mathbf{\Sigma}}{\mbox{\scriptsize pub}}$ is an action signature, our
distinguished set $\Gamma\subseteq\Sigma$ is $\\{\mbox{\em Pub}\\}$ and
$\mbox{\sc Pre}(\mbox{\em Pub})$ is the the proposition $p$.) We can take the
update product of this with $C_{n}$ to get the model
$C_{n}\otimes({\mathbf{\Sigma}}{\mbox{\scriptsize pub}},\mbox{\em
Pub},{\mbox{\boldmath$p$\unboldmath}})$. The universe of this model is

$\\{(a_{i},\mbox{\em Pub}):1\leq i\leq 5n\ \&\ i\neq 1\ \&\ i\neq 2n+1\\}.$

The accessibilities are given by

$\textstyle{(a_{2},\mbox{\em
Pub})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{B}$$\textstyle{(a_{3},\mbox{\em
Pub})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{\cdots}$$\textstyle{(a_{2n-1},\mbox{\em
Pub})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{(a_{2n},\mbox{\em
Pub})}$$\textstyle{(a_{2n+1},\mbox{\em
Pub})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{(a_{2n+2},\mbox{\em
Pub})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{B}$$\textstyle{\cdots}$$\textstyle{(a_{5n-1},\mbox{\em
Pub})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{(a_{5n},\mbox{\em
Pub})}$

In this model $p$ is true at all points, and $q$ is true only at
$(a_{4n+1},\mbox{\em Pub})$. The update relation
$({\mathbf{\Sigma}}{\mbox{\scriptsize pub}},\mbox{\em
Pub},{\mbox{\boldmath$p$\unboldmath}})_{C_{n}}$ is

$\\{(a_{i},(a_{i},\mbox{\em Pub})):1\leq i\leq 5n\ \&\ i\neq 1\ \&\ i\neq
2n+1\\}.$

The intuition is that when we relativize the model to $p$ (that is, we update
the model with a public announcement of $p$), $a_{1}$ and $a_{2n+1}$
disappear. The cycle breaks into two disconnected components.

To save on notation, let us write $D_{n}$ for the model
$C_{n}\otimes({\mathbf{\Sigma}}{\mbox{\scriptsize pub}},\mbox{\em
Pub},{\mbox{\boldmath$p$\unboldmath}})$. It follows that

$[\\![q]\\!]_{\scriptstyle
D_{n}}\quad=\quad\|{\mbox{\boldmath$q$\unboldmath}}\|_{D_{n}}\quad=\quad\\{(a_{4n+1},\mbox{\em
Pub})\\},$

and therefore that

$[\\![\Diamond^{*}_{A,B}q]\\!]_{\scriptstyle
D_{n}}\quad=\quad(\Diamond^{*}_{A,B}{\mbox{\boldmath$q$\unboldmath}})_{D_{n}}\quad=\quad\\{(a_{i},\mbox{\em
Pub}):2n+1\leq i\leq 5n\\}.$

It now follows that

$\begin{array}[]{lcl}[\\![\langle\mbox{\em Pub}\
p\rangle\Diamond_{A,B}^{*}q]\\!]_{\scriptstyle
C_{n}}&\quad=&\\{a_{i}:(a_{i},\mbox{\em Pub})\in D_{n}\ \&\ (a_{i},\mbox{\em
Pub})\in[\\![\Diamond^{*}_{A,B}q]\\!]_{\scriptstyle D_{n}}\\}\\\
&\quad=&\\{a_{i}:2n+2\leq i\leq 5n\\}\end{array}$

Later, we are going to be especially interested in the points $a_{n+1}$ and
$a_{3n+1}$. The analysis above shows that $a_{n+1}$ does not belong to
$[\\![\langle\mbox{\em Pub}\ p\rangle\Diamond_{A,B}^{*}q]\\!]_{\scriptstyle
C_{n}}$, but $a_{3n+1}$ does belong to it. The intuition is that after we
relativize the original cycle to $p$ by deleting $a_{1}$ and $a_{2n+1}$, there
is no path from $a_{n+1}$ to $a_{4n+1}$. But even after we make the deletion,
there is a path from $a_{3n+1}$ to $a_{4n+1}$, and this is why $a_{3n+1}$
satisfies the sentence $\langle\mbox{\em Pub}\ p\rangle\Diamond_{A,B}^{*}q$.

#### A second example

We next consider a different example based on another action signature. This
is the action signature $\mbox{\em Pri}^{A}$ of completely private
announcements to $A$. It concerns two agents, $A$ and $B$, and it has
$\Sigma=\\{\mbox{\em Pri}^{A},\mbox{\em skip}\\}$. The fixed enumeration here
is that $\mbox{\em Pri}^{A}$ comes first and skip comes second. We also have
$\mbox{\em Pri}^{A}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\mbox{\em Pri}^{A}$, $\mbox{\em Pri}^{A}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{B}$}\hskip
7.22743pt$}\mbox{\em skip}$, skip
$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$skip, and skip
$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{B}$}\hskip
7.22743pt$skip.

${\cal L}_{1}({\mathbf{\Sigma}}{\mbox{\scriptsize pri}})$ contains the
sentence $\langle\mbox{\em Pri}^{A}\ p\,{\sf
true}\rangle\Diamond_{A}^{*}\Diamond_{B}\neg p$. We show in Section 7.3 that
this sentence is not expressible in ${\cal
L}_{1}({\mathbf{\Sigma}}{\mbox{\scriptsize pub}})$, even by a set of
sentences. We take this to be a formal confirmation that a logical system with
private announcements is more powerful than a system with only public
announcements.

Let $N^{+}$ be the set $\\{1,2,\ldots\\}$ of non-zero natural numbers. We
shall construct models ${\mathbf{S}}_{f}$, where $J\subseteq N^{+}$ and
$f\,:J\rightarrow N^{+}$. (Note that we leave the domain $J$ out of the
notation ${\mathbf{S}}_{f}$.) We also construct models ${\mathbf{T}}_{f,j}$
where $J\subseteq N^{+}$, $f\,:J\rightarrow N^{+}$, and $j\in J$. The models
${\mathbf{S}}_{f}$ and ${\mathbf{T}}_{f,j}$ have the same state set:

$\\{a,b\\}\cup\\{c^{i}_{k}:i\in J\mbox{ and }1\leq k\leq f(i)\\}.$

The atomic proposition $p$ is true at all points except $b$. The arrows in
${\mathbf{S}}_{f}$ are given by

  1. 1.

$x\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}x$ for all $x$.

  2. 2.

$a\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}b$.

  3. 3.

$b\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}c^{i}_{1}$ for all $i\in J$.

  4. 4.

$c^{i}_{k}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}b$ for all $i\in J$ and $1\leq i\leq f(i)$.

  5. 5.

$c^{i}_{f(i)}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{B}$}\hskip
7.22743pt$}b$ for all $i\in J$.

${\mathbf{T}}_{f,j}$ has all these arrows and exactly one more:

$a\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}c^{j}_{1}.$

The model ${\mathbf{S}}_{f}$ are shown in Figure 2. Note that we only show the
case when $J=\\{j,k\\}$; the general case is of course similar. We did not
show the reflexive
$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip 7.22743pt$
relations. And we remind the reader that ${\mathbf{T}}_{f,j}$ has one more
arrow.

|
---|---
$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{c^{j}_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{c^{j}_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{c^{j}_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{\cdots}$$\scriptstyle{A}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces
c^{j}_{f(j)}}$$\scriptstyle{B}$$\textstyle{c^{k}_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{\cdots}$$\scriptstyle{A}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces
c^{k}_{f(k)}}$$\scriptstyle{B}$

Figure 2: The model ${\mathbf{S}}_{f}$ for $J$ a two-element set $\\{j,k\\}$,
omitting the reflexive arrows.

We shall need to calculate
${\mathbf{S}}_{f}\otimes({\mathbf{\Sigma}}{\mbox{\scriptsize pri}},\mbox{\em
Pri}^{A},{\mbox{\boldmath$p$\unboldmath}},\mbox{\sf\bf tr})$. We need the same
thing for the models ${\mathbf{T}}_{f,j}$. To save on notation, we call the
updated models $\hat{{\mathbf{S}}}_{f}$ and $\hat{{\mathbf{T}}}_{f,j}$.
Finally, we need the update relations between ${\mathbf{S}}_{f}$ and
$\hat{{\mathbf{S}}}_{f}$ and between ${\mathbf{T}}_{f,j}$ and
$\hat{{\mathbf{T}}}_{f,j}$.

Here are some facts about the structure of $\hat{{\mathbf{S}}}_{f}$:

  1. 1.

$(a,\mbox{\em Pri}^{A})\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(a,\mbox{\em Pri}^{A})$.

  2. 2.

$(a,\mbox{\em Pri}^{A})\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(b,\mbox{\em Pri}^{A})$ does not hold in $\hat{{\mathbf{S}}}_{f}$.

  3. 3.

The only $\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$-successor of $(a,\mbox{\em Pri}^{A})$ is itself.

  4. 4.

$(x,\mbox{\em skip})\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}(y,\mbox{\em skip})$ whenever $x\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}x$ in ${\mathbf{S}}_{f}$; similarly for $(x,\mbox{\em
skip})\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{B}$}\hskip
7.22743pt$}(y,\mbox{\em skip})$.

  5. 5.

$c^{i}_{k}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}c^{i}_{k+1}$ for all $i\in J$ and $1\leq k<f(i)$.

The structure of $\hat{{\mathbf{T}}}_{f,j}$ differs from
$\hat{{\mathbf{S}}}_{f}$. Since $a\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}c^{j}_{1}$ in ${\mathbf{T}}_{f,j}$, we have a path in
$\hat{{\mathbf{T}}}_{f,j}$:

$(a,\mbox{\em Pri}^{A})\ \,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\ (c^{j}_{1},\mbox{\em Pri}^{A})\ \,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\\\ \ \cdots\ \,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\ (c^{j}_{f(j)},\mbox{\em Pri}^{A})\ \,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{B}$}\hskip
7.22743pt$}\ (b,\mbox{\em skip}).$

Once again, ${\mathbf{S}}_{f}$ contains no path from $(a,\mbox{\em Pri}^{A})$
to any other point, in particular, no path to $(b,\mbox{\em skip})$.

The update relation between ${\mathbf{S}}_{f}$ and $\hat{{\mathbf{S}}}_{f}$ is
$\\{(x,(x,\mbox{\em Pri}^{A})):x\neq b\\}.$ And from this, we see that

$\begin{array}[]{lcl}[\\![\langle\mbox{\em Pri}^{A}\ p,{\sf
true}\rangle\Diamond_{A}^{*}\Diamond_{B}\neg
p]\\!]_{\scriptstyle{\mathbf{S}}_{f}}&\quad=&\\{x:(x,\mbox{\em
Pri}^{A})\in[\\![\Diamond_{A}^{*}\Diamond_{B}\neg
p]\\!]_{\scriptstyle\hat{{\mathbf{S}}}_{f}}\\}\\\ &\quad=&\\{c^{i}_{k}:i\in
J\mbox{ and }1\leq k\leq f(i)\\}\end{array}$

In particular, $a\notin[\\![\langle\mbox{\em Pri}^{A}\ p,{\sf
true}\rangle\Diamond_{A}^{*}\Diamond_{B}\neg
p]\\!]_{\scriptstyle{\mathbf{S}}_{f}}$.

The update relation between ${\mathbf{T}}_{f,j}$ and
$\hat{{\mathbf{T}}}_{f,j}$ is the same, and this time

$\begin{array}[]{lcl}[\\![\langle\mbox{\em Pri}^{A}\ p,{\sf
true}\rangle\Diamond_{A}^{*}\Diamond_{B}\neg
p]\\!]_{\scriptstyle{\mathbf{T}}_{f,j}}&\quad=&\\{x:(x,\mbox{\em
Pri}^{A})\in[\\![\Diamond_{A}^{*}\Diamond_{B}\neg
p]\\!]_{\scriptstyle\hat{{\mathbf{T}}}_{f,j}}\\}\\\ &\quad=&\\{x:x\neq b\\}\\\
\end{array}$

And this time, $a\in[\\![\langle\mbox{\em Pri}^{A}\ p,{\sf
true}\rangle\Diamond_{A}^{*}\Diamond_{B}\neg
p]\\!]_{\scriptstyle{\mathbf{S}}_{f}}$.

In Section 7.3, we shall use these models to prove that our sentence
$\langle\mbox{\em Pri}^{A}\ p,{\sf
true}\rangle\Diamond_{A}^{*}\Diamond_{B}\neg p$ is not expressible by any
sentence or even any set of sentences using public announcements only. The
proof does not use any of our other results, and the reader may turn to it at
this point.

###  3.3 Basic properties

###### Proposition 3.1

Let $\varphi$ be a sentence of ${\cal L}({\mathbf{\Sigma}})$, and let $\alpha$
be an action of ${\cal L}({\mathbf{\Sigma}})$. Then

  1. 1.

$[\\![\varphi]\\!]$ is preserved by bisimulation.

  2. 2.

$[\\![\alpha]\\!]$ is standard and preserves bisimulation.

Proof By induction on ${\cal L}({\mathbf{\Sigma}})$. For ${\sf true}$ and the
atomic sentences $p_{i}$, we use Proposition 2.4. The same result takes care
of the induction steps for all the sentential operators except $[\pi]\varphi$.
For this, we use Proposition 2.8 part 2, and also the induction hypothesis.
Turning to the programs, the standardness comes from Proposition 2.1 and the
observation that signature-based program models induce standard updates. The
assertion that the interpretation of programs of ${\cal L}({\mathbf{\Sigma}})$
preserve bisimulation comes from Proposition 2.8 part 1; for the programs
$\sigma_{i}\vec{\psi}$ we use Proposition 2.9 and the induction hypothesis.
$\dashv$

In what follows, we shall use Proposition 3.1 without mentioning it.

##  4 The logical system for validity of ${\cal L}({\mathbf{\Sigma}})$
sentences

We write $\models\varphi$ to mean that for all state models ${\mathbf{S}}$ and
all $s\in S$, $s\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$. In this
case, we say that $\varphi$ is valid.

#### Sublanguages

We are of course interested in the full languages ${\cal
L}({\mathbf{\Sigma}})$. As have already been mentioned, the satisfiability
problems for these languages are in general not recursively axiomatizable.
(See [16] for details on this.) This is one of the reasons we also consider
sublanguages ${\cal L}_{0}({\mathbf{\Sigma}})$ and ${\cal
L}_{1}({\mathbf{\Sigma}})$: ${\cal L}_{1}({\mathbf{\Sigma}})$ is the fragment
without the action iteration construct $\pi^{*}$; ${\cal
L}_{0}({\mathbf{\Sigma}})$ is the fragment without $\pi^{*}$ and
$\Box^{*}_{{\cal B}}$. It turns out that ${\cal L}_{0}({\mathbf{\Sigma}})$ is
the easiest to study: it is of the same expressive power as ordinary multi-
modal logic. The main completeness result of the paper is a sound and complete
proof system for the validities in ${\cal L}_{1}({\mathbf{\Sigma}})$.

In Figure 3 below we present a logic for ${\cal L}({\mathbf{\Sigma}})$. We
write $\vdash\varphi$ if $\varphi$ can be obtained from the axioms of the
system using its inference rules. We often omit the turnstile $\vdash$ when it
is clear from the context.

#### Logics generated by families of signatures

Given a family $\mathcal{S}$ of action signatures, we would like to combine
all the logics $\\{{\cal
L}({\mathbf{\Sigma}})\\}_{{\mathbf{\Sigma}}\in\mathcal{S}}$ into a single
logic. Let us assume the signatures ${\mathbf{\Sigma}}\in\mathcal{S}$ are
mutually disjoint (otherwise, just choose mutually disjoint copies of these
signatures). We define the logic ${\cal L}(\mathcal{S})$ generated by the
family $\mathcal{S}$ in the following way: the syntax is defined by taking the
same definition we had in Figure 1 for the syntax of ${\cal
L}({\mathbf{\Sigma}})$, but in which on the side of the programs we take
instead as basic actions all expressions of the form

$\sigma_{i}\psi_{1}\cdots\psi_{n}$

where $\sigma\in\Sigma$, for some signature ${\mathbf{\Sigma}}\in\mathcal{S}$,
and $n$ is the length of the listing of non-trivial action types of
${\mathbf{\Sigma}}$. The semantics is again given by the same definition as in
Figure 1, but in which the clause about $\sigma\psi_{1}\cdots\psi_{n}$ refers
to the appropriate signature: for every ${\mathbf{\Sigma}}\in\mathcal{S}$,
every $\sigma\in\Sigma$, if $n$ is the length of the listing of
${\mathbf{\Sigma}}$, then

$[\\![\sigma_{i}\psi_{1}\cdots\psi_{n}]\\!]\quad=\quad({\mathbf{\Sigma}},\sigma,[\\![\psi_{1}]\\!],\ldots,[\\![\psi_{n}]\\!]).$

$\begin{array}[]{rlll}&\mbox{\bf Basic Axioms}\\\ &\mbox{All sentential
validities}\\\
&\mbox{($[\pi]$-normality)}&\vdash[\pi](\varphi\rightarrow\psi)\rightarrow([\pi]\varphi\rightarrow[\pi]\psi)\\\
&\mbox{($\Box_{A}$-normality)}&\vdash\Box_{A}(\varphi\rightarrow\psi)\rightarrow(\Box_{A}\varphi\rightarrow\Box_{A}\psi)&\\\
{*}&\mbox{($\Box^{*}_{{\cal C}}$-normality)}&\vdash\Box^{*}_{{\cal
C}}(\varphi\rightarrow\psi)\rightarrow(\Box^{*}_{{\cal
C}}\varphi\rightarrow\Box^{*}_{{\cal C}}\psi)&\\\ \\\ &\mbox{\bf Action
Axioms}&\\\ &\mbox{(Atomic
Permanence)}&\vdash[\sigma_{i}\vec{\psi}]p\leftrightarrow(\psi_{i}\rightarrow
p)\\\ &\mbox{(Partial
Functionality})&\vdash[\sigma_{i}\vec{\psi}]\neg\chi\leftrightarrow(\psi_{i}\rightarrow\neg[\sigma_{i}\vec{\psi}]\chi)&\\\
&\mbox{(Action-
Knowledge)}&\vdash[\sigma_{i}\vec{\psi}]\Box_{A}\varphi\leftrightarrow(\psi_{i}\rightarrow\bigwedge\\{\Box_{A}[\sigma_{j}\vec{\psi}]\varphi:\sigma_{i}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}\mbox{ in ${\mathbf{\Sigma}}$}\\})&\\\ \\\ {**}&\mbox{\bf
Action Mix
Axiom}&\vdash[\pi^{*}]\varphi\rightarrow\varphi\wedge[\pi][\pi^{*}]\varphi\\\
{*}&\mbox{\bf Epistemic Mix Axiom}&\vdash\Box^{*}_{{\cal
C}}\varphi\rightarrow\varphi\wedge\bigwedge\\{\Box_{A}\Box^{*}_{{\cal
C}}\varphi:A\in{\cal C}\\}\\\ \\\ &\mbox{\bf Skip Axiom}&\vdash[\mbox{\em
skip}]\varphi\leftrightarrow\varphi\\\ &\mbox{\bf Crash
Axiom}&\vdash[\mbox{\em crash}]{\sf false}\\\ &\mbox{\bf Composition
Axiom}&\vdash[\pi][\rho]\varphi\leftrightarrow[\pi;\rho]\varphi\\\ &\mbox{\bf
Choice
Axiom}&\vdash[\pi\sqcup\rho]\varphi\leftrightarrow[\pi]\varphi\wedge[\rho]\varphi\\\
\\\ \hline\cr\\\ &\mbox{\bf Modal Rules}\\\ &\mbox{(Modus Ponens)}&\mbox{From
}\vdash\varphi\mbox{ and }\vdash\varphi\rightarrow\psi,\mbox{ infer
}\vdash\psi\\\ &\mbox{($[\pi]$-necessitation)}&\mbox{From }\vdash\psi,\mbox{
infer }\vdash[\pi]\psi\\\ &\mbox{($\Box_{A}$-necessitation)}&\mbox{From
}\vdash\varphi,\mbox{ infer }\vdash\Box_{A}\varphi&\\\
{*}&\mbox{($\Box^{*}_{{\cal C}}$-necessitation)}&\mbox{From
}\vdash\varphi,\mbox{ infer }\vdash\Box^{*}_{{\cal C}}\varphi\\\ \\\
{**}&\mbox{\bf Program Induction Rule}&\mbox{From
}\vdash\chi\rightarrow\psi\wedge[\pi]\chi,\mbox{infer
}\vdash\chi\rightarrow[\pi^{*}]\psi\\\ {*}&\mbox{\bf Action Rule}\\\
\end{array}$ Let $\psi$ be a sentence, let $\alpha$ be a simple action, and
let ${\cal C}$ be a set of agents. Let there be sentences $\chi_{{\beta}}$ for
all ${\beta}$ such that ${\alpha}\rightarrow_{{\cal C}}^{*}{\beta}$ (including
${\alpha}$ itself), and such that 1.
$\vdash\chi_{{\beta}}\rightarrow[{\beta}]\psi$; 2. if $A\in{\cal C}$ and
${\beta}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}{\gamma}$, then $\vdash(\chi_{{\beta}}\wedge\mbox{\sc
Pre}(\beta))\rightarrow\Box_{A}\chi_{\gamma}$. From these assumptions, infer
$\vdash\chi_{{\alpha}}\rightarrow[{\alpha}]\Box_{{\cal C}}^{*}\psi$.

Figure 3: The logical system for ${\cal L}({\mathbf{\Sigma}})$. For ${\cal
L}_{1}({\mathbf{\Sigma}})$, we drop the ${**}$ axioms and rule; for ${\cal
L}_{0}({\mathbf{\Sigma}})$, we also drop the $*$ axioms and rules. The
definition of Pre in the Action Rule is given in Section 5.1.

###  4.1 Soundness of the axioms

In this section, we check the soundness of the axioms of the system. The basic
axioms are all routine, and so we omit the details on them.

###### Proposition 4.1

The Atomic Permanence Axiom
$[\sigma_{i}\vec{\psi}]p\leftrightarrow(\psi_{i}\rightarrow p)$ is sound.

Proof Recall from Section 2.7 how $[\\![\sigma_{i}\vec{\psi}]\\!]$ works; call
this update r. Fix a state model ${\mathbf{S}}$. The following are equivalent:

  1. 1.

$s\in[\\![[\sigma_{i}\vec{\psi}]{p}]\\!]_{\scriptstyle{\mathbf{S}}}$.

  2. 2.

$s\in([\mbox{\bf
r}]{{\mbox{\boldmath$p$\unboldmath}}})_{\scriptstyle{\mathbf{S}}}$.

  3. 3.

If $s\ {\mbox{\bf r}}_{{\mathbf{S}}}\ t$, then
$t\in{\mbox{\boldmath$p$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf r})}$.

  4. 4.

If $(s,\sigma_{i})\in{\mathbf{S}}(\mbox{\bf r})$, then
$(s,\sigma_{i})\in{\mbox{\boldmath$p$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf
r})}$.

  5. 5.

If $s\in[\\![\psi_{i}]\\!]_{\scriptstyle{\mathbf{S}}}$, then
$s\in\|p\|_{{\mathbf{S}}}={\mbox{\boldmath$p$\unboldmath}}_{{\mathbf{S}}}$.

  6. 6.

$s\in[\\![\psi_{i}\rightarrow{p}]\\!]_{\scriptstyle{\mathbf{S}}}$.

Most of the individual equivalences are easy, and we only comment on
(3)$\Longleftrightarrow$(4) and (4)$\Longleftrightarrow$(5). the definition of
the update $\mbox{\bf r}=({\mathbf{\Sigma}},\sigma_{i})$ implies that
${\mathbf{S}}(\mbox{\bf r})={\mathbf{S}}\otimes{\mathbf{\Sigma}}$. And
$\mbox{\bf r}_{{\mathbf{S}}}$ has the property that everything which $s\in S$
is related to by $\mbox{\bf r}_{{\mathbf{S}}}$ is of the form
$(s,\sigma_{i})$, where $\sigma_{i}$ is from the statement of this axiom and
$(s,\sigma_{i})\in{\mathbf{S}}(\mbox{\bf r})$. These points imply the
equivalence (3)$\Longleftrightarrow$(4). For (4)$\Longleftrightarrow$(5) note
that $(s,\sigma_{i})\in{\mathbf{S}}(\mbox{\bf r})$ iff
$s\in\mbox{pre}(\sigma_{i})_{{\mathbf{S}}}=[\\![\psi_{i}]\\!]_{\scriptstyle{\mathbf{S}}}$;
also the definition of the update product in equation (2.7) implies that
$(s,\sigma_{i})\in{\mbox{\boldmath$p$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf
r})}$ iff $s\in\|p\|_{{\mathbf{S}}}$.  $\dashv$

###### Proposition 4.2

The Partial Functionality Axiom
$[\sigma_{i}\vec{\psi}]\neg\chi\leftrightarrow(\psi_{i}\rightarrow\neg[\sigma_{i}\vec{\psi}]\chi)$
is sound.

Proof Again, let $\mbox{\bf r}=[\\![\sigma_{i}\vec{\psi}]\\!]$. Also, let
${\mbox{\boldmath$\chi$\unboldmath}}=[\\![\chi]\\!]$. Fix a state model
${\mathbf{S}}$. The following are equivalent:

  1. 1.

$s\in[\\![[\sigma_{i}\vec{\psi}]\neg\chi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  2. 2.

$s\in([\mbox{\bf
r}]{\neg{\mbox{\boldmath$\chi$\unboldmath}}})_{\scriptstyle{\mathbf{S}}}$.

  3. 3.

If $s\ {\mbox{\bf r}}_{{\mathbf{S}}}\ t$, then
$t\in\neg{\mbox{\boldmath$\chi$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf r})}$.

  4. 4.

If $s\ {\mbox{\bf r}}_{{\mathbf{S}}}\ t$, then
$t\notin{\mbox{\boldmath$\chi$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf r})}$.

  5. 5.

If $s\in[\\![\psi_{i}]\\!]_{\scriptstyle{\mathbf{S}}}$, then
$(s,\sigma_{i})\notin([\mbox{\bf
r}]{\mbox{\boldmath$\chi$\unboldmath}})_{{\mathbf{S}}}$.

  6. 6.

If $s\in[\\![\psi_{i}]\\!]_{\scriptstyle{\mathbf{S}}}$, then
$s\notin\neg{\mbox{\boldmath$\chi$\unboldmath}}_{{\mathbf{S}}(\mbox{\bf r})}$.

  7. 7.

If $s\in[\\![\psi_{i}]\\!]_{\scriptstyle\mathbf{S}}$, then
$s\in(\neg[\mbox{\bf r}]{\mbox{\boldmath$\chi$\unboldmath}})_{{\mathbf{S}}}$.

  8. 8.

$s\in[\\![\psi_{i}\rightarrow\neg[\mbox{\bf
r}]{\mbox{\boldmath$\chi$\unboldmath}}]\\!]_{\scriptstyle{\mathbf{S}}}$.

The crucial equivalence here is (6)$\Longrightarrow$(5). The reason this holds
is that in the action model for $\sigma_{i}\vec{\psi}$, there is just one
distinguished world. So for each fixed $s\in S$, there is at most one $t$ such
that $s\ {\mbox{\bf r}}_{{\mathbf{S}}}\ t$; i.e., $(s,\sigma_{i})$.  $\dashv$

###### Proposition 4.3

The Action-Knowledge Axiom

$[\sigma_{i}\vec{\psi}]\Box_{A}\varphi\leftrightarrow(\psi_{i}\rightarrow\bigwedge\\{\Box_{A}[\sigma_{j}\vec{\psi}]\varphi:\sigma_{i}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}\mbox{ in ${\mathbf{\Sigma}}$}\\})$

is sound.

Proof Again let $\mbox{\bf r}=[\\![\sigma_{i}\vec{\psi}]\\!]$. Fix a state
model ${\mathbf{S}}$. The following are equivalent:

  1. 1.

$s\in[\\![[\sigma_{i}\vec{\psi}]\Box_{A}\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  2. 2.

$s\in[\mbox{\bf r}][\\![\Box_{A}\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  3. 3.

If $s\ {\mbox{\bf r}}_{{\mathbf{S}}}\ u$, then
$u\in[\\![\Box_{A}\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf r})}$.

  4. 4.

If $s\in[\\![\psi_{i}]\\!]_{\scriptstyle{\mathbf{S}}}$, then
$(s,\sigma_{i})\in[\\![\Box_{A}\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf
r})}$.

  5. 5.

If $(s,\sigma_{i})\in{\mathbf{S}}(\mbox{\bf r})$, then for all
$(t,\sigma_{j})$ such that $(t,\sigma_{j})\in{\mathbf{S}}(\mbox{\bf r})$,
$s\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}t$ and $\sigma_{i}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}$, we have
$(t,\sigma_{j})\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf r})}$.

  6. 6.

If $(s,\sigma_{i})\in{\mathbf{S}}(\mbox{\bf r})$, then for all $t$ and all
$\sigma_{j}$ such that $s\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}t$ and $\sigma_{i}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}$: if $(t,\sigma_{j})\in{\mathbf{S}}(\mbox{\bf r})$, then
$(t,\sigma_{j})\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf r})}$.

  7. 7.

If $(s,\sigma_{i})\in{\mathbf{S}}(\mbox{\bf r})$, then for all $t$ and
$\sigma_{j}$ such that $s\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}t$ and $\sigma_{i}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}$:
$t\in[\\![[\sigma_{j}\vec{\psi}]\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  8. 8.

If $s\in[\\![\psi_{i}]\\!]_{\scriptstyle{\mathbf{S}}}$, then for all
$\sigma_{j}$ such that $\sigma_{i}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}$,
$s\in[\\![\Box_{A}[\sigma_{j}\vec{\psi}]\varphi]\\!]_{\scriptstyle\mathbf{S}}$.

  9. 9.

$s\in[\\![\psi_{i}\rightarrow\bigwedge\\{\Box_{A}[\sigma_{j}\vec{\psi}]\varphi:\sigma_{i}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}\\}]\\!]_{\scriptstyle{\mathbf{S}}}$.

$\dashv$

###### Proposition 4.4

The Action Mix Axiom
$[\pi^{*}]\varphi\rightarrow\varphi\wedge[\pi][\pi^{*}]\varphi$ is sound. The
Program Induction Rule is also sound: from
$\vdash\chi\rightarrow\psi\wedge[\pi]\chi$, infer
$\vdash\chi\rightarrow[\pi^{*}]\psi$.

Proof These are standard.  $\dashv$

###### Proposition 4.5

The Skip Axiom $[\mbox{\it skip\/}]\varphi\leftrightarrow\varphi$ is sound.

Proof Fix a state model ${\mathbf{S}}$. Recall that the semantics of skip is
the update $1$. So the following are equivalent:

  1. 1.

$s\in[\\![[\mbox{\em skip}]\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  2. 2.

If $s\ {{\mbox{\boldmath$1$\unboldmath}}}_{{\mathbf{S}}}\ t$, then
$t\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}({\mbox{\boldmath$1$\unboldmath}})}$.

  3. 3.

$s\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

$\dashv$

###### Proposition 4.6

The Crash Axiom $[\mbox{\it crash\/}]{\sf false}$ is sound.

Proof Recall that $[\\![\mbox{\em
crash}]\\!]={\mbox{\boldmath$0$\unboldmath}}$, the update such that
${\mathbf{S}}({\mbox{\boldmath$0$\unboldmath}})$ is the empty model, and
${\mbox{\boldmath$0$\unboldmath}}_{{\mathbf{S}}}$ is the empty relation.
Working through the definitions, $[\mbox{\em crash}]{\sf false}$ is easily
seen to hold vacuously.  $\dashv$

###### Proposition 4.7

The Composition Axiom $[\pi;\rho]\varphi\leftrightarrow[\pi][\rho]\varphi$ is
sound.

Proof Write r for $[\\![\pi]\\!]$ and b for $[\\![\rho]\\!]$. Fix a state
model ${\mathbf{S}}$. The following are equivalent:

  1. 1.

$s\in[\\![[\pi;\rho]\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  2. 2.

If $s\ {[\\![\pi;\rho]\\!]}_{{\mathbf{S}}}\ u$, then
$u\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf r};\mbox{\bf b})}$.

  3. 3.

If $s\ {(\mbox{\bf r};\mbox{\bf b})}_{{\mathbf{S}}}\ u$, then
$u\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf r};\mbox{\bf b})}$.

  4. 4.

If $s\ {\mbox{\bf r}}_{{\mathbf{S}}}\ t$ and $t\ {\mbox{\bf
b}}_{{\mathbf{S}}(\mbox{\bf r})}\ u$, then
$u\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf r};\mbox{\bf b})}$.

  5. 5.

If $s\ {\mbox{\bf r}}_{{\mathbf{S}}}\ t$, then
$t\in[\\![[\rho]\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf r})}$.

  6. 6.

$s\in[\\![[\pi][\rho]\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

The equivalence of (3) and (4) is by the definition of relational composition.
The remaining equivalences are from the semantic definitions. The equivalence
of (4) and (5) is by the fact that ${\mathbf{S}}(\mbox{\bf r};\mbox{\bf
b})={\mathbf{S}}(\mbox{\bf r})(\mbox{\bf b})$.  $\dashv$

###### Proposition 4.8

The Choice Axiom
$[\pi\sqcup\rho]\varphi\leftrightarrow[\pi]\varphi\wedge[\rho]\varphi$ is
sound.

Proof Fix a state model ${\mathbf{S}}$; we drop ${\mathbf{S}}$ from the
notation in the rest of this proof. Write $\gamma$ for $\pi\sqcup\rho$, r for
$[\\![\pi]\\!]$, b for $[\\![\rho]\\!]$, and c for $[\\![\gamma]\\!]$. Then
the following are equivalent:

  1. 1.

$s\in[\\![[\pi\sqcup\rho]\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  2. 2.

If $s\ {\mbox{\bf c}}\ u$, then
$u\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf c})}$.

  3. 3.

If $s\ {\mbox{\bf r}}\ t$, then
$t\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf c})}$; and if $s\
{\mbox{\bf b}}\ t^{\prime}$, then
$t^{\prime}\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf c})}$.

  4. 4.

If $s\ {\mbox{\bf r}}\ t$, then
$t\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf r})}$; and if $s\
{\mbox{\bf b}}\ t^{\prime}$, then
$t^{\prime}\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}(\mbox{\bf b})}$.

  5. 5.

$s\in[\\![[\pi]\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$ and
$s\in[\\![[\rho]\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  6. 6.

$s\in[\\![[\pi]\varphi\wedge[\rho]\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

The equivalence (2)$\Longleftrightarrow$(3) comes from the fact that each of
the $u$ such that $s\ {\mbox{\bf c}}\ u$ is either either (a) an element $t$
of ${\mathbf{S}}(\mbox{\bf r})$ related to $s$ by r, or else (b) an element
$t^{\prime}$ of ${\mathbf{S}}(\mbox{\bf b})$ related to $s$ by b. This is by
the definition of $\mbox{\bf r}\sqcup\mbox{\bf b}$.

We show the equivalence (3)$\Longleftrightarrow$(4) by considering the cases
(a) and (b) noted just above. We use the fact that the natural injections of
${\mathbf{S}}(\mbox{\bf r})$ and ${\mathbf{S}}(\mbox{\bf b})$ in
${\mathbf{S}}(\mbox{\bf c})$ are bisimulations, and also the fact that
$[\\![\varphi]\\!]$ is preserved by bisimulations (see Proposition 3.1).
$\dashv$

##  5 The Action Rule

Recall that our logical system is listed in Figure 3 above. We have shown the
soundness of all of the axioms and rules, except for the Action Rule. But
before we can even define the operation Pre that figures into the Action Rule,
we need to discuss a structure that comes up in our work, the canonical action
model ${\mathbf{\Omega}}$. And even after we define ${\mathbf{\Omega}}$, there
is a fair amount of work to do before we can prove the soundness of the Action
Rule.

###  5.1 The canonical action model ${\mathbf{\Omega}}$

Recall that we defined action models and program models in Sections 2.3. At
this point, we define the canonical action model ${\mathbf{\Omega}}$.

Definition  A basic action is a program of the form $\sigma\vec{\psi}$. A
simple action of ${\cal L}({\mathbf{\Sigma}})$ is a program in which neither
the program sum operation $\sqcup$ nor the iteration operation $\pi^{*}$
occur. We use letters like $\alpha$ and $\beta$ to denote simple actions only.

#### The canonical action model ${\mathbf{\Omega}}$

We define a program model ${\mathbf{\Omega}}$ in several steps. The actions of
the model ${\mathbf{\Omega}}$ (that is, the elements of its carrier set) are
the simple actions of the language ${\cal L}({\mathbf{\Sigma}})$ (as defined
just above). For all $A$, the accessibility relation
$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip 7.22743pt$ is
the smallest relation such that

  1. 1.

skip $\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$skip.

  2. 2.

$\sigma_{i}\vec{\varphi}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}\vec{\psi}$ iff $\sigma_{i}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\sigma_{j}$ in ${\mathbf{\Sigma}}$ and $\vec{\varphi}=\vec{\psi}$.

  3. 3.

If $\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\alpha^{\prime}$ and $\beta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime}$, then $\alpha;\beta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\alpha^{\prime};\beta^{\prime}$.

###### Proposition 5.1

As a frame, ${\mathbf{\Omega}}$ is locally finite: for each simple $\alpha$,
there are only finitely many $\beta$ such that $\alpha\,\lower
1.0pt\hbox{$\\!\longrightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{\\!\\!{\cal
A}^{*}}$}\hskip 7.22743pt$}\beta$.

Proof By induction on $\alpha$; we use heavily the fact that the accessibility
relations on ${\mathbf{\Omega}}$ are the smallest family with their defining
property. For the simple action expressions $\sigma\vec{\psi}$, we use the
assumption that the action model ${\mathbf{\Sigma}}$ underlying all our
definitions is finite. (Taking it to be locally finite would also be
sufficient.)  $\dashv$

Next, we define $\mbox{\sc Pre}\,:\Omega\rightarrow{\cal
L}_{1}({\mathbf{\Sigma}})$ by recursion so that

$\begin{array}[]{lcl}\mbox{\sc Pre}(\mbox{\em skip})&\quad=&{\sf true}\\\
\mbox{\sc Pre}(\mbox{\em crash})&\quad=&{\sf false}\\\ \mbox{\sc
Pre}(\sigma_{i}\vec{\psi})&\quad=&\psi_{i}\\\ \mbox{\sc
Pre}(\alpha;\beta)&\quad=&\langle\alpha\rangle\mbox{\sc Pre}(\beta)\\\
\end{array}$

This function Pre is not the function pre which is part of the structure of an
epistemic action model. However, there is a connection: We are in the midst of
defining the epistemic action model ${\mathbf{\Omega}}$, and its pre function
is defined in terms of Pre.

Another point: the clause in the definition of Pre could read $\mbox{\sc
Pre}(\alpha;\beta)=\mbox{\sc Pre}(\alpha)\wedge[{\alpha}]\mbox{\sc
Pre}(\beta)$. This is equivalent to what we have above. It is sometimes
tempting to think that the definition should be $\mbox{\sc
Pre}(\alpha;\beta)=\mbox{\sc Pre}(\alpha)\wedge\langle{\alpha}\rangle\mbox{\sc
Pre}(\beta)$. But in this, the first conjunct is redundant:
$\langle{\alpha}\rangle\mbox{\sc Pre}(\beta)$ implies $\mbox{\sc
Pre}(\alpha)$.

We set

$\mbox{pre}(\sigma)\quad=\quad[\\![\mbox{\sc Pre}(\sigma)]\\!].$

This simple action model ${\mathbf{\Omega}}$ is the canonical epistemic action
model; it plays the same role in our work as the canonical model in modal
logic.

Remark  The structure $(\Omega,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{\sc Pre})$ is entirely syntactic. It is _not_ an
action model. This contrasts with the canonical action model
${\mathbf{\Omega}}=(\Omega,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{pre})$; the last component of this structure is
semantic. The syntactic structure $(\Omega,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{{\cal
A}}$}\hskip 7.22743pt$},\mbox{\sc Pre})$ is the one which is actually used in
the statement of the Action Rule of the logical system. We emphasize this
point to allay any suspicion that our logical system is formulated in terms of
semantic concepts.

This is also perhaps a good place to remind the reader that neither Pre nor
pre is a first-class symbol in ${\cal L}({\mathbf{\Sigma}})$; it is only a
defined symbol. In Section 6 below we shall introduce another language called
${\cal L}_{1}^{+}({\mathbf{\Sigma}})$. In that language, Pre will be a first-
class function symbol.

###  5.2 The main result about ${\mathbf{\Omega}}$

Definition  For any $\alpha\in\Omega$, let $\hat{\alpha}$ be the program model
$({\mathbf{\Omega}},\\{\alpha\\})$. As in Section 2.5, we use the same
notation $\hat{\alpha}$ to denote induced update. (However, it will be
important to distinguish the two uses, and so we speak of the program model
$\hat{\alpha}$ and also the update $\hat{\alpha}$.)

###### Theorem 5.2

Let $\alpha\in\Omega$. Then there is a signature-based program model
$({\mathbf{\Delta}},\delta_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})$
such that

  1. 1.

As updates,
$[\\![\alpha]\\!]\sim({\mathbf{\Delta}},\delta_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})$.

  2. 2.

As propositions, $\mbox{pre}(\alpha)={\mbox{\boldmath$\psi$\unboldmath}}_{i}$.

  3. 3.

As program models,
$({\mathbf{\Delta}},\delta_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})\sim\hat{\alpha}$.

In particular, as updates, $[\\![\alpha]\\!]\sim\hat{\alpha}$.

Proof By induction on $\alpha$. For skip, we take
$({\mathbf{\Delta}},\delta_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})$ to
be $1$ from Section 2.6. Our semantics of skip is exactly the first point
above, and the second follows from the definition of Pre earlier in this
section. The last point comes from the fact that the only arrows from skip in
${\mathbf{\Omega}}$ are skip
$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip 7.22743pt$skip
for all $A$.

For crash, we define
$({\mathbf{\Delta}},\delta_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})$ to
be $0$, the empty program model. This is not exactly what we want here.
Instead, consider a one-action set $\\{\sigma\\}$ with no $A$-arrows for any
agent $A$, $\mbox{\sc Pre}(\sigma)={\sf\bf False}$. This gives a signature-
based action model whose induced update is equivalent to crash. Our definition
of Pre is that $\mbox{\sc Pre}(\mbox{\em crash})={\sf false}$. And crash is
not the source of any arrows in $\Omega$.

We next consider an action $\sigma_{i}\vec{\psi}$. We take ${\mathbf{\Delta}}$
to be ${\mathbf{\Sigma}}$, the action signature with which we are working in
this lemma. We also take $\delta_{i}$ to be $\sigma_{i}$. And for each $j$ in
the fixed enumeration of $\Sigma$, we take
${\mbox{\boldmath$\psi$\unboldmath}}_{j}=[\\![\psi_{j}]\\!]$. Then the result
follows from the definitions of the semantics of ${\cal L}({\mathbf{\Sigma}})$
and of Pre. The bisimulation relating
$({\mathbf{\Sigma}},\sigma_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})$ and
$({\mathbf{\Omega}},\sigma_{i}\vec{\psi})$ is the relation
$\\{(\sigma_{j},\sigma_{j}\vec{\psi}):1\leq j\leq n\\}$. Here $n$ is the
number of elements in $\Sigma$.

Finally, assume our result for $\alpha$ and $\beta$. Let
$(\Delta,\delta_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})$ and
$(\Delta^{\prime},\delta^{\prime}_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}^{\prime}})$
satisfy our lemma for $\alpha$ and $\beta$. Then by Proposition 2.5,

$[\\![\alpha;\beta]\\!]\quad\sim\quad(\Delta,\delta_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}});(\Delta^{\prime},\delta^{\prime}_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}^{\prime}}).$
(5.2)

This is not quite what we want, since on the right we do not have a signature-
based program model. Let the enumeration of $\Delta$ be
$\delta_{1},\ldots,\delta_{n}$, and let the enumeration of $\Delta^{\prime}$
be $\delta^{\prime}_{1},\ldots,\delta^{\prime}_{m}$. Let

$f\,:\\{1,\ldots,nm\\}\rightarrow\\{1,\ldots,n\\}\times\\{1,\ldots,m\\}$

be a bijection. Let $g$ and $h$ be such that $f=g\times h$. Let
$\Delta^{\prime\prime}=\Delta\times\Delta^{\prime}$, and enumerate this set by
$\delta^{\prime\prime}_{k}=(\delta_{g(k)},\delta^{\prime}_{h(k)})$. For $1\leq
k\leq nm$, let

${\mbox{\boldmath$\chi$\unboldmath}}_{k}\quad=\quad\langle({\mathbf{\Delta}},\delta_{g(k)},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})\rangle\mbox{pre}(\delta^{\prime}_{h(k)}).$

Let $k^{*}$ be such that $f(k^{*})=(i,i^{\prime})$. For our lemma, we consider
$({\mathbf{\Delta}}^{\prime\prime},\delta^{\prime\prime}_{k^{*}},\vec{{\mbox{\boldmath$\chi$\unboldmath}}})$.
There is an obvious bisimulation between this model and the update on the
right of equation (5.2) above. For the second assertion of our lemma,

$\begin{array}[]{lcll}\mbox{pre}(\alpha;\beta)&\quad=&[\\![\langle\alpha\rangle\mbox{\sc
Pre}(\beta)]\\!]\\\ &\quad=&\langle[\\![\alpha]\\!]\rangle[\\![\mbox{\sc
Pre}(\beta)]\\!]\\\
&\quad=&\langle({\mathbf{\Delta}},\delta_{i},{\mbox{\boldmath$\psi$\unboldmath}}_{i})\rangle{\mbox{\boldmath$\psi$\unboldmath}}^{\prime}_{j}&\mbox{(*)}\\\
&\quad=&{\mbox{\boldmath$\chi$\unboldmath}}_{k^{*}}\\\ \end{array}$

In the equivalence marked $(*)$, we used Proposition 2.6.

We turn to the last part. Let $R$ and $S$ be bisimulations showing
$({\mathbf{\Delta}},\delta_{i},\vec{{\mbox{\boldmath$\psi$\unboldmath}}})\sim({\mathbf{\Omega}},\alpha)$
and
$({\mathbf{\Delta}}^{\prime},\delta_{j},\vec{{\mbox{\boldmath$\psi$\unboldmath}}^{\prime}})\sim({\mathbf{\Omega}},\beta)$.
Then the following bisimulation, called $T$, shows that
$({\mathbf{\Delta}}^{\prime\prime},\delta^{\prime\prime}_{k^{*}},\vec{{\mbox{\boldmath$\chi$\unboldmath}}})\sim({\mathbf{\Omega}},\alpha;\beta)$:

$(\delta_{c},\delta^{\prime}_{d})\ T\ \rho;\eta\quad\mbox{iff}\quad\delta_{c}\
R\ \rho\mbox{ and }\delta^{\prime}_{d}\ S\ \eta\ .$

This completes our induction. In the last point of this result, the assertion
that $[\\![\alpha]\\!]\sim\hat{\alpha}$, we use Proposition 2.10 and parts (1)
and (3) of the present result.  $\dashv$

###  5.3 Soundness of the Action Rule

As we have mentioned, the Action Rule is the main rule in the system for
${\cal L}_{1}({\mathbf{\Sigma}})$ that goes beyond the rules of ${\cal
L}_{0}({\mathbf{\Sigma}})$. It is an induction rule which in the setting of
epistemic logic allows us to prove that common knowledge obtains after various
actions. Here again is our statement of the Action Rule:

Let $\alpha$ be a simple action. Let $\psi$ be a sentence, and let ${\cal C}$
be a set of agents. Let there be sentences $\chi_{\beta}$ for all $\beta$ such
that $\alpha\rightarrow_{{\cal C}}^{*}\beta$ (including $\alpha$ itself), and
such that

  1. 1.

$\vdash\chi_{\beta}\rightarrow[\beta]\psi$.

  2. 2.

If $A\in{\cal C}$ and $\beta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}{\gamma}$, then $\vdash(\chi_{\beta}\wedge\mbox{\sc
Pre}(\beta))\rightarrow\Box_{A}\chi_{\gamma}$.

From these assumptions, infer
$\vdash\chi_{\alpha}\rightarrow[\alpha]\Box_{{\cal C}}^{*}\psi$.

Remark  We use $\rightarrow_{{\cal C}}^{*}$ as an abbreviation for the
reflexive and transitive closure of the relation $\bigcup_{A\in C}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}$. Recall from Proposition 5.1 that there are only finitely many
$\beta$ such that $\alpha\rightarrow_{{\cal C}}^{*}\beta$. So even though the
Action Rule might look like it takes infinitely many premises, it really only
takes finitely many.

Remark  It is possible to drop the Composition Axiom in favor of a more
involved version of the Action Rule. The point is we shall later introduce
normal forms for sentences, and using the Composition Axiom will greatly
simplify these normal forms. Moreover, adding the Composition Axiom leads to
shorter proofs. The Action Rule here is geared towards those normal forms. So
if we were to drop the Composition Axiom, we would need a stronger, more
complicated, formulation of the Action Rule, one which involved sequences of
actions. It is not terribly difficult to formulate such a rule, and
completeness can be obtained by an elaboration of the work which we shall do.

###### Lemma 5.3

$s\in[\\![\langle\alpha\rangle\Diamond_{{\cal
C}}^{*}\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$ iff there is a sequence of
states from $S$

$s\ =\ s_{0}\quad\rightarrow_{A_{1}}\quad
s_{1}\quad\rightarrow_{A_{2}}\quad\cdots\quad\rightarrow_{A_{k-1}}\quad
s_{k-1}\quad\rightarrow_{A_{k}}\quad s_{k}$

where $k\geq 0$, and also a sequence of actions of the same length $k$,

$\alpha\ =\
\alpha_{0}\quad\rightarrow_{A_{1}}\quad\alpha_{1}\quad\rightarrow_{A_{2}}\quad\cdots\quad\rightarrow_{A_{k-1}}\quad\alpha_{k-1}\quad\rightarrow_{A_{k}}\quad\alpha_{k}$

such that $A_{i}\in{\cal C}$ and
$s_{i}\in\mbox{pre}(\alpha_{i})_{{\mathbf{S}}}$ for all $0\leq i<k$, and
$s_{k}\in[\\![\langle\alpha_{k}\rangle\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

Remark  The case $k=0$ just says that
$s\in[\\![\langle\alpha\rangle\Diamond_{{\cal
C}}^{*}\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$ is implied by
$s\in[\\![\langle\alpha\rangle\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

Proof The following are equivalent:

  1. 1.

$s\in[\\![\langle\alpha\rangle\Diamond_{{\cal
C}}^{*}\varphi]\\!]_{\scriptstyle{\mathbf{S}}}$.

  2. 2.

$s\in(\langle[\\![\alpha]\\!]\rangle[\\![\Diamond_{{\cal
C}}^{*}\varphi]\\!])_{{\mathbf{S}}}$.

  3. 3.

$s\in(\langle\hat{\alpha}\rangle[\\![\Diamond_{{\cal
C}}^{*}\varphi]\\!])_{{\mathbf{S}}}$.

  4. 4.

$s\in\mbox{pre}(\alpha)_{{\mathbf{S}}}$, and
$(s,\alpha)\in[\\![\Diamond_{{\cal
C}}^{*}\varphi]\\!]_{\scriptstyle{\mathbf{S}}\otimes{\mathbf{\Omega}}}$.

  5. 5.

$s\in\mbox{pre}(\alpha)_{{\mathbf{S}}}$, and for some $k\geq 0$ there is a
sequence in ${\mathbf{S}}\otimes{\mathbf{\Omega}}$,

$(s,\alpha)\ =\ t_{0}\quad\rightarrow_{A_{1}}\quad
t_{1}\quad\rightarrow_{A_{2}}\quad\cdots\quad\rightarrow_{A_{k-1}}\quad
t_{k-1}\quad\rightarrow_{A_{k}}\quad t_{k}$

such that $A_{i}\in{\cal C}$ and
$t_{k}\in[\\![\varphi]\\!]_{\scriptstyle{\mathbf{S}}\otimes{\mathbf{\Omega}}}$.

  6. 6.

There are sequences of $s=s_{0},\ldots,s_{k}$ and
$\alpha_{0},\ldots,\alpha_{k}$ as in the statement of this lemma.

The first equivalence is by the semantics of ${\cal L}({\mathbf{\Sigma}})$.
The equivalence (2)$\Longleftrightarrow$(3) uses the equality
$[\\![\alpha]\\!]=\hat{\alpha}$ which we saw in the concluding statement of
Theorem 5.2 in Section 5.2, and also Proposition 2.6. Equivalence
(3)$\Longleftrightarrow$(4) uses our overall definitions and the structure of
${\mathbf{\Omega}}$ as an action model. (4)$\Longleftrightarrow$(5) is just
the semantics of $\Diamond_{{\cal C}}^{*}$. Finally, the equivalence
(5)$\Longleftrightarrow$ (6) again uses the conclusion of Theorem 5.2. That
is, for all $i$, $(s_{i},\alpha)\in{\mathbf{S}}\otimes{\mathbf{\Omega}}$ iff
$s_{i}\in\mbox{pre}(\alpha_{i})_{{\mathbf{S}}}$.  $\dashv$

###### Proposition 5.4

The Action Rule is sound.

Proof Assume that $s\in[\\![\chi_{\alpha}]\\!]_{\scriptstyle{\mathbf{S}}}$ but
also $s\in[\\![\langle\alpha\rangle\Diamond_{{\cal
C}}^{*}\neg\psi]\\!]_{\scriptstyle{\mathbf{S}}}$. According to Lemma 5.3,
there is a labeled sequence of states from $S$

$s\ =\ s_{0}\quad\rightarrow_{A_{1}}\quad
s_{1}\quad\rightarrow_{A_{2}}\quad\cdots\quad\rightarrow_{A_{k-1}}\quad
s_{k-1}\quad\rightarrow_{A_{k}}\quad s_{k}$

where $k\geq 0$ and each $A_{i}\in{\cal C}$, and also a sequence of actions of
length $k$, with the same labels,

$\alpha\ =\
\alpha_{0}\quad\rightarrow_{A_{1}}\quad\alpha_{1}\quad\rightarrow_{A_{2}}\quad\cdots\quad\rightarrow_{A_{k-1}}\quad\alpha_{k-1}\quad\rightarrow_{A_{k}}\quad\alpha_{k}$

such that $s_{i}\in\mbox{pre}(\alpha_{i})_{{\mathbf{S}}}$ for all $0\leq i<k$,
and
$s_{k}\in[\\![\langle\alpha_{k}\rangle\neg\psi]\\!]_{\scriptstyle{\mathbf{S}}}$.
If $k=0$, we would have
$s\in[\\![\langle\alpha\rangle\neg\psi]\\!]_{\scriptstyle{\mathbf{S}}}$. But
one of the assumptions in the statement of the Action Rule is that
$\vdash\chi_{\alpha}\rightarrow[\alpha]\psi$. So we would have
$s\in[\\![[\alpha]\psi]\\!]_{\scriptstyle{\mathbf{S}}}$. This would be a
contradiction.

Now we argue the case $k>0$. We show by induction on $1\leq i\leq k$ that
$s_{i}\in[\\![\chi_{\alpha_{i}}]\\!]_{\scriptstyle{\mathbf{S}}}$. The case
$i=0$ is the opening assumptions of this proof. Assume that
$s_{i}\in[\\![\chi_{\alpha_{i}}]\\!]_{\scriptstyle{\mathbf{S}}}$. By
hypothesis, $s_{i}\in\mbox{pre}(\alpha_{i})_{{\mathbf{S}}}$. In view of the
second assumption in the Action Rule,
$s_{i}\in[\\![\Box_{A_{i+1}}\chi_{\alpha_{i+1}}]\\!]_{\scriptstyle{\mathbf{S}}}$.
Hence $s_{i+1}\in[\\![\chi_{\alpha_{i+1}}]\\!]_{\scriptstyle{\mathbf{S}}}$.
This completes our induction.

In particular,
$s_{k}\in[\\![\chi_{\alpha_{k}}]\\!]_{\scriptstyle{\mathbf{S}}}$. Using again
the first assumption in the Action Rule, we have
$s_{k}\in[\\![[\alpha_{k}]\psi]\\!]_{\scriptstyle{\mathbf{S}}}$. This is a
contradiction.  $\dashv$

###  5.4 Syntactic Facts

At this point, we have presented the semantic facts which we need concerning
${\cal L}_{1}({\mathbf{\Sigma}})$. These include the soundness of the logical
system for validity. To prove completeness, we also need some syntactic facts.
We could have presented this section earlier, but since it leans on the Action
Rule, we have delayed it until establishing the soundness of that rule had
been established.

In this section, $\alpha$, $\beta$, etc. denote simple actions in ${\cal
L}_{1}({\mathbf{\Sigma}})$.

#### A stronger form of the Action-Knowledge Axiom

At this point, we establish a stronger form of the Action-Knowledge Axiom. In
Figure 3 in Section 4, this axiom was stated only for basic actions. The
strengthenings here is to simple actions, that is, to compositions of basic
actions, skip, and crash.

###### Lemma 5.5

The Action-Knowledge Axiom is provable for all simple actions $\alpha$:

$\vdash[\alpha]\Box_{A}\varphi\leftrightarrow(\mbox{\sc
Pre}(\alpha)\rightarrow\bigwedge\\{\Box_{A}[\beta]\varphi:\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta\mbox{ in ${\mathbf{\Omega}}$}\\})$ (5.3)

Proof By induction on $\alpha$. If $\alpha$ is skip, $\mbox{\sc
Pre}(\alpha)={\sf true}$, the only $\beta$ with $\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta$ is skip, and equivalence (5.3) reads:

$\vdash[\mbox{\em skip}]\Box_{A}\varphi\leftrightarrow({\sf
true}\rightarrow\Box_{A}[\mbox{\em skip}]\varphi)$

And this is an easy consequence of propositional reasoning, the Skip Axiom,
and $\Box_{A}$-necessitation. If $\alpha$ is crash, $\mbox{\sc
Pre}(\alpha)={\sf false}$, and there are no $\beta$ such that $\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta$. Equivalence (5.3) then reads:

$\vdash[\mbox{\em crash}]\Box_{A}\varphi\leftrightarrow({\sf
false}\rightarrow{\sf true}).$

By the Crash Axiom and modal reasoning, $\vdash[\mbox{\em
crash}]\Box_{A}\varphi$; and so the assertion just above holds.

If $\alpha$ is of the form $\sigma_{i}\vec{\psi}$, then we simply have the
Action-Knowledge Axiom in the form we know it.

So assume our lemma for $\alpha^{\prime}$ and $\alpha$; we prove it for
$\alpha^{\prime};\alpha$. We show that

$\vdash[\alpha^{\prime};\alpha]\Box_{A}\varphi\leftrightarrow(\mbox{\sc
Pre}(\alpha^{\prime};\alpha)\rightarrow\bigwedge\\{\Box_{A}[\beta^{\prime};\beta]\varphi:\alpha^{\prime};\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime};\beta\mbox{ in ${\mathbf{\Omega}}$ }\\})$ (5.4)

We start with the equivalence in (5.3), use $[\alpha^{\prime}]$-necessitation
and normality, and get

$\vdash[\alpha^{\prime}][\alpha]\Box_{A}\varphi\leftrightarrow([\alpha^{\prime}]\mbox{\sc
Pre}(\alpha)\rightarrow\bigwedge\\{[\alpha^{\prime}]\Box_{A}[\beta]\varphi:\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta\mbox{ in ${\mathbf{\Omega}}$}\\})$ (5.5)

By the induction hypothesis on $\alpha^{\prime}$ and several uses of the
Composition Axiom, we have that for all $\beta$,

$\vdash[\alpha^{\prime}]\Box_{A}[\beta]\varphi\leftrightarrow(\mbox{\sc
Pre}(\alpha^{\prime})\rightarrow\bigwedge\\{\Box_{A}[\beta^{\prime};\beta]\varphi:\alpha^{\prime}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime}\mbox{ in ${\mathbf{\Omega}}$}\\}).$

The Composition Axiom and (5.5) lead to the provable equivalence of
$[\alpha^{\prime};\alpha]\Box_{A}\varphi$ and

$[\alpha^{\prime}]\mbox{\sc Pre}(\alpha)\rightarrow(\mbox{\sc
Pre}(\alpha^{\prime})\rightarrow\bigwedge\\{\Box_{A}[\beta^{\prime};\beta]\varphi:\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta\mbox{ and }\alpha^{\prime}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime}\mbox{ in ${\mathbf{\Omega}}$ }\\}).$

But $\vdash\mbox{\sc Pre}(\alpha^{\prime};\alpha)\leftrightarrow\mbox{\sc
Pre}(\alpha^{\prime})\wedge[\alpha^{\prime}]\mbox{\sc Pre}(\alpha)$. In
addition, we have a general fact $\alpha^{\prime};\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime};\beta$ iff $\alpha^{\prime}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime}$ and $\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta$. Using these observations and some propositional reasoning,
we get (5.4), as desired.  $\dashv$

Remark  There are no sound versions of the Action-Knowledge Axiom for actions
containing $\sqcup$. For example let ${\cal A}$ be a singleton, hence omitted
from the notation. Consider ${\mathbf{\Sigma}}=\\{\sigma,\tau\\}$ this as an
action signature with the enumeration $\sigma$, $\tau$, and with (say) the
arrows $\sigma\rightarrow\tau$ and $\tau\rightarrow\sigma$. Note that by
Atomic Permanence $[\sigma\ pq]r$ is equivalent to $p\rightarrow r$, $[\tau\
pq]r$ is equivalent to $q\rightarrow r$, by Action-Knowledge and Atomic
Permanence $[\sigma\ pq]\Box r$ is equivalent to
$p\rightarrow\Box(q\rightarrow r)$, and $[\tau\ pq]\Box r$ is equivalent to
$q\rightarrow\Box(p\rightarrow r)$, Consider also the sentence $[(\sigma\
pq)\sqcup(\tau\ pq)]\Box r$. By the Choice Axiom, it is equivalent to

$(p\rightarrow\Box(q\rightarrow r))\wedge(q\rightarrow\Box(p\rightarrow r)).$
(5.6)

Now we did not define $\mbox{\sc Pre}((\sigma\ pq)\sqcup(\tau\ pq))$, but the
most reasonable choice is $p\vee q$. And we did not define the accessibility
structure of actions containing $\sqcup$, but in this case the most likely
choice is to have $(\sigma\ pq)\sqcup(\tau\ pq)$ relate to itself and nothing
else. But then when we write out the right-hand side of the equivalence (5.3),
we get

$(p\vee q)\rightarrow(\Box(p\rightarrow r)\wedge\Box(q\rightarrow r)).$

Clearly this is not equivalent to (5.6). Even if one were to change $\mbox{\sc
Pre}((\sigma\ pq)\sqcup(\tau\ pq))$ to, say ${\sf true}$, or to $p\wedge q$,
we still would not have an equivalence: (5.6) is stronger.

#### A stronger form of the Partial Functionality Axiom

We shall also need the following result, a version of the Partial
Functionality Axiom:

###### Lemma 5.6

$\vdash\langle\alpha\rangle\varphi\leftrightarrow\mbox{\sc
Pre}(\alpha)\wedge[\alpha]\varphi$.

Proof This is an induction, much like the proof of Lemma 5.3 above.  $\dashv$

#### Syntactic bisimulation

Our next set of results pertains to a syntactic notion of action equivalence,
one with a bisimulation-like flavor.

Definition  A syntactic bisimulation is a relation $R$ on the set $\Omega$ of
simple actions of ${\cal L}({\mathbf{\Sigma}})$ with the following property:
if $\alpha\ R\ \beta$, then

  1. 1.

$\vdash\mbox{\sc Pre}(\alpha)\leftrightarrow\mbox{\sc Pre}(\beta)$.

  2. 2.

For all $\alpha^{\prime}$ and $A$ such that $\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\alpha^{\prime}$, there is some $\beta^{\prime}$ such that
$\beta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime}$ and $\alpha^{\prime}\ R\ \beta^{\prime}$.

  3. 3.

For all $\beta^{\prime}$ and $A$ such that $\beta\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime}$, there is some $\alpha^{\prime}$ such that
$\alpha\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\alpha^{\prime}$ and $\alpha^{\prime}\ R\ \beta^{\prime}$.

We say that $\alpha$ and $\beta$ are provably equivalent if there is some
syntactic bisimulation relating them. We write $\alpha\equiv\beta$ in this
case.

For sentences, we write $\varphi\equiv\psi$ and say that $\varphi$ and $\psi$
are equivalent if $\vdash\varphi\leftrightarrow\psi$.

###### Lemma 5.7

$\vdash\langle\alpha\rangle{\sf true}\leftrightarrow\mbox{\sc Pre}(\alpha)$.

Proof By induction on $\alpha$. For $\alpha=\mbox{\em skip}$ and
$\alpha=\mbox{\em crash}$, we use the Skip Axiom and the Crash Axiom,
respectively. Here is the argument for $\alpha$ of the form
$\sigma_{i}\vec{\psi}$. First, by necessitation we have
$\vdash[\sigma_{i}\vec{\psi}]{\sf true}$. And by this and Partial
Functionality, $\vdash[\sigma_{i}\vec{\psi}]\neg{\sf
true}\leftrightarrow\neg\psi_{i}$. So
$\vdash\neg[\sigma_{i}\vec{\psi}]\neg{\sf true}\leftrightarrow\psi_{i}$. That
is, $\vdash\langle\sigma_{i}\vec{\psi}\rangle{\sf
true}\leftrightarrow\psi_{i}$.

Finally, assume the result for $\beta$. Then by normality and necessitation,
$\vdash\langle\alpha\rangle\langle\beta\rangle{\sf
true}\leftrightarrow\langle\alpha\rangle\mbox{\sc Pre}(\beta)$. So
$\vdash\langle\alpha\rangle\langle\beta\rangle{\sf
true}\leftrightarrow\mbox{\sc Pre}(\alpha;\beta)$. We conclude by showing as a
general fact that
$\vdash\langle\alpha\rangle\langle\beta\rangle\varphi\leftrightarrow\langle\alpha;\beta\rangle\varphi$.
For this, the Composition Axiom tells us that
$\vdash[\alpha][\beta]\neg\varphi\leftrightarrow[\alpha;\beta]\neg\varphi$. So
$\vdash\neg[\alpha]\neg\neg[\beta]\neg\varphi\leftrightarrow\neg[\alpha;\beta]\neg\varphi$.
Thus
$\vdash\langle\alpha\rangle\langle\beta\rangle\varphi\leftrightarrow\langle\alpha;\beta\rangle\varphi$,
as desired.  $\dashv$

###### Lemma 5.8

The following monoid-type laws hold:

  1. 1.

$\vdash\mbox{\sc Pre}(\alpha;\mbox{\em skip})\leftrightarrow\mbox{\sc
Pre}(\alpha)\leftrightarrow\mbox{\sc Pre}(\mbox{\em skip};\alpha)$.

  2. 2.

$\vdash\mbox{\sc Pre}(\alpha;(\beta;\gamma))\leftrightarrow\mbox{\sc
Pre}((\alpha;\beta);\gamma)$.

Proof We use the definitions to calculate

$\begin{array}[]{lcl}\mbox{\sc Pre}(\alpha;\mbox{\em
skip})&\quad=&\langle\alpha\rangle{\sf true}\\\ \mbox{\sc Pre}(\mbox{\em
skip};\alpha)&\quad=&\langle\mbox{\em skip}\rangle\mbox{\sc
Pre}(\alpha).\end{array}$

We obtain a formal proof using Lemma 5.7 and the Skip Axiom. Turning to the
second law,

$\begin{array}[]{lcl}\mbox{\sc
Pre}(\alpha;(\beta;\gamma))&\quad=&\langle\alpha\rangle\mbox{\sc
Pre}(\beta;\gamma)\\\ &\quad=&\langle\alpha\rangle\langle\beta\rangle\mbox{\sc
Pre}(\gamma)\\\ &\quad\equiv&\langle\alpha;\beta\rangle\mbox{\sc
Pre}(\gamma)\\\ &\quad=&\mbox{\sc Pre}((\alpha;\beta);\gamma).\\\ \end{array}$

The equivalence above which mentions $\equiv$ uses the Composition Axiom.
$\dashv$

###### Lemma 5.9

Concerning the syntactic equivalence $\equiv$ on $\Omega$:

  1. 1.

The relation $\equiv$ is an equivalence relation.

  2. 2.

If $\varphi_{1}\equiv\psi_{1}$, $\ldots$, $\varphi_{n}\equiv\psi_{n}$, then
$\sigma_{i}\vec{\varphi}\equiv\sigma_{i}\vec{\psi}$.

  3. 3.

$\alpha;skip\equiv\alpha\equiv skip;\alpha$.

  4. 4.

$\alpha;(\beta;\gamma)\equiv(\alpha;\beta);\gamma$.

  5. 5.

If $\alpha\equiv\alpha^{\prime}$ and $\beta\equiv\beta^{\prime}$, then
$\alpha;\beta\equiv\alpha^{\prime};\beta^{\prime}$.

Proof The first part is routine. Part (2) uses the bisimulation consisting of
all pairs $(\sigma_{j}\vec{\varphi},\sigma_{j}\vec{\psi})$ such that $1\leq
j\leq n$ and for all $i$, $\varphi_{i}\equiv\psi_{i}$. Lemma 5.8 is used in
parts (3) and (4). The rest of argument for part (3) is easy and we omit it.
For part (4), we take $R$ to be the set of pairs

$(\alpha^{\prime};(\beta^{\prime};\gamma^{\prime}),(\alpha^{\prime};\beta^{\prime});\gamma^{\prime})$

such that for some sequence $w$ of $\rightarrow_{A}$ with $A\in{\cal A}^{*}$,
$\alpha^{\prime}$ is reachable from $\alpha$ via $w$, and similarly for
$\beta^{\prime}$ and $\gamma^{\prime}$ (via the same $w$). Part (5) is
similar.  $\dashv$

###### Lemma 5.10

For all $A\in{\cal C}$ and all $\beta$ such that $\alpha\rightarrow_{A}\beta$,

  1. 1.

$\vdash[\alpha]\Box_{{\cal C}}^{*}\psi\rightarrow[\alpha]\psi$.

  2. 2.

$\vdash[\alpha]\Box_{{\cal C}}^{*}\psi\wedge\mbox{\sc
Pre}(\alpha)\rightarrow\Box_{A}[\beta]\Box_{{\cal C}}^{*}\psi$.

Proof Part (1) follows from the Epistemic Mix Axiom and modal reasoning. For
part (2), we start with a consequence of the Epistemic Mix Axiom:
$\vdash\Box_{{\cal C}}^{*}\psi\rightarrow\Box_{A}\Box_{{\cal C}}^{*}\psi$.
Then by modal reasoning, $\vdash[\alpha]\Box_{{\cal
C}}^{*}\psi\rightarrow[\alpha]\Box_{A}\Box_{{\cal C}}^{*}\psi$. By the Action-
Knowledge Axiom in the generalized form of Lemma 5.3, we have
$\vdash[\alpha]\Box_{{\cal C}}^{*}\psi\wedge\mbox{\sc
Pre}(\alpha)\rightarrow\Box_{A}[\beta]\Box_{{\cal C}}^{*}\psi$.  $\dashv$

We present next our main result on syntactic equivalence of actions. It is a
syntactic version of Proposition 2.6.

###### Lemma 5.11

Let $\alpha$ and $\beta$ be simple actions. If $\alpha\equiv\beta$, then for
all $\varphi$, $\vdash[\alpha]\varphi\leftrightarrow[\beta]\varphi$.

Proof By induction on $\varphi$. Fix a syntactic bisimulation $R$ relating
$\alpha$ and $\beta$. For $\varphi={\sf true}$ or an atomic sentence $p_{i}$,
our result is easy. The induction steps for $\neg$ and $\wedge$ are trivial.
The step for $\Box_{A}$ is not hard, and so we omit it.

We next check the result for sentences $[\gamma]\varphi$. We need to see that

$\vdash[\alpha][\gamma]\varphi\leftrightarrow[\alpha^{\prime}][\gamma]\varphi.$

For this, it is sufficient by the Composition Axiom to show that
$\vdash[\alpha;\gamma]\varphi\leftrightarrow[\alpha^{\prime};\gamma]\varphi$.
By Lemma 5.9, parts (1) and (5), $\alpha;\gamma\equiv\alpha^{\prime};\gamma$.
So we are done by the induction hypothesis.

This leaves the step for sentences of the form $\Box_{{\cal B}}^{*}\varphi$,
assuming the result for $\varphi$. We use the Action Rule to show that
$\vdash[\alpha]\Box_{{\cal C}}^{*}\varphi\rightarrow[\beta]\Box_{{\cal
C}}^{*}\varphi$. We need a functional witness to $R$; that is, a map
$\beta^{\prime}\mapsto\alpha^{\prime}$ for all $\beta^{\prime}$ such that
$\beta\,\lower
1.0pt\hbox{$\\!\longrightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{\\!\\!{\cal
A}^{*}}$}\hskip 7.22743pt$}\beta^{\prime}$, such that
$\alpha^{\prime}R\beta^{\prime}$ for all these actions. Further, let
$\chi_{\beta^{\prime}}$ be $[\alpha^{\prime}]\Box_{{\cal C}}^{*}\varphi$. We
need to show that for all $A\in C$ and all $\beta^{\prime}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime\prime}$,

a.

$\vdash[\alpha^{\prime}]\Box_{{\cal
C}}^{*}\varphi\rightarrow[\beta^{\prime}]\varphi$; and

b.

If $\beta^{\prime}\,\lower
1.0pt\hbox{$\rightarrow\raisebox{4.30554pt}{$\scriptscriptstyle{A}$}\hskip
7.22743pt$}\beta^{\prime\prime}$, then $\vdash[\alpha^{\prime}]\Box_{{\cal
C}}^{*}\varphi\wedge\mbox{\sc
Pre}(\beta^{\prime})\rightarrow\Box_{A}[\alpha^{\prime\prime}]\Box_{{\cal
C}}^{*}\varphi$.

For (a), we know from Lemma 5.10, that $\vdash[\alpha^{\prime}]\Box_{{\cal
C}}^{*}\varphi\rightarrow[\alpha^{\prime}]\varphi$. By induction hypothesis on
$\varphi$,
$\vdash[\alpha^{\prime}]\varphi\leftrightarrow[\beta^{\prime}]\varphi$. And
this implies (a). For (b), Lemma 5.10 tells us that under the assumptions,

$\vdash[\alpha^{\prime}]\Box_{{\cal C}}^{*}\varphi\wedge\mbox{\sc
Pre}(\alpha^{\prime})\rightarrow\Box_{A}[\alpha^{\prime\prime}]\Box_{{\cal
C}}^{*}\varphi.$

The fact that $R$ is a syntactic bisimulation tells us that $\vdash\mbox{\sc
Pre}(\alpha^{\prime})\leftrightarrow\mbox{\sc Pre}(\beta^{\prime})$. This
implies (b).

This completes the induction on $\varphi$.  $\dashv$

Lemma 5.11 will be used in several places to come.

##  6 Completeness theorems