ENS Rennes, France<EMAIL_ADDRESS>University of Naples
“Federico II”, Naples, Italy<EMAIL_ADDRESS>This project has
received funding from the European Union’s Horizon 2020 research and
innovation programme under the Marie Sklodowska-Curie grant agreement No
709188. University of Naples “Federico II”, Naples, Italy<EMAIL_ADDRESS>University of Naples “Federico II”, Naples, Italy<EMAIL_ADDRESS>Aurèle
Barrière, Bastien Maubert, Aniello Murano and Sasha Rubin John Q. Open and
Joan R. Access 2 42nd Conference on Very Important Topics (CVIT 2016) CVIT
2016 CVIT 2016 December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Changing Observations in Epistemic Temporal Logic

Aurèle Barrière  ,  Bastien Maubert  ,  Aniello Murano  and  Sasha Rubin

###### Abstract.

We study dynamic changes of agents’ observational power in logics of knowledge
and time. We consider $\textnormal{{CTL}}^{*}\textnormal{K}$, the extension of
$\textnormal{{CTL}}^{*}$ with knowledge operators, and enrich it with a new
operator that models a change in an agent’s way of observing the system. We
extend the classic semantics of knowledge for perfect-recall agents to account
for changes of observation, and we show that this new operator strictly
increases the expressivity of $\textnormal{{CTL}}^{*}\textnormal{K}$. We
reduce the model-checking problem for our logic to that for
$\textnormal{{CTL}}^{*}\textnormal{K}$, which is known to be decidable. This
provides a solution to the model-checking problem for our logic, but its
complexity is not optimal. Indeed we provide a direct decision procedure with
better complexity.

###### Key words and phrases:

Epistemic logic, Temporal logic, Model checking

###### 1991 Mathematics Subject Classification:

Logic and Verification

##  1\. Introduction

In multi-agent systems, agents usually have only partial information about the
state of the system [23]. This has led to the development of epistemic logics,
often combined with temporal logics, for describing and reasoning about how
distributed systems and agents’ knowledge evolve over time. Such formalisms
have been applied to the modelling and analysis of, e.g., distributed
protocols [18, 12], information flow and cryptographic protocols [26, 13] and
knowledge-based programs [27].

In these frameworks, an agent’s view of a particular state of the system is
given by an observation of that state. In all the cited settings, an agent’s
observation of a given state does not change over time. In other words, these
frameworks have no primitive for reasoning about agents whose observation
power can change. Because this phenomenon occurs in real scenarios, for
instance when a user of a system is granted access to previously hidden data,
we propose here to tackle this problem. Precisely, we extend classic epistemic
temporal logics with a new unary operator, $\Delta^{o}$, that represents
changes of observation power, and is read “the agent changes her observation
power to $o$”. For instance, the formula
$\Delta^{o_{1}}\mathit{A}\mathit{F}(\Delta^{o_{2}}(\mathit{K}p\vee\mathit{K}\neg
p))$ expresses that “For an agent with initial observation power $o_{1}$, in
all possible futures there exists a point where, if the agent updates her
observation power to $o_{2}$, she learns whether or not the proposition $p$
holds”. If in this example $o_{1}$ and $o_{2}$ represent different “security
levels” and $p$ is sensitive information, then the formula expresses a
possible avenue for attack. The logics and model-checking procedures that we
present in this paper allow the expression and evaluation of such properties.
Another motivation for studying such logics comes from the recently introduced
Strategy Logic with Imperfect Information [6], an extension of Strategy Logic
[19] in which agents can dynamically change observation power when changing
strategies.

There is a rich history of epistemic logic in AI, including the static and
temporal settings [12], the dynamic setting [28] as well as the strategic
setting [23]. The most common logics of knowledge and time are CTLK, LTLK and
$\textnormal{{CTL}}^{*}\textnormal{K}$, which extend the classic temporal
logics CTL, LTL and $\textnormal{{CTL}}^{*}$ with epistemic operators. These
logics have been studied for two main recall abilities: no memory or perfect
recall. For memoryless agents, adapting the semantics of these logics to
include the observation-change operator is straightforward. Model-checking
algorithms also can be easily adapted by keeping updated in the procedure each
agent’s current observation, and this information is of linear size. The
resulting logics thus have a Pspace -complete model-checking problem, as LTLK,
CTLK and $\textnormal{{CTL}}^{*}\textnormal{K}$ do [21, 16].

The case of agents with perfect recall, which we study in this work, is more
delicate. The model-checking problem for LTLK and
$\textnormal{{CTL}}^{*}\textnormal{K}$ is nonelementary decidable [25, 8, 1],
with $k$-Exptime upper-bound for formulas with at most $k$ nested knowledge
operators. The same upper-bounds are known for CTLK [10]. In this work we show
that, as for the memoryless semantics, the introduction of observation changes
in epistemic temporal logics with perfect recall does not increase the
complexity of the model-checking problem.

We extend $\textnormal{{CTL}}^{*}\textnormal{K}$ (which subsumes CTLK and
LTLK) with observation-change operators $\Delta^{o}$, starting with the
single-agent case, and we solve its model-checking problem. To do so we define
an alternative semantics which, unlike the natural one, is based on a bounded
amount of information. Once the two semantics proven to be equivalent,
designing a model-checking algorithm is almost straightforward. We then extend
the logic to the multi-agent case, introducing operators $\Delta^{o}_{a}$ for
each agent $a$, and we extend our approach to solve its model-checking
problem. Next, we study the expressivity of our logic, showing that the
observation-change operator increases expressivity. We finally provide a
reduction to $\textnormal{{CTL}}^{*}\textnormal{K}$ which shows how to remove
observation-change operators, at the cost of a blow-up in the size of the
model. Our direct model-checking procedure is shown to have a better
complexity than going through this reduction and using known model-checking
algorithms for $\textnormal{{CTL}}^{*}\textnormal{K}$.

##  2\. $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$

In this section we define the logic
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$, which extends
$\textnormal{{CTL}}^{*}\textnormal{K}$. We first study the case where there is
only one agent (and thus only one knowledge operator). We will extend to the
multi-agent setting in Section 5.

###  2.1. Notation

A _finite_ (resp. _infinite_) _word_ over some alphabet $\Sigma$ is an element
of $\Sigma^{*}$ (resp. $\Sigma^{\omega}$). The _length_ of a finite word
$w=w_{0}\ldots w_{n}$ is $|w|=n+1$, and we let $\mbox{last}(w)=w_{n}$. Given a
finite (resp. infinite) word $w$ and $0\leq i\leq|w|$ (resp.
$i\in\mathbb{N}$), we let $w_{i}$ be the letter at position $i$ in $w$,
$w_{\leq i}$ is the prefix of $w$ that ends at position $i$, and $w_{\geq i}$
is the suffix that starts at position $i$. We write $w\preccurlyeq w^{\prime}$
if $w$ is a prefix of $w^{\prime}$.

###  2.2. Syntax

We fix a countably infinite set of atomic propositions, $\mathcal{AP}$. We
also let $\mathcal{O}$ be a finite set of observations, that represent
possible observational powers of the agent. Note that in this work,
“observation” does not refer to a punctual observation of a system’s state,
but rather a way of observing the system, or “observational power” of an
agent.

As for state and path formulas in $\textnormal{{CTL}}^{*}$, we distinguish
between history formulas and path formulas. We say history formulas instead of
state formulas because, considering agents with _perfect recall_ of the past,
the truth of epistemic formulas depends not only on the current state, but
also on the history before reaching this state.

######  Definition 2.1 (Syntax).

The sets of history formulas $\varphi$ and path formulas $\psi$ are defined by
the following grammar:

$\begin{array}[]{ccl}\varphi&::=&p\leavevmode\nobreak\ |\leavevmode\nobreak\
\neg\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\varphi\wedge\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathit{A}\psi\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathit{K}\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\Delta^{o}\varphi\\\ \psi&::=&\varphi\leavevmode\nobreak\
|\leavevmode\nobreak\ \neg\psi\leavevmode\nobreak\ |\leavevmode\nobreak\
\psi\wedge\psi\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathit{X}\psi\leavevmode\nobreak\ |\leavevmode\nobreak\
\psi\mathit{U}\psi,\end{array}$

where $p\in\mathcal{AP}$ and $o\in\mathcal{O}$.

We call $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ formulas all history
formulas so defined. Operators $\mathit{X}$ and $\mathit{U}$ are the classic
next and until operators of temporal logics, and $\mathit{A}$ is the universal
path quantifier from branching-time temporal logics. $\mathit{K}$ is the
knowledge operator from epistemic logics, and $\mathit{K}\varphi$ reads as
“the agent knows that $\varphi$ is true”. Our new _observation change_
operator, $\Delta^{o}$, reads as “the agent now observes the system with
observation $o$”.

As usual, we define $\top=p\vee\neg p$,
$\varphi\vee\varphi^{\prime}=\neg(\varphi\wedge\neg\varphi)$,
$\varphi\to\varphi^{\prime}=\neg\varphi\vee\varphi^{\prime}$, as well as the
temporal operators _finally_ ($\mathit{F}$) and _always_ ($\mathit{G}$):
$\mathit{F}\varphi=\top\mathit{U}\varphi$, and
$\mathit{G}\varphi=\neg\mathit{F}\neg\varphi$.

###  2.3. Semantics

The models of $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ are Kripke
structures equipped with one observation relation $\sim_{o}$ on states for
each observation $o$.

######  Definition 2.2 (Models).

A _Kripke structure with observations_ is given as a structure
$M=(\textnormal{AP},S,T,V,\\{\sim_{o}\\}_{o\in\mathcal{O}},{{s}^{\iota}},o^{\iota})$,
where

  * •

$\textnormal{AP}\subset\mathcal{AP}$ is a finite subset of atomic
propositions,

  * •

$S$ is a set of states,

  * •

$T\subseteq S\times S$ is a left-total111i.e., for every $s\in S$ there exists
$s^{\prime}\in S$ such that $sTs^{\prime}$. This cosmetic restriction is made
to avoid having to deal with finite runs ending in deadlocks.  transition
relation,

  * •

$V:S\rightarrow 2^{\textnormal{AP}}$ is a valuation function,

  * •

$\sim_{o}\subseteq S\times S$ is an equivalence relation, for each
$o\in\mathcal{O}$,

  * •

${{s}^{\iota}}\subseteq S$ is an initial state, and

  * •

$o^{\iota}\in\mathcal{O}$ is the initial observation.

A path is an infinite sequence of states $\pi=s_{0}s_{1}\dots$ such that for
all $i\geq 0$, $s_{i}Ts_{i+1}$, and a history $h$ is a finite prefix of a
path. For $I\subseteq S$, we write $T(I)=\\{s^{\prime}\mid\exists s\in I\mbox{
s.t. }sTs^{\prime}\\}$ for the set of successors of states in $I$. Finally,
for $o\in\mathcal{O}$ and $s\in S$, we let $[s]_{o}=\\{s^{\prime}\mid
s\sim_{o}s^{\prime}\\}$ be the equivalence class of $s$ for relation
$\sim_{o}$.

######  Remark 2.3.

We model agents’ information via indistinguishability relations $\sim_{o}$,
where $s\sim_{o}s^{\prime}$ means that $s$ and $s^{\prime}$ are
indistinguishable for an agent who has observation power $o$. Other approaches
exist. One is via _observation functions_ (see, e.g., [25]), that map states
to atomic observations, and where two states are indistinguishable for an
observation function if they have the same image. Another consists in seeing
states as tuples of _local states_ , one for each agent, two global states
being indistinguishable for an agent if her local state is the same in both
(see, e.g., [16]). All these formalisms are essentially equivalent with
respect to epistemic temporal logics [20]. In these alternative formalisms,
observation change would correspond to, respectively, changing observation
function, and changing local states in global states. Note that the formalism
via local states, because indistinguishability is hard-coded in states of the
system, is less adapted to the modelling of observation change.

Observation records. To define which histories the agent cannot distinguish,
we need to keep track of how she observed the system at each point in time. To
do so, we record each observation change as a pair $(o,n)$, where $o$ is the
new observation and $n$ is the time when this change occurs.

######  Definition 2.4.

An _observation record_ is a finite word over $\mathcal{O}\times\mathbb{N}$.

Note that observation records are meant to represent changes of observational
ability, and thus they do not contain the initial observation (which is given
in the model). We write $\emptyset$ for the empty observation record.

######  Example 2.5.

Consider a model $M$ with initial observation $o^{\iota}$, a history
$h=s_{0}\ldots s_{4}$ and an observation record
$r=(o_{1},0)\cdot(o_{2},3)\cdot(o_{3},3)$. The agent first observes state
$s_{0}$ with observation $o^{\iota}$. The observation record shows that at
time 0, thus before the first transition, the agent changed for observation
$o_{1}$. She then observed state $s_{0}$ again, but this time with observation
$o_{1}$. Then the system goes through states $s_{1}$ and $s_{2}$ and reaches
$s_{3}$, all of which she observes with observation $o_{1}$. At time 3, the
agent changes to observation $o_{2}$, and thus observes state $s_{3}$ again,
but this time with observation $o_{2}$, and finally she switches to
observation $o_{3}$ and thus observes $s_{3}$ once more, with observation
$o_{3}$. Finally, the system goes to state $s_{4}$, which the agent observes
with observation $o_{3}$.

We write $r\cdot(o,n)$ for the observation record obtained by appending
$(o,n)$ to the observation record $r$, and $r[n]$ for the record consisting of
all pairs $(o,m)$ in $r$ such that $m=n$. We say that an observation record
$r$ _stops at $n$_ if $r[m]$ is empty for all $m>n$, and $r$ _stops at history
$h$_ if it stops at $|h|-1$. Unless otherwise specified, when we consider an
observation record $r$ together with a history $h$, it is understood that $r$
stops at $h$.

Observations at time $n$. We let ${ol}(r,n)$ be the list of observations used
by the agent at time $n$. It consists of the observation that the agent has
when the $n$-th transition is taken, plus those of observation changes that
occur before the next transition. It is defined by induction on $n$:

$\displaystyle{ol}(r,0)$ $\displaystyle=o^{\iota}\cdot o_{1}\cdot\ldots\cdot
o_{k},$ $\displaystyle\mbox{if }r[0]=(o_{1},0)\cdot\ldots\cdot(o_{k},0),\mbox{
and}$ $\displaystyle{ol}(r,n+1)$ $\displaystyle=\mbox{last}({ol}(r,n))\cdot
o_{1}\cdot\ldots\cdot o_{k},$ $\displaystyle\mbox{if
}r[n+1]=(o_{1},n+1)\cdot\ldots\cdot(o_{k},n+1).$

Observe that ${ol}(r,n)$ is never empty: if no observation change occurs at
time $n$, ${ol}(r,n)$ only contains the last observation taken by the agent.
If $r$ is empty, the latter is the initial observation $o_{\iota}$ defined by
the model.

######  Example 2.6.

Consider record $r=(o_{1},0)\cdot(o_{2},3)\cdot(o_{3},3)$. We have that
${ol}(r,0)=o^{\iota}\cdot o_{1}$, ${ol}(r,1)={ol}(r,2)=o_{1}$,
${ol}(r,3)=o_{1}\cdot o_{2}\cdot o_{3}$, and ${ol}(r,4)=o_{3}$.

Synchronous perfect recall. The usual definition of synchronous perfect recall
states that for an agent with observation $o$, histories $h$ and $h^{\prime}$
are indistinguishable if they have the same length and are point-wise
indistinguishable, i.e., $|h|=|h^{\prime}|$ and for each $i<|h|$,
$h_{i}\sim_{o}h^{\prime}_{i}$.

We adapt this definition to changing observations: two histories are
indistinguishable if, at each point in time, the states are indistinguishable
for all observations used at that time.

######  Definition 2.7 (Dynamic synchronous perfect recall).

Given an observation record $r$, two histories $h$ and $h^{\prime}$ are
equivalent, written $h\approx^{r}h^{\prime}$, if

$|h|=|h^{\prime}|\leavevmode\nobreak\ \textit{and}\leavevmode\nobreak\ \forall
i<|h|,\leavevmode\nobreak\ \forall o\in{ol}(r,i),\leavevmode\nobreak\
h_{i}\sim_{o}h^{\prime}_{i}.$

We now define the natural semantics of
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$.

######  Definition 2.8 (Natural semantics).

Fix a model $M$. A history formula $\varphi$ is evaluated in a history $h$ and
an observation record $r$. A path formula $\psi$ is interpreted on a run
$\pi$, a point in time $n\in\mathbb{N}$ and an observation record. The
semantics is defined by induction on formulas:

$\begin{array}[]{lcl}h,r\models p&\mbox{ if }&p\in
V(\mathit{last}(h))\\\\[1.0pt] h,r\models\neg\varphi&\mbox{ if
}&h,r\not\models\varphi\\\\[1.0pt]
h,r\models\varphi_{1}\wedge\varphi_{2}&\mbox{ if
}&h,r\models\varphi_{1}\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\
h,r\models\varphi_{2}\\\\[1.0pt] h,r\models\mathit{A}\psi&\mbox{ if
}&\forall\pi\mbox{ s.t. }h\preccurlyeq\pi,\;\pi,|h|-1,r\models\psi\\\\[1.0pt]
h,r\models\mathit{K}\varphi&\mbox{ if }&\forall h^{\prime}\mbox{ s.t.
}h^{\prime}\approx^{r}h,\;h^{\prime},r\models\varphi\\\\[1.0pt]
h,r\models\Delta^{o}\varphi&\mbox{ if
}&h,r\cdot(o,|h|-1)\models\varphi\\\\[1.0pt] \pi,n,r\models\varphi&\mbox{ if
}&\pi_{\leq n},r\models\varphi\\\\[1.0pt] \pi,n,r\models\neg\psi&\mbox{ if
}&\pi,n,r\not\models\psi\\\\[1.0pt]
\pi,n,r\models\psi_{1}\wedge\psi_{2}&\mbox{ if }&\pi,n,r\models\psi_{1}\mbox{
and }\pi,n,r\models\psi_{2}\\\\[1.0pt] \pi,n,r\models\mathit{X}\psi&\mbox{ if
}&\pi,(n+1),r\models\psi\\\\[1.0pt]
\pi,n,r\models\psi_{1}\mathit{U}\psi_{2}&\mbox{ if }&\exists m\geq n\mbox{
s.t. }\pi,m,r\models\psi_{2}\mbox{ and}\\\\[1.0pt] &&\forall k\mbox{ s.t.
}n\leq k<m,\;\pi,k,r\models\psi_{1}\end{array}$

We say that a model $M$ with initial state ${{s}^{\iota}}$ _satisfies_ a
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ formula $\varphi$, written
$M\models\varphi$, if ${{s}^{\iota}},\emptyset\models\varphi$.

We first discuss a subtlety of our semantics, which is that an agent can
observe the same state consecutively with several observations.

######  Remark 2.9.

Consider the formula $\Delta^{o^{\prime}}\varphi$ and history $h$. By
definition, $h,r\models\Delta^{o^{\prime}}\varphi$ iff
$h,r\cdot(o^{\prime},|h|-1)\models\varphi$. Note that although the history did
not change (it is still $h$), the observation record is extended by the
observation $o^{\prime}$ at time $|h|-1$, with the following consequence.
Suppose that $ol(r,|h|-1)=o$. After switching to $o^{\prime}$, the agent
considers possible all histories $h^{\prime}$ such that i)
$h\sim_{r}h^{\prime}$ (they were considered possible before the change of
observation) and ii) $last(h)\sim_{o^{\prime}}last(h^{\prime})$ (they are
still considered possible after the change of observation). Informally this
means that by changing observation from $o$ to $o^{\prime}$, the agent’s
information is _further refined_ by $o^{\prime}$, and it is as though the
agent at time $|h|-1$ observed the system with observation $o\cap o^{\prime}$.
At later times, her observation is simply $o^{\prime}$, until another change
of observation occurs.

###  2.4. Examples of observation change

######  Example 2.10.

A logic of accumulative knowledge (and resource bounds) is introduced in [15].
It studies agents that can perform successive _observations_ to improve their
knowledge of the situation, each observation refining their current view of
the world. In their framework, an observation models a yes/no question about
the current situation; if the answer is ‘yes’, the agent can eliminate all
possible worlds for which the answer is ‘no’, and vice versa. Formally, an
observation is a binary partition of the possible states, and the agent learns
in which partition is the current state. Such observations are particular
cases of our models’ indistinguishability relations, and the semantics of an
agent performing an observation $o$ is exactly captured by the semantics of
our operator $\Delta^{o}$. Similarly, performing sequence of observations
$o_{1}\ldots o_{n}$ corresponds to the successive application of operators
$\Delta^{o_{1}}\ldots\Delta^{o_{n}}$. As an example, [15] shows how to model a
medical diagnosis in which the disease is narrowed down by performing a series
of successive tests.

Our logic is incomparable with the one discussed in the previous example, in
which observations have a cost, but no temporal aspect is considered. In this
work we do not consider costs, but we study the evolution of knowledge through
time in addition to dynamic observation change. We now illustrate with an
example how both interact.

######  Example 2.11 (Security scenario).

Consider a system with two possible levels of security clearance, which define
what information users have access to, and are modelled by observations
$o_{1}$ and $o_{2}$. In this scenario, we want to hide a secret $p$ from the
users. A desirable property is thus expressed by the formula
$(\Delta^{o_{1}}\mathit{A}G\neg\mathit{K}p)\wedge(\Delta^{o_{2}}\mathit{A}G\neg\mathit{K}p)$,
which means that a user using either $o_{1}$ or $o_{2}$ will never know that
$p$ holds. Model $M$ from Figure 1 satisfies this formula.

Now consider the formula
$\varphi=\Delta^{o_{1}}\mathit{E}F\Delta^{o_{2}}\mathit{K}p$, which means that
if the user starts with observation $o_{1}$, there exists a moment where she
might discover the secret by changing her observation. We show that $M$
satisfies $\varphi$ and thus that it should forbid users to change their
security level. Consider the history $h=s_{0}s_{2}s_{5}$ in model $M$ with
initial observation $o_{1}$. At time 0 the user knows that the system is in
state $s_{0}$. After going to $s_{2}$, she does not know if the current state
is $s_{2}$ or $s_{1}$, as they are indistinguishable using $o_{1}$. At time 2,
at first the user does not know whether the system is in $s_{4}$ or $s_{5}$.
Even though $s_{6}$ and $s_{5}$ are indistinguishable with $o_{1}$, she does
not consider $s_{6}$ possible, as she remembers that the system was not in
$s_{3}$ before. Now, if she changes to observation $o_{2}$, she sees that the
system is either in state $s_{5}$ or $s_{6}$. Refining her previous knowledge
that the system is either in state $s_{4}$ or $s_{5}$, she deduces that the
current state is $s_{5}$, and that $p$ holds.

pt$s_{0}$$\neg p\leavevmode\nobreak\ $ptpt$s_{2}$$\neg p$$s_{1}$$\neg
p$$s_{3}$$\neg p$$s_{5}$$p$$s_{4}$$\neg p$$s_{6}$$\neg
p$ptptptptptptptptptpt$\sim_{o_{1}}$pt$\sim_{o_{1}}$pt$\sim_{o_{2}}$pt$\sim_{o_{2},o_{1}}$
Figure 1. Model $M$ in the security example

######  Example 2.12 (Fault-Tolerant Diagnosability).

Diagnosability is a property of systems in which the occurrence of a failure
is always eventually detected [22]. In the setting considered in [7], a
diagnosability condition is a pair $(c_{1},c_{2})$ of nonempty disjoint sets
of states that the system should always be able to tell apart. The system is
monitored through a set of sensors, and they study the problem of finding
minimal sets of sensors that ensure diagnosability. That is, find a minimal
sensor configuration sc such that
$\Delta^{o_{\text{sc}}}\mathit{A}\mathit{G}(\mathit{K}c_{1}\vee\mathit{K}c_{2})$
holds, where $o_{\text{sc}}$ is the observation corresponding to sensor
configuration sc.

In $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ one can express and model-
check a stronger notion of diagnosability that we call fault-tolerant
diagnosability, where the system must remain diagnosable even after the loss
of a sensor. For a given diagnosability condition $(c_{1},c_{2})$ and sensor
configuration sc, we write $o_{\text{sc}}$ the original observation (with
every sensor in sc), $o_{i}$ the observation where sensor $i$ failed, and
$p_{i}$ is a proposition indicating the failure of sensor $i$. The following
formula expresses that sensor configuration sc ensures fault-tolerant
diagnosability of the system:

$\Phi_{\text{diag}}=\Delta^{o_{\text{sc}}}\mathit{A}\mathit{G}((\mathit{K}c_{1}\vee\mathit{K}c_{2})\wedge(p_{i}\rightarrow\Delta^{o_{i}}\mathit{A}\mathit{G}(\mathit{K}c_{1}\vee\mathit{K}c_{2}))).$

Observe that it is possible for a system to satisfy $\Phi_{\text{diag}}$ but
not $\Delta^{o_{i}}\mathit{A}\mathit{G}(\mathit{K}c_{1}\vee\mathit{K}c_{2})$
if sensor $i$, before failing, brings some piece of information that is
crucial for diagnosis.

###  2.5. Model-checking problem

We are interested in the model checking-problem for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ which consists in, given a model
$M$ and a formula $\varphi$, deciding whether $M\models\varphi$.

Model-checking approach. Perfect-recall semantics refers to histories of
unbounded length, but it is well known that in many situations it is possible
to maintain a bounded amount of information that is sufficient to deal with
perfect recall. We show that it is also the case for our logic, by
generalising the classic approach to take into account observation change.
Intuitively, it is enough to know the current state, the current observation
and the set of states that the agent believes the system might be in. The
latter is usually called _information set_ in epistemic temporal logics and
games with imperfect information. We define an alternative semantics based on
information sets instead of histories and records, and we prove that this
semantics is equivalent to the natural one presented in this section. Because
information sets are of bounded size, it is then easy to build from this
alternative semantics a model checking algorithm for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$.

##  3\. Alternative semantics

We define an alternative semantics for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$. It is based on information sets,
a classic notion in games with imperfect information [29], whose definition we
now adapt to our setting.

######  Definition 3.1 (Information sets).

Given a model $M$, the information set $I(h,r)$ after a history $h$ and an
observation record $r$ is defined as follows:

$I(h,r)=\\{s\in S\mid\exists
h^{\prime},h^{\prime}\approx^{r}h\leavevmode\nobreak\
\text{and}\leavevmode\nobreak\ \mbox{last}(h^{\prime})=s\\}.$

This information is sufficient to evaluate epistemic formulas for one agent
when we consider the S5 semantics of knowledge, i.e., when
indistinguishability relations are equivalence relations as is the case here.
We now describe how this information can be maintained along the evaluation of
a formula. To do so, we define two update functions for information sets. One
is used when the agent changes of observational power, and the other when a
transition is taken in the model.

######  Definition 3.2 (Information set updates).

Fix a model
$M=(\textnormal{AP},S,T,V,\\{\sim_{o}\\}_{o\in\mathcal{O}},{{s}^{\iota}},o^{\iota})$.
Functions $U_{T}$ and $U_{\Delta}$ are defined as follows, for all $I\subseteq
S$, all $s,s^{\prime}\in S$ and $o,o^{\prime}\in\mathcal{O}$.

$\begin{array}[]{l}U_{T}(I,s^{\prime},o)=T(I)\cap[s^{\prime}]_{o}\\\
U_{\Delta}(I,s,o^{\prime})=I\cap[s]_{o^{\prime}}\end{array}$

These updates read as follows. When the agent has observational power $o$ and
information set $I$, and the model takes a transition to a state $s^{\prime}$,
the new information set is $U_{T}(I,s^{\prime},o)$, which consists of all
successors of her previous information set $I$ that are
$\sim_{o}$-indistinguishable with the new state $s^{\prime}$. When the agent
is in state $s$ with information set $I$, and she changes for observational
power $o^{\prime}$, her new information set is $U_{\Delta}(I,s,o^{\prime})$,
i.e., all states that she considered possible before and that she still
considers possible after switching to $o^{\prime}$.

We let $O(h,r)$ be the last observation taken by the agent after history $h$,
according to $r$. Formally, $O(h,r)=o_{n}$ if
${ol}(r,|h|-1)=o_{1}\cdot\ldots\cdot o_{n}$. The following result establishes
that the functions $U_{\Delta}$ and $U_{T}$ correctly update information sets.
It is proved by simple application of the definitions.

######  Proposition 3.3.

For every history $h\cdot s$, every observation record $r$ that stops at $h$,
and every observation $o$, it holds that

$\begin{array}[]{rcl}I(h\cdot s,r)&=&U_{T}(I(h,r),s,O(h,r))\mbox{,\quad
and}\\\
I(h,r\cdot(o,|h|-1))&=&U_{\Delta}(I(h,r),\mbox{last}(h),o).\end{array}$

Using these update functions we can now define our alternative semantics for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$.

######  Definition 3.4 (Alternative semantics).

Fix a model $M$. A history formula $\varphi$ is evaluated in a state $s$, an
information set $I$ and an observation $o$. A path formula $\psi$ is
interpreted on a run $\pi$, an information set $I$ and an observation $o$. The
semantic relation $\models_{I}$ is defined by induction on formulas:

$\begin{array}[]{l c l}s,I,o\models_{I}p&\mbox{if}&p\in V(s)\\\\[1.0pt]
s,I,o\models_{I}\neg\varphi&\mbox{if}&s,I,o\not\models_{I}\varphi\\\\[1.0pt]
s,I,o\models_{I}\varphi_{1}\wedge\varphi_{2}&\mbox{if}&s,I,o\models_{I}\varphi_{1}\text{
and }s,I,o\models_{I}\varphi_{2}\\\\[1.0pt]
s,I,o\models_{I}\mathit{A}\psi&\mbox{if}&\forall\pi\mbox{ s.t.
}\pi_{0}=s,\;\pi,I,o\models_{I}\psi\\\\[1.0pt]
s,I,o\models_{I}\mathit{K}\varphi&\mbox{if}&\forall s^{\prime}\in
I,\;s^{\prime},I,o\models_{I}\varphi\\\\[1.0pt]
s,I,o\models_{I}\Delta^{o^{\prime}}\varphi&\mbox{if}&s,U_{\Delta}(I,s,o^{\prime}),o^{\prime}\models_{I}\varphi\\\\[1.0pt]
\pi,I,o\models_{I}\varphi&\mbox{if}&\pi_{0},I,o\models_{I}\varphi\\\\[1.0pt]
\pi,I,o\models_{I}\neg\psi&\mbox{if}&\pi,I,o\not\models_{I}\psi\\\\[1.0pt]
\pi,I,o\models_{I}\psi_{1}\wedge\psi_{2}&\mbox{if}&\pi,I,o\models_{I}\psi_{1}\text{
and }\pi,I,o\models_{I}\psi_{2}\\\\[1.0pt]
\pi,I,o\models_{I}\mathit{X}\psi&\mbox{if}&\pi_{\geq
1},U_{T}(I,\pi_{1},o),o\models_{I}\psi\\\\[1.0pt]
\pi,I,o\models_{I}\psi_{1}\mathit{U}\psi_{2}&\mbox{if}&\exists n\geq 0\mbox{
such that }\pi_{\geq n},\;U_{T}^{n}(I,\pi,o),o\models_{I}\psi_{2}\mbox{
and}\\\\[1.0pt] &&\forall m\mbox{ such that }0\leq m<n,\;\pi_{\geq
m},U_{T}^{m}(I,\pi,o),o\models_{I}\psi_{1},\end{array}$

where $U_{T}^{n}(I,\pi,o)$ is the iteration of the temporal update, defined
inductively as follows:

  * •

$U_{T}^{0}(I,\pi,o)=I$, and

  * •

$U_{T}^{n+1}(I,\pi,o)=U_{T}(U_{T}^{n}(I,\pi,o),\pi_{n+1},o)$.

Using Proposition 3.3, one can prove that the natural semantics $\models$ and
the information semantics $\models_{I}$ are equivalent (the proof is in
Appendix A).

######  Theorem 3.5.

For every history formula $\varphi$, model $M$, history $h$ and observation
record $r$ that stops at $h$,

$h,r\models\varphi\quad\mbox{iff}\quad\mbox{last}(h),I(h,r),o(h,r)\models_{I}\varphi.$

##  4\. Model checking $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$

In this section we devise a model-checking procedure based on the equivalence
between the natural and alternative semantics (Theorem 3.5), and we prove the
following result.

######  Theorem 4.1.

Model checking $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ is in Exptime .

Augmented model. Given a model $M$, we define an augmented model $\hat{M}$ in
which the states are tuples $(s,I,o)$ consisting of a state $s$ of the
original model, an information set $I$ and an observation $o$. According to
Theorem 3.5, history formulas can be viewed on this model as state formulas,
and a model checking procedure can be devised by merely following the
definition of the alternative semantics.

Let
$M=(\textnormal{AP},S,T,V,\\{\sim_{o}\\}_{o\in\mathcal{O}},{{s}^{\iota}},o^{\iota})$.
We define the Kripke structure
$\hat{M}=(S^{\prime},T^{\prime},V^{\prime},{{s}^{\iota}}^{\prime})$, where:

  * •

$S^{\prime}=S\times 2^{S}\times\mathcal{O}$,

  * •

$(s,I,o)\leavevmode\nobreak\ T^{\prime}\leavevmode\nobreak\
(s^{\prime},I^{\prime},o)\mbox{ if }s\leavevmode\nobreak\
T\leavevmode\nobreak\ s^{\prime}$ and $I^{\prime}=U_{T}(I,s^{\prime},o)$,

  * •

$V^{\prime}(s,I,o)=V(s)$, and

  * •

${{s}^{\iota}}^{\prime}=({{s}^{\iota}},[{{s}^{\iota}}]_{o^{\iota}},o^{\iota})$.

We call $\hat{M}$ the _augmented model_ , and we write $\hat{M}_{o}$ the
Kripke structure obtained by restricting $\hat{M}$ to states of the form
$(s,I,o^{\prime})$ where $o^{\prime}=o$. Note that the different $\hat{M}_{o}$
are disjoint with regards to $T^{\prime}$.

Model-checking procedure. We now define the function
Check$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ which evaluates a history
formula in a state of the augmented model $\hat{M}$:

Function Check$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$
($\hat{M},(s_{c},I_{c},o_{c}),\Phi$) returns _true_ if
$M,s_{c},I_{c},o_{c}\models_{I}\varphi$ and _false_ otherwise, and is defined
as follows: if $\Phi$ is a $\textnormal{{CTL}}^{*}$ formula, we evaluate it
using a classic model-checking procedure for $\textnormal{{CTL}}^{*}$.
Otherwise, $\Phi$ contains a subformula of the form
$\varphi=\mathit{K}\varphi_{1}$ or $\varphi=\Delta^{o^{\prime}}\varphi_{1}$
where $\varphi_{1}\in\textnormal{{CTL}}^{*}$. We evaluate $\varphi_{1}$ in
every state of $\hat{M}$, and mark those that satisfy $\varphi_{1}$ with a
fresh atomic proposition $p_{\varphi_{1}}$. Then, if
$\varphi=\mathit{K}\varphi_{1}$, we mark with a fresh atomic proposition
$p_{\varphi}$ every state $(s,I,o)$ of $\hat{M}$ such that for every
$s^{\prime}\in I$, $(s^{\prime},I,o)$ is marked with $p_{\varphi_{1}}$. Else,
$\varphi=\Delta^{o^{\prime}}\varphi_{1}$ and we mark with a fresh proposition
$p_{\varphi}$ every state $(s,I,o)$ such that
$(s,U_{\Delta}(I,s,o^{\prime}),o^{\prime})$ is marked with $p_{\varphi_{1}}$.
Finally, we recursively call function
Check$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ on the marked model and
formula $\Phi^{\prime}$ obtained by replacing $\varphi$ with $p_{\varphi}$ in
$\Phi$.

To model check a formula $\varphi$ in a model $M$, we first build $\hat{M}$,
and call function Check$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$
($\hat{M},(s_{\iota},[s_{\iota}]_{o_{\iota}},o_{\iota}),\varphi$).

######  Example 4.2.

Let $M$ be the model depicted in Fig. 2, where $o_{1}$ is the blind
observation ($\sim_{o_{1}}=S\times S$), $o_{2}$ is the perfect observation
($s\sim_{o_{2}}s^{\prime}\ \mathit{iff}\ s=s^{\prime}$), $s_{1}$ is the
initial state and the agent is initially blind (the initial observation is
$o_{1}$). Note that we did not represent indistinguishability relations
$o_{1}$ and $o_{2}$. The augmented model $\hat{M}$ is depicted in Fig. 3,
where we only drew relevant states, i.e. those that are reachable from the
initial state via transitions and observation changes.

Consider formula
$\varphi=\Delta^{o_{2}}(\mathit{K}q\vee\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)$
which means that if the agent changes to the perfect observation, then either
the agent knows that $q$ holds, or even after switching back to the blind
observation she knows that in every possible next step, $q$ holds. After
running the algorithm, we get the following valuation for $\hat{M}$:

$\begin{array}[]{l c
l}V^{\prime}(s_{1},\\{s_{1},s_{2}\\},o_{1})&=&\\{q,p_{\varphi}\\}\\\
V^{\prime}(s_{2},\\{s_{1},s_{2}\\},o_{1})&=&\\{p_{\varphi}\\}\end{array}\newline
\begin{array}[]{l c
l}V^{\prime}(s_{1},\\{s_{1}\\},o_{1})&=&\\{q,p_{(\mathit{K}q)},p_{(\mathit{K}q\vee\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)},p_{\varphi}\\}\\\
V^{\prime}(s_{2},\\{s_{2}\\},o_{1})&=&\\{p_{(\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)},p_{(\mathit{K}q\vee\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)},p_{\varphi}\\}\\\
V^{\prime}(s_{1},\\{s_{1}\\},o_{2})&=&\\{q,p_{(\mathit{K}q)},p_{(\mathit{K}q\vee\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)},p_{\varphi}\\}\\\
V^{\prime}(s_{2},\\{s_{2}\\},o_{2})&=&\\{p_{(\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)},p_{(\mathit{K}q\vee\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)},p_{\varphi}\\}\\\
\end{array}$

Let us explain why $p_{\varphi}$ is eventually marked in the initial state
$(s_{1},\\{s_{1},s_{2}\\},o_{1})$ of $\hat{M}$. First look at state
$(s_{1},\\{s_{1}\\},o_{2})$. Since $q$ is in $V(s_{1})$, $q$ is also in
$V^{\prime}(s_{1},\\{s_{1}\\},o_{2})$. Next, because for all $s^{\prime}$ in
$\\{s_{1}\\}$, $q$ is in $V^{\prime}(s^{\prime},\\{s_{1}\\},o_{2})$, the fresh
atom $p_{(\mathit{K}q)}$ is added in $V^{\prime}(s_{1},\\{s_{1}\\},o_{2})$ and
thus the fresh atom
$p_{(\mathit{K}q\vee\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)}$ is later
also added in $V^{\prime}(s_{1},\\{s_{1}\\},o_{2})$. Finally, when
$\Delta^{o_{2}}(\mathit{K}q\vee\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)$
is evaluated on $(s_{1},\\{s_{1},s_{2}\\},o_{1})$, since
$U_{\Delta}(\\{s_{1},s_{2}\\},s_{1},o_{2})=\\{s_{1}\\}$ and
$p_{(\mathit{K}q\vee\Delta^{o_{1}}\mathit{K}\mathit{A}\mathit{X}q)}$ is in
$V^{\prime}(s_{1},\\{s_{1}\\},o_{2})$, the fresh atom $p_{\varphi}$ is
eventually added in $V^{\prime}(s_{1},\\{s_{1},s_{2}\\},o_{1})$.

The algorithm thus returns, as expected, that $M\models\varphi$.

pt$s_{1}$$q$ptpt$s_{2}$$\neg q$pt

Figure 2. Model $M$

pt$s_{1},\\{s_{1},s_{2}\\},o_{1}$$q$ptpt$s_{2},\\{s_{1},s_{2}\\},o_{1}$$\neg
q$$s_{1},\\{s_{1}\\},o_{1}$$q$$s_{2},\\{s_{2}\\},o_{1}$$\neg
q$$s_{1},\\{s_{1}\\},o_{2}$$q$$s_{2},\\{s_{2}\\},o_{2}$$\neg q$ptptpt

Figure 3. The augmented model $\hat{M}$

Algorithm correctness. The correctness of the algorithm follows from the
following properties:

  * •

For each formula $\mathit{K}\varphi_{1}$ chosen by the algorithm,
$p_{\varphi}\in V^{\prime}(s,I,o)\ \mathit{iff}\
M,s,I,o\models_{I}\mathit{K}\varphi_{1}$

  * •

For each formula $\Delta^{o^{\prime}}\varphi_{1}$ chosen by the algorithm,
$p_{\varphi}\in V^{\prime}(s,I,o)\ \mathit{iff}\
M,s,I,o\models_{I}\Delta^{o^{\prime}}\varphi_{1}$

Complexity analysis. In the following, we let $|M|$ be the number of states in
model $M$. Model checking a $\textnormal{{CTL}}^{*}$ formula $\varphi$ on a
model $M$ with state-set $S$ can be done in time $2^{O(|\varphi|)}O(|S|)$ [11,
17]. Our procedure, for a $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ formula
$\varphi$ and a model $M$, calls the $\textnormal{{CTL}}^{*}$ model-checking
procedure for at most $|\varphi|$ formulas of size at most $|\varphi|$, on
each state of the augmented model $\hat{M}$. The latter is of size
$2^{O(|M|)}\times|\mathcal{O}|$, but each call to the $\textnormal{{CTL}}^{*}$
model-checking procedure is performed on a disjoint component $\hat{M}_{o}$ of
size $2^{O(|M|)}$. Our overall procedure thus runs in time
$|\mathcal{O}|\times 2^{O(|\varphi|+|M|)}$.

##  5\. Multi-agent setting

We now extend $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ to the multi-agent
setting. We fix $\mathit{Ag}=\\{a_{1},\ldots,a_{m}\\}$ a finite set of agents
and define the logic $\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$. This
logic contains, for each agent $a$ and observation $o$, an operator
$\Delta^{o}_{a}$ which reads as “agent $a$ changes for observation $o$”. We
consider that these observation changes are public in the sense that all
agents are aware of them. The reason is that if agent $a$ changes observation
without agent $b$ knowing it, agent $b$ may entertain false beliefs about what
agent $a$ knows. This would not be consistent with the S5 semantics of
knowledge that we consider in this work, where false beliefs are ruled out by
the Truth axiom $\mathit{K}\varphi\to\varphi$.

###  5.1. Syntax and natural semantics

We first extend the syntax, with knowledge operators $\mathit{K}_{a}$ and
observation change operators $\Delta^{o}_{a}$ for each agent.

######  Definition 5.1 (Syntax).

The sets of history formulas $\varphi$ and path formulas $\psi$ are defined by
the following grammar:

$\begin{array}[]{ccl}\varphi&::=&p\leavevmode\nobreak\ |\leavevmode\nobreak\
\neg\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\varphi\wedge\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathit{A}\psi\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathit{K}_{a}\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\Delta^{o}_{a}\varphi\\\ \psi&::=&\varphi\leavevmode\nobreak\
|\leavevmode\nobreak\ \neg\psi\leavevmode\nobreak\ |\leavevmode\nobreak\
\psi\wedge\psi\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathit{X}\psi\leavevmode\nobreak\ |\leavevmode\nobreak\
\psi\mathit{U}\psi,\end{array}$

where $p\in\mathcal{AP}$, $a\in\mathit{Ag}$ and $o\in\mathcal{O}$.

Formulas of $\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ are all history
formulas.

The models of $\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ are as for the
one-agent case, except that we assign one initial observation to each agent.
In the following we shall write $\bm{o}$ for a tuple
$\\{o_{a}\\}_{a\in\mathit{Ag}}$, $\bm{o}_{a}$ for $o_{a}$, and
$\bm{o}[a\leftarrow o]$ for the tuple $\bm{o}$ where $\bm{o}_{a}$ is replaced
with $o$. Finally, for $i\in\\{1,\ldots,m\\}$, $\bm{o}_{i}$ refers to
$\bm{o}_{a_{i}}$.

######  Definition 5.2 (Multiagent models).

A _multiagent Kripke structure with observations_ is given by a structure
$M=(\textnormal{AP},S,T,V,\\{\sim_{o}\\}_{o\in\mathcal{O}},{{s}^{\iota}},\bm{o}^{\iota})$,
where

  * •

$\textnormal{AP}\subset\mathcal{AP}$ is a finite subset of atomic
propositions,

  * •

$S$ is a set of states,

  * •

$T\subseteq S\times S$ is a left-total transition relation between states,

  * •

$V:S\rightarrow 2^{\textnormal{AP}}$ is a valuation function,

  * •

$\sim_{o}\subseteq S\times S$ is an equivalence relation, for each
$o\in\mathcal{O}$,

  * •

${{s}^{\iota}}\subseteq S$ is an initial state, and

  * •

$\bm{o}^{\iota}$ is the initial observation for each agent.

We now adapt some definitions to the multi-agent setting.

Records tuples. We now need one observation record for each agent. We shall
write $\bm{r}$ for a tuple $\\{r_{a}\\}_{a\in\mathit{Ag}}$. Given a tuple
$\bm{r}=\\{r_{a}\\}_{a\in\mathit{Ag}}$ and $a\in\mathit{Ag}$ we write
$\bm{r}_{a}$ for $r_{a}$, and for an observation $o$ and time $n$ we let
$\bm{r}\cdot(o,n)_{a}$ be the record tuple $\bm{r}$ where $\bm{r}_{a}$ is
replaced with $\bm{r}_{a}\cdot(o,n)$. Finally, for $i\in\\{1,\ldots,m\\}$,
$\bm{r}_{i}$ refers to $\bm{r}_{a_{i}}$.

Observations at time $n$. We let ${ol}_{a}(\bm{r},n)$ be the list of
observations used by agent $a$ at time $n$:

$\displaystyle{ol}_{a}(\bm{r},0)$ $\displaystyle=\bm{o}^{\iota}_{a}\cdot
o_{1}\cdot\ldots\cdot o_{k},$ $\displaystyle\mbox{if
}\bm{r}_{a}[0]=(o_{1},0)\cdot\ldots\cdot(o_{k},0),\mbox{ and}$
$\displaystyle{ol}_{a}(\bm{r},n+1)$
$\displaystyle=\mbox{last}({ol}_{a}(\bm{r},n))\cdot o_{1}\cdot\ldots\cdot
o_{k},$ $\displaystyle\mbox{if
}\bm{r}_{a}[n+1]=(o_{1},n+1)\cdot\ldots\cdot(o_{k},n+1).$

######  Definition 5.3 (Dynamic synchronous perfect recall).

Given a record tuple $\bm{r}$, two histories $h$ and $h^{\prime}$ are
equivalent for agent $a$, written $h\approx^{\bm{r}}_{a}h^{\prime}$, if

$|h|=|h^{\prime}|\leavevmode\nobreak\ \textit{and}\leavevmode\nobreak\ \forall
i<|h|,\leavevmode\nobreak\ \forall o\in{ol}_{a}(\bm{r},i),\leavevmode\nobreak\
h_{i}\sim_{o}h^{\prime}_{i}.$

######  Definition 5.4 (Natural semantics).

Let $M$ be a model, $h$ a history in $M$ and $\bm{r}$ a record tuple. We only
define the semantics for the following inductive cases, the remaining ones are
straightforwardly adapted from the one-agent case (Definition 2.8).

$\begin{array}[]{lcl}h,\bm{r}\models\mathit{K}_{a}\varphi&\mbox{if}&\forall
h^{\prime}\mbox{ s.t.
}h^{\prime}\approx^{\bm{r}}_{a}h,\;h^{\prime},\bm{r}\models\varphi\\\\[2.0pt]
h,\bm{r}\models\Delta^{o}_{a}\varphi&\mbox{if}&h,\bm{r}\cdot(o,|h|-1)_{a}\models\varphi\end{array}$

A model $M$ with initial state ${{s}^{\iota}}$ _satisfies_ a
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ formula $\varphi$, written
$M\models\varphi$, if ${{s}^{\iota}},\bm{\emptyset}\models\varphi$, where
$\bm{\emptyset}$ is the tuple where each agent has empty observation record.

###  5.2. Alternative semantics

As in the one-agent case, we define an alternative semantics that we prove
equivalent to the natural one and upon which we build our model-checking
algorithm. The main difference here is that we need richer structures than
information sets to represent an epistemic situation of a system with multiple
agents. For instance, to evaluate formula
$\mathit{K}_{a}\mathit{K}_{b}\mathit{K}_{c}p$, we need to know what agent $a$
knows about agent $b$’s knowledge of agent $c$’s knowledge of the system’s
state. To do so we use the $k$-trees introduced in [24, 25] in the setting of
static observations, and which contain enough information to evaluate formulas
of knowledge depth $k$.

$k$-trees. Fix a model
$M=(\textnormal{AP},S,T,V,\\{\sim_{o}\\}_{o\in\mathcal{O}},{{s}^{\iota}},\bm{o}^{\iota})$.
Intuitively, a $k$-tree over $M$ is a structure of the form $\langle
s,\mathcal{I}_{1},\ldots,\mathcal{I}_{m}\rangle$, where $s\in S$ is the
current state of the system, and for each $i\in\\{1,\ldots,m\\}$,
$\mathcal{I}_{i}$ is a set of $(k-1)$-trees that represents the state of
knowledge (of depth $k-1$) of agent $a_{i}$. Formally, for every history $h$
and record tuple $\bm{r}$ we define by induction on $k$ the $k$-tree
$I^{k}(h,\bm{r})$ as follows:

$\displaystyle I^{0}(h,\bm{r})$
$\displaystyle=\langle\mbox{last}(h),\emptyset,\ldots,\emptyset\rangle$
$\displaystyle I^{k+1}(h,\bm{r})$
$\displaystyle=\langle\mbox{last}(h),\mathcal{I}_{1},\ldots,\mathcal{I}_{m}\rangle,$

where for each $i$, $\mathcal{I}_{i}=\\{I^{k}(h^{\prime},\bm{r})\mid
h^{\prime}\approx^{\bm{r}}_{a_{i}}h\\}$.

For a $k$-tree $I^{k}=\langle
s,\mathcal{I}_{1},\ldots,\mathcal{I}_{m}\rangle$, we call $s$ the _root_ of
$I^{k}$, and write it $r(I^{k})$. We also write $I^{k}(a)$ for
$\mathcal{I}_{i}$, where $a=a_{i}$, and we let ${\mathcal{T}}^{k}$ be the set
of $k$-trees for $M$.

Observe that for one agent (i.e. $m=1$), a $1$-tree is an information set
together with the current state.

Updating $k$-trees. We now generalise our update functions $U_{\Delta}$ and
$U_{T}$ (Definition 3.2) to update $k$-trees. We first define, by induction on
$k$, the function $U_{T}^{k}$ that updates $k$-trees when a transition is
taken.

$\displaystyle U_{T}^{0}(\langle
s,\emptyset,\ldots,\emptyset\rangle,s^{\prime},\bm{o})$ $\displaystyle=\langle
s^{\prime},\emptyset,\ldots,\emptyset\rangle$ $\displaystyle
U_{T}^{k+1}(\langle
s,\mathcal{I}_{1},\ldots,\mathcal{I}_{m}\rangle,s^{\prime},\bm{o})$
$\displaystyle=\langle
s^{\prime},\mathcal{I}^{\prime}_{1},\ldots,\mathcal{I}^{\prime}_{m}\rangle,$

where for each $i$,

$\mathcal{I}^{\prime}_{i}=\\{U_{T}^{k}(I^{k},s^{\prime\prime},\bm{o})\mid
I^{k}\in\mathcal{I}_{i}\mbox{,
}s^{\prime\prime}\sim_{\bm{o}_{i}}s^{\prime}\mbox{ and
}r(I^{k})Ts^{\prime\prime}\\}.$

$U_{T}^{k}$ takes the current $k$-tree $\langle
s,\mathcal{I}_{1},\ldots,\mathcal{I}_{m}\rangle$, the new state $s^{\prime}$
and the current observation $\bm{o}$ for each agent, and returns the new
$k$-tree after the transition.

We now define the second update function $U_{\Delta}^{k}$, which is used when
an agent $a_{i}$ changes observation for some $o^{\prime}$.

$\displaystyle U_{\Delta}^{0}(\langle
s,\emptyset,\ldots,\emptyset\rangle,o,a_{i})$ $\displaystyle=\langle
s,\emptyset,\ldots,\emptyset\rangle$ $\displaystyle U_{\Delta}^{k+1}(\langle
s,\mathcal{I}_{1},\ldots,\mathcal{I}_{m}\rangle,o,a_{i})$
$\displaystyle=\langle
s,\mathcal{I}^{\prime}_{1},\ldots,\mathcal{I}^{\prime}_{m}\rangle,$

where for each $j\neq i$,

$\mathcal{I}^{\prime}_{j}=\\{U_{\Delta}^{k}(I^{k},o^{\prime},a_{i})\mid
I^{k}\in\mathcal{I}_{j}\\},\mbox{ and}$
$\mathcal{I}^{\prime}_{i}=\\{U_{\Delta}^{k}(I^{k},o^{\prime},a_{i})\mid
I^{k}\in\mathcal{I}_{i}\mbox{ and }r(I^{k})\sim_{o^{\prime}}s\\}.$

The intuition is that when agent $a_{i}$ changes observation for $o^{\prime}$,
in every place of the $k$-tree that refers to agent $a_{i}$’s knowledge, we
remove possible states (and corresponding subtrees) that are no longer
equivalent to the current possible state for $a_{i}$’s new observation
$o^{\prime}$.

We let $\bm{O}(h,\bm{r})$ be the tuple of last observations taken by each
agent after history $h$, according to $\bm{r}$. For each $a\in\mathit{Ag}$,
$\bm{O}(h,\bm{r})_{a}=o_{n}$ if ${ol}_{a}(\bm{r},|h|-1)=o_{1}\cdot\ldots\cdot
o_{n}$. The following proposition establishes that functions $U_{T}^{k}$ and
$U_{\Delta}^{k}$ correctly update $k$-trees.

######  Proposition 5.5.

For every history $h\cdot s$, record tuple $\bm{r}$ that stops at $h$,
observation tuple $\bm{o}$ and integer $k$, it holds that

$\begin{array}[]{rcl}I^{k}(h\cdot
s,\bm{r})&=&U_{T}^{k}(I^{k}(h,\bm{r}),s,\bm{o}(h,\bm{r})),\mbox{ and}\\\
I^{k}(h,\bm{r}\cdot(o,|h|-1)_{a})&=&U_{\Delta}^{k}(I^{k}(h,\bm{r}),o,a).\end{array}$

The proof can be found in Appendix B.

We now define the alternative semantics for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$.

######  Definition 5.6 (Alternative semantics).

The semantics of a history formula $\varphi$ of knowledge depth $k$ is defined
inductively on a $k$-tree $I^{k}$ and a tuple of current observations $\bm{o}$
(note that the current state is the root of the $k$-tree).

$\begin{array}[]{l c l}I^{k},\bm{o}\models_{I}p&\mbox{if}&p\in
V(r(I^{k}))\\\\[2.0pt]
I^{k},\bm{o}\models_{I}\neg\varphi&\mbox{if}&I^{k},\bm{o}\not\models_{I}\varphi\\\\[2.0pt]
I^{k},\bm{o}\models_{I}\varphi_{1}\wedge\varphi_{2}&\mbox{if}&I^{k},\bm{o}\models_{I}\varphi_{1}\text{
and }I^{k},\bm{o}\models_{I}\varphi_{2}\\\\[2.0pt]
I^{k},\bm{o}\models_{I}\mathit{A}\psi&\mbox{if}&\forall\pi\mbox{ s.t.
}\pi_{0}=r(I^{k}),\;\pi,I^{k},\bm{o}\models_{I}\psi\\\\[2.0pt]
I^{k},\bm{o}\models_{I}\mathit{K}_{a}\varphi&\mbox{if}&\forall I^{k-1}\in
I^{k}(a),\;I^{k-1},\bm{o}\models_{I}\varphi\\\\[2.0pt]
I^{k},\bm{o}\models_{I}\Delta^{o^{\prime}}_{a}\varphi&\mbox{if}&U_{\Delta}^{k}(I^{k},o^{\prime},a),\bm{o}[a\leftarrow
o^{\prime}]\models_{I}\varphi\\\ &&\quad\quad\quad\mbox{where
}\bm{o}[a\leftarrow o^{\prime}]\mbox{ is }\bm{o}\mbox{ where }\bm{o}_{a}\mbox{
is replaced with }o^{\prime}\\\\[2.0pt]
\pi,I^{k},\bm{o}\models_{I}\varphi&\mbox{if}&I^{k},\bm{o}\models_{I}\varphi\\\\[2.0pt]
\pi,I^{k},\bm{o}\models_{I}\neg\psi&\mbox{if}&\pi,I^{k},\bm{o}\not\models_{I}\psi\\\\[2.0pt]
\pi,I^{k},\bm{o}\models_{I}\psi_{1}\wedge\psi_{2}&\mbox{if}&\pi,I^{k},\bm{o}\models_{I}\psi_{1}\text{
and }\pi,I^{k},\bm{o}\models_{I}\psi_{2}\\\\[2.0pt]
\pi,I^{k},\bm{o}\models_{I}\mathit{X}\psi&\mbox{if}&\pi_{\geq
1},U_{T}^{k}(I^{k},\pi_{1},\bm{o}),\bm{o}\models_{I}\psi\\\\[2.0pt]
\pi,I^{k},\bm{o}\models_{I}\psi_{1}\mathit{U}\psi_{2}&\mbox{if}&\exists n\geq
0\mbox{ such that }\pi_{\geq
n},{U_{T}^{k}}^{n}(I^{k},\pi,\bm{o}),\bm{o}\models_{I}\psi_{2}\mbox{
and}\\\\[1.0pt] &&\forall m\mbox{ such that }0\leq m<n,\;\pi_{\geq
m},{U_{T}^{k}}^{m}(I^{k},\pi,\bm{o}),\bm{o}\models_{I}\psi_{1},\end{array}$

where ${U_{T}^{k}}^{n}$ is the iteration of $U_{T}^{k}$, defined similarly to
the mono-agent case.

The following theorem can be proved similarly to Theorem 3.5, using
Proposition 5.5 instead of Proposition 3.3.

######  Theorem 5.7.

For every history formula $\varphi$ of knowledge depth $k$, each model $M$,
history $h$ and tuple of records $\bm{r}$,

$h,\bm{r}\models\varphi\quad\mbox{iff}\quad
I^{k}(h,\bm{r}),\bm{o}(h,r)\models_{I}\varphi.$

##  6\. Model checking $\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$

Like in the mono-agent case, it is rather easy to devise from this alternative
semantics a model-checking algorithm for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$, the main difference being
that the states of the augmented model are now $k$-trees. In this section we
adapt the model-checking procedure for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ to the multi-agent setting, once
again relying on the equivalence between the natural and alternative semantics
(Theorem 5.7), and we prove the following result.

######  Theorem 6.1.

The model-checking problem for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ is in $k$-EXPTIME for
formulas of knowledge depth at most $k$.

Augmented model. Given a model $M$, we define an augmented model $\hat{M}$ in
which the states are pairs $(I^{k},\bm{o})$ consisting of a $k$-tree $I^{k}$
and an observation for each agent, $\bm{o}$.

Let
$M=(\textnormal{AP},S,T,V,\\{\sim_{o}\\}_{o\in\mathcal{O}},{{s}^{\iota}},\bm{o}^{\iota})$.
We define the Kripke structure
$\hat{M}=(S^{\prime},T^{\prime},V^{\prime},{{s}^{\iota}}^{\prime})$, where:

  * •

$S^{\prime}={\mathcal{T}}^{k}\times\mathcal{O}^{\mathit{Ag}}$,

  * •

$(I^{k},\bm{o})\leavevmode\nobreak\ T^{\prime}\leavevmode\nobreak\
({I^{k}}^{\prime},\bm{o})\mbox{ if }s\leavevmode\nobreak\
T\leavevmode\nobreak\ s^{\prime}$ and
${I^{k}}^{\prime}=U_{T}^{k}(I^{k},s^{\prime},\bm{o})$, where $s=r(I^{k})$ and
$s^{\prime}=r({I^{k}}^{\prime})$,

  * •

$V^{\prime}(I^{k},\bm{o})=V(r(I^{k}))$, and

  * •

${{s}^{\iota}}^{\prime}=(I^{k}({{s}^{\iota}},\bm{\emptyset}),\bm{o}^{\iota})$.

We call $\hat{M}$ the _augmented model_ , and we write $\hat{M}_{\bm{o}}$ the
Kripke structure obtained by restricting $\hat{M}$ to states of the form
$(I^{k},\bm{o}^{\prime})$ where $\bm{o}^{\prime}=\bm{o}$. Note that the
different $\hat{M}_{\bm{o}}$ are disjoint with regards to $T^{\prime}$.

Model-checking procedure. We now define the function
Check$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ which evaluates a
history formula in a state of the augmented model $\hat{M}$:

Function Check$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$
($\hat{M},(I^{k}_{c},\bm{o}_{c}),\Phi$) returns _true_ if
$M,I^{k}_{c},\bm{o}_{c}\models_{I}\varphi$ and _false_ otherwise, and is
defined as follows: if $\Phi$ is a $\textnormal{{CTL}}^{*}$ formula, we
evaluate it using a classic model-checking procedure for
$\textnormal{{CTL}}^{*}$. Otherwise, $\Phi$ contains a subformula of the form
$\varphi=\mathit{K}_{a}\varphi^{\prime}$ or
$\varphi=\Delta^{o^{\prime}}_{a}\varphi^{\prime}$ where
$\varphi^{\prime}\in\textnormal{{CTL}}^{*}$. We evaluate $\varphi^{\prime}$ in
every state of $\hat{M}$, and mark those that satisfy $\varphi^{\prime}$ with
a fresh atomic proposition $p_{\varphi^{\prime}}$. Then, if
$\varphi=\mathit{K}_{a}\varphi^{\prime}$, we mark with a fresh atomic
proposition $p_{\varphi}$ every state $(I^{k},\bm{o})$ of $\hat{M}$ such that
for every $I^{k-1}\in I^{k}(a)$, $(I^{k-1},\bm{o})$ is marked with
$p_{\varphi^{\prime}}$. Else,
$\varphi=\Delta^{o^{\prime}}_{a}\varphi^{\prime}$ and we mark with a fresh
proposition $p_{\varphi}$ every state $(I^{k},\bm{o})$ such that
$(U_{\Delta}^{k}(I^{k},o^{\prime},a),\bm{o}[a\leftarrow o^{\prime}])$ is
marked with $p_{\varphi^{\prime}}$. Finally, we recursively call function
Check$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ on the marked model and
formula $\Phi^{\prime}$ obtained by replacing $\varphi$ with $p_{\varphi}$ in
$\Phi$.

To model check a formula $\varphi$ in a model $M$, we build $\hat{M}$ and call
Check$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$
($\hat{M},(I^{k}({{s}^{\iota}},\bm{\emptyset}),\bm{o}^{\iota}),\varphi$).

Algorithm correctness. The correctness of the algorithm follows from the
following properties:

  * •

For each formula $\mathit{K}_{a}\varphi$ chosen by the algorithm,
$p_{\varphi}\in V^{\prime}(I^{k},\bm{o})\ \mathit{iff}\
M,I^{k},\bm{o}\models_{I}\mathit{K}_{a}\varphi$

  * •

For each formula $\Delta^{o^{\prime}}_{a}\varphi$ chosen by the algorithm,
$p_{\varphi}\in V^{\prime}(I^{k},\bm{o})\ \mathit{iff}\
M,I^{k},\bm{o}\models_{I}\Delta^{o^{\prime}}_{a}\varphi$

Complexity analysis. The number of different $k$-trees for $m$ agents and a
model with $l$ states is no greater than $C_{k}=\mbox{exp}(m\times l,k)/m$,
where $\mbox{exp}(a,b)$ is defined as $\mbox{exp}(a,0)=a$ and
$\mbox{exp}(a,b+1)=a2^{\scriptsize\mbox{exp}(a,b)}$ [25]. The size of the
augmented model $\hat{M}$ is thus bounded by $\mbox{exp}(m\times
l,k)/m\times|\mathcal{O}|^{|\mathit{Ag}|}$, and it can be computed in time
$\mbox{exp}(O(m\times l),k)\times|\mathcal{O}|^{|\mathit{Ag}|}$.

Model checking a $\textnormal{{CTL}}^{*}$ formula $\varphi$ on a model $M$
with state-set $S$ can be done in time $2^{O(|\varphi|)}\times O(|S|)$ [11,
17]. For a $\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ formula $\varphi$
of knowledge depth at most $k$ and a model $M$ with $l$ states, our procedure
calls the $\textnormal{{CTL}}^{*}$ model-checking procedure for at most
$|\varphi|$ formulas of size at most $|\varphi|$, on each state of the
augmented model $\hat{M}$ which has size $\mbox{exp}(m\times
l,k)/m\times|\mathcal{O}|^{m}$. Each recursive call (for each subformula and
state of $\hat{M}$) is performed on a disjoint component $\hat{M}_{\bm{o}}$ of
size at most $\mbox{exp}(m\times l,k)/m$, and thus takes time
$2^{O(|\varphi|)}\times O(\mbox{exp}(m\times l,k)/m)$, and there are at most
$|\varphi|\times\mbox{exp}(m\times l,k)/m\times|\mathcal{O}|^{m}$ of them. Our
overall procedure thus runs in time $|\mathcal{O}|^{m}\times
2^{O(|\varphi|)}\times\mbox{exp}(O(m\times l),k)$, i.e.
$|\mathcal{O}|^{|\mathit{Ag}|}\times
2^{O(|\varphi|)}\times\mbox{exp}(O(|\mathit{Ag}|\times|M|),k)$.

##  7\. Expressivity

In this section we prove that the observation-change operator adds expressive
power to epistemic temporal logics. Formally, we compare the expressive power
of $\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ with that of
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ [14, 9], which is the syntactic
fragment of $\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ obtained by
removing the observation-change operator. Our semantics for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ generalises that of
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$, with which it coincides on
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ formulas. Note that our multi-agent
models (Definition 5.2) are more general than usual models for
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$, as they may contain observation
relations that are not initially assigned to any agent, but such relations are
mute in the evaluation of $\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ formulas.

For two logics $\mathcal{L}$ and $\mathcal{L}^{\prime}$ over the same class of
models, we say that $\mathcal{L}^{\prime}$ is _at least as expressive as_
$\mathcal{L}$, written $\mathcal{L}\preceq\mathcal{L}^{\prime}$, if for every
formula $\varphi\in\mathcal{L}$ there exists a formula
$\varphi^{\prime}\in\mathcal{L}^{\prime}$ such that
$\varphi\equiv\varphi^{\prime}$. $\mathcal{L}^{\prime}$ is _strictly more
expressive than_ $\mathcal{L}$, written
$\mathcal{L}\prec\mathcal{L}^{\prime}$, if
$\mathcal{L}\preceq\mathcal{L}^{\prime}$ and
$\mathcal{L}^{\prime}\not\preceq\mathcal{L}$. Finally, $\mathcal{L}$ and
$\mathcal{L}^{\prime}$ are _equiexpressive_ , written
$\mathcal{L}\equiv\mathcal{L}^{\prime}$, if
$\mathcal{L}\preceq\mathcal{L}^{\prime}$ and
$\mathcal{L}^{\prime}\preceq\mathcal{L}$.

######  Proposition 7.1.

For all $m\geq 1$,
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}\preceq\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$.

######  Proof 7.2.

This simply follows from the fact that
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ extends
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$.

We first point out that when there is only one observation, i.e.,
$|\mathcal{O}|=1$, the observation-change operator has no effect, and thus
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ is no more expressive than
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$.

######  Proposition 7.3.

For $|\mathcal{O}|=1$,
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}\equiv\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$.

######  Proof 7.4.

We show that for $|\mathcal{O}|=1$,
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}\preceq\textnormal{{CTL}}^{*}\textnormal{K}_{m}$,
which together with Proposition 7.1 provides the result. Observe that when
$|\mathcal{O}|=1$, observation change has no effect, and in fact observation
records can be omitted in the natural semantics. For every
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ formula $\varphi$, define the
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ formula $\varphi^{\prime}$ by
removing all observation-change operators $\Delta^{o}_{a}$ from $\varphi$. It
is easy to see that $\varphi\equiv\varphi^{\prime}$.

We now show that as soon as we have at least two observations, the
observation-change operator adds expressivity. We first consider the mono-
agent case.

pt$s_{0}$$\neg p\leavevmode\nobreak\ $ptpt$s_{2}$$\neg p$$s_{1}$$\neg
p$$s_{3}$$\neg p$$s_{5}$$p$$s_{4}$$\neg p$$s_{6}$$\neg
p$ptptptptptptptptptpt$\sim_{o_{1},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}o_{2}}}$pt$\sim_{o_{1}}$pt$\sim_{o_{2}}$pt$\sim_{o_{2},o_{1}}$
Figure 4. Model $M^{\prime}$ in the proof of Proposition 7.5

######  Proposition 7.5.

If $|\mathcal{O}|>1$ then
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta\not\preceq\textnormal{{CTL}}^{*}\textnormal{K}$.

######  Proof 7.6.

Assume that $\mathcal{O}$ contains $o_{1}$ and $o_{2}$. Consider the model $M$
from Example 2.11 (Figure 1), and define the model $M^{\prime}$ which is the
same as $M$ except that $s_{4}$ and $s_{5}$ are indistinguishable for both
$o_{1}$ and $o_{2}$, while in $M$ they are only indistinguishable for $o_{1}$
(see Figure 4). In both models, agent $a$ is initially assigned observation
$o_{1}$. We exhibit a formula of $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$
that can distinguish between $M$ and $M^{\prime}$, and justify that no formula
of $\textnormal{{CTL}}^{*}\textnormal{K}$ can, which shows that
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta\not\preceq\textnormal{{CTL}}^{*}\textnormal{K}$.

Consider formula $\varphi=\mathit{E}F\Delta^{o_{2}}\mathit{K}_{a}p$. With a
reasoning similar to that detailed in Example 2.11, we can show that
$M\models\varphi$. We now show that $M^{\prime}\not\models\varphi$: The only
history in which agent $a$ may get to know that $p$ holds is the path
$s_{0}s_{2}s_{5}$, since in other histories $p$ does not hold. After observing
this path with observation $o_{1}$, agent $a$ considers that both $s_{4}$ and
$s_{5}$ are possible. She still does after switching to observation $o_{2}$,
as $s_{4}$ and $s_{5}$ are $o_{2}$-indistinguishable. As a result
$M^{\prime}\not\models\varphi$, and thus $\varphi$ distinguishes $M$ and
$M^{\prime}$.

Now to see that no formula of $\textnormal{{CTL}}^{*}\textnormal{K}$ can
distinguish between these two models, it is enough to see that in both models
the only agent $a$ is assigned observation $o_{1}$, and thus on these models
no operator of $\textnormal{{CTL}}^{*}\textnormal{K}$ can refer to observation
$o_{2}$, which is the only difference between $M$ and $M^{\prime}$.

This proof for the mono-agent case relies on the fact that
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ can refer to observations that
are not initially assigned to any agent, and thus cannot be referred to within
$\textnormal{{CTL}}^{*}\textnormal{K}$. The same proof can be easily adapted
to the multi-agent case, by considering the same models $M$ and $M^{\prime}$
and assigning the same initial observation $o_{1}$ to all agents. We show that
in fact, when we have at least two agents,
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ is strictly more expressive
than $\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ even when we only consider
models in which all observations are initially assigned to some agent.

######  Proposition 7.7.

If $|\mathcal{O}|>1$ and $m\geq 2$, it holds that
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}\not\preceq\textnormal{{CTL}}^{*}\textnormal{K}_{m}$
even when restricted to models where all observations are initially assigned.

######  Proof 7.8.

Assume that $\mathcal{O}$ contains $o_{1}$ and $o_{2}$. We consider the case
of two agents $a$ and $b$ ($m=2$); the proof can easily be generalised to more
agents. Consider again the models $M$ and $M^{\prime}$ used in the proof of
Proposition 7.5. This time, in both models, agent $a$ is initially assigned
observation $o_{1}$ and agent $b$ observation $o_{2}$. For the same reasons as
before, formula $\varphi=\mathit{E}F\Delta^{o_{2}}\mathit{K}_{a}p$
distinguishes between $M$ and $M^{\prime}$.

Now to see that no formula of $\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ can
distinguish these two models, recall that the only difference between $M$ and
$M^{\prime}$ concerns observation $o_{2}$, and that agents $a$ and $b$ are
bound to observations $o_{1}$ and $o_{2}$ respectively. Since in
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ agents cannot change observation,
the modification of $o_{2}$ between $M$ and $M^{\prime}$ can only affect the
knowledge of agent $b$, by letting her consider in $M^{\prime}$ that history
$s_{0}s_{1}s_{4}$ is indistinguishable to history $s_{0}s_{2}s_{5}$. However
this is not the case: indeed, $s_{1}$ and $s_{2}$ are not
$o_{2}$-indistinguishable, and because we consider perfect recall,
$s_{0}s_{1}s_{4}$ and $s_{0}s_{2}s_{5}$ are not $o_{2}$-indistinguishable
neither, even though $s_{4}$ and $s_{5}$ are.

More formally, define the _perfect-recall unfolding_ of a model $M$ as the
infinite tree consisting of all possible histories starting in the initial
state, in which two nodes $h$ and $h^{\prime}$ are related for $o_{i}$ if
$|h|=|h^{\prime}|$ and for all $i<|h|$, $h_{i}\sim_{o_{i}}h^{\prime}_{i}$. By
its semantics it is clear that $\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ is
invariant under perfect-recall unfolding. Now it suffices to notice that the
perfect-recall unfoldings of $M$ and $M^{\prime}$ are the same, and thus
cannot be distinguished by any $\textnormal{{CTL}}^{*}\textnormal{K}_{m}$
formula.

######  Remark 7.9.

Unlike $\textnormal{{CTL}}^{*}\textnormal{K}_{m}$,
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$ is not invariant under the
perfect-recall unfoldings considered in the proof of Proposition 7.7. The
reason is that in these unfoldings, observation relations on histories are
defined for fixed observations, and therefore cannot account for observation
changes induced by operators $\Delta^{o}_{a}$.

Putting together Propositions 7.1, 7.5 and 7.7, we obtain:

######  Theorem 7.10.

If $|\mathcal{O}|>1$ then
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}\prec\textnormal{{CTL}}^{*}\textnormal{K}\Delta_{m}$.

##  8\. Eliminating observation change

In this section we show how to reduce the model-checking problem for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ to that of
$\textnormal{{CTL}}^{*}\textnormal{K}$. The approach can be easily generalised
to the multi-agent case.

Fix an instance $(M,\Phi)$ of the model-checking problem for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$, where $M$ is a (mono-agent)
model and $\Phi$ is a $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ formula. We
build an equivalent instance $(M^{\prime},\Phi^{\prime})$ of the model-
checking problem for $\textnormal{{CTL}}^{*}\textnormal{K}$; in particular,
$M^{\prime}$ contains a single observation relation, and $\Phi^{\prime}$ does
not use the observation-change operator $\Delta^{o}$.

Assume that
$M=(\textnormal{AP},S,T,V,\\{\sim_{o}\\}_{o\in\mathcal{O}},{{s}^{\iota}},o^{\iota})$.
We first define the model $M^{\prime}$. For each observation symbol
$o\in\mathcal{O}$ we create a copy $M_{o}$ of the original model $M$. Moving
to copy $M_{o}$ will simulate switching to observation $o$. To make this
possible, we need to introduce transitions between each state $s_{o}$ of a
copy $M_{o}$ to state $s_{o^{\prime}}$ of copy $M_{o^{\prime}}$, for all
$o\neq o^{\prime}$.

Let $M^{\prime}=(\textnormal{AP}\cup\\{p_{o}\mid
o\in\mathcal{O}\\},S^{\prime},T^{\prime},V^{\prime},\sim^{\prime},{{s}^{\iota}}^{\prime})$,
where

  * •

for each $o\in\mathcal{O}$, $p_{o}$ is a fresh atomic proposition,

  * •

$S^{\prime}=\bigcup_{o\in\mathcal{O}}\\{s_{o}\mid s\in S\\}$,

  * •

$T^{\prime}=\\{(s_{o},s^{\prime}_{o})\mid o\in\mathcal{O}\text{ and
}(s,s^{\prime})\in T\\}$

$\cup\;\\{(s_{o},s_{o^{\prime}})\mid s\in S,o,o^{\prime}\in\mathcal{O}\text{
and }o\neq o^{\prime}\\}$

  * •

$V^{\prime}(s_{o})=V(s)\cup\\{p_{o}\\}$, for all $s\in S$ and
$o\in\mathcal{O}$,

  * •

$\sim^{\prime}=\bigcup_{o\in\mathcal{O}}\\{(s_{o},s^{\prime}_{o})\mid
s\sim_{o}s^{\prime}\\}$, and

  * •

${{s}^{\iota}}^{\prime}={{s}^{\iota}}_{o^{\iota}}$.

We now define formula $\Phi^{\prime}$. The transformation $\text{tr}^{o}$ is
parameterised with an observation $o\in\mathcal{O}$ and is defined by
induction on $\Phi$ as follows:

$\displaystyle\text{tr}^{o}(\Delta^{o^{\prime}}\varphi)$
$\displaystyle=\begin{cases}\text{tr}^{o^{\prime}}(\varphi)&\text{if
}o=o^{\prime}\\\
\mathit{A}\mathit{X}(p_{o^{\prime}}\rightarrow\text{tr}^{o^{\prime}}(\varphi))&\text{otherwise}\end{cases}$
$\displaystyle\text{tr}^{o}(\mathit{A}\psi)$
$\displaystyle=\mathit{A}(\mathit{G}p_{o}\to\text{tr}^{o}(\psi))$

All other cases simply distribute over operators. We finally let
$\Phi^{\prime}=\text{tr}^{o^{\iota}}(\Phi)$.

Using the alternative semantics it is rather easy to see that the following
holds:

######  Lemma 8.1.

$M\models\Phi$ if, and only if, $M^{\prime}\models\Phi^{\prime}$.

This establishes the correctness of the reduction, and because we know how to
model-check $\textnormal{{CTL}}^{*}\textnormal{K}$, provides a model-checking
procedure for $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$. However this
algorithm does not provide optimal complexity. Indeed, the model $M^{\prime}$
is of size $|M|\times|\mathcal{O}|$, and the best known model-checking
algorithm for $\textnormal{{CTL}}^{*}\textnormal{K}$ runs in time exponential
in the size of the model and the size of the formula [8]. Going through this
reduction thus yields a procedure that is exponential in the number of
observations. Our direct model-checking procedure, which generalises
techniques used for the classic case of static observations, provides instead
a decision procedure which is only polynomial in the number of observations
(Theorem 4.1).

The reduction described above can be easily generalised to the multi-agent
case, by creating one copy $M_{\bm{o}}$ of the original model $M$ for each
possible assignment $\bm{o}$ of observations to agents. We thus get a model
$M^{\prime}$ of size $|M|\times{|\mathcal{O}|^{|\mathit{Ag}|}}$, and since the
best known model-checking procedure for
$\textnormal{{CTL}}^{*}\textnormal{K}_{m}$ is $k$-exponential in the size of
the model [8], this reduction provides a procedure which is $k$-exponential in
the number of observations and $k+1$-exponential in the number of agents. The
direct approach provides an algorithm that is only polynomial in the number of
observations, exponential in the number of agents, and whose combined
complexity is $k$-exponential time (Theorem 6.1).

##  9\. Conclusion and future work

Epistemic temporal logics play a central role in MAS as they permit to
describe in an elegant way the knowledge of agents along the evolution of a
system. Previous works in this field have treated agents’ observation power as
a static feature. However, in many real life scenarios, agents’ observation
power may change along computations.

In this work we introduced $\textnormal{{CTL}}^{*}\textnormal{K}\Delta$, a
logic that can express such dynamic changes of observation power, and we
demonstrated how this can be used to express relevant properties in practical
scenarios. We studied the model checking of
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$ over both mono- and multi-agent
systems and proved that in both cases, the ability to express observation
changes comes at no complexity cost, but strictly increases expressivity. We
also showed how to reduce the model-checking problem for our logic to that of
$\textnormal{{CTL}}^{*}\textnormal{K}$, removing the observation-change
operator. This provides a model-checking procedure for
$\textnormal{{CTL}}^{*}\textnormal{K}\Delta$, but given the complexity of the
best-known model-checking algorithm for
$\textnormal{{CTL}}^{*}\textnormal{K}$, this procedure is not as efficient as
the direct algorithm we provide.

As future work, we plan to build upon the techniques developed here to
investigate epistemic extensions of strategic logics with imperfect
information. Several such logics have been defined and studied recently [2, 5,
6, 3, 4], and [6] in particular already presents the feature of dynamic
observation change via change of strategy. We believe that the present work
will help to establish new results on the model checking of such logics.

## References

  * [1] Guillaume Aucher.  Supervisory control theory in epistemic temporal logic.  In AAMAS, pages 333–340, 2014.  URL: http://dl.acm.org/citation.cfm?id=2615787.
  * [2] Francesco Belardinelli.  A logic of knowledge and strategies with imperfect information.  In LAMAS, pages 1–15, 2015.
  * [3] Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, and Sasha Rubin.  Verification of broadcasting multi-agent systems against an epistemic strategy logic.  In IJCAI, pages 91–97, 2017.
  * [4] Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, and Sasha Rubin.  Verification of multi-agent systems with imperfect information and public actions.  In AAMAS, pages 1268–1276, 2017.
  * [5] Raphaël Berthon, Bastien Maubert, and Aniello Murano.  Decidability results for ATL* with imperfect information and perfect recall.  In AAMAS, pages 1250–1258, 2017.
  * [6] Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, and Moshe Y. Vardi.  Strategy logic with imperfect information.  In LICS, pages 1–12, 2017.  URL: https://doi.org/10.1109/LICS.2017.8005136, doi:10.1109/LICS.2017.8005136.
  * [7] Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, and Xavier Olive.  Symbolic synthesis of observability requirements for diagnosability.  In AAAI, 2012.
  * [8] Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat.  Uniform strategies, rational relations and jumping automata.  Information and Computation, 242:80 – 107, 2015.  URL: http://www.sciencedirect.com/science/article/pii/S0890540115000279, doi:https://doi.org/10.1016/j.ic.2015.03.012.
  * [9] Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat.  Unifying hyper and epistemic temporal logics.  In FoSSaCS, pages 167–182, 2015.  URL: https://doi.org/10.1007/978-3-662-46678-0_11, doi:10.1007/978-3-662-46678-0_11.
  * [10] Cătălin Dima.  Revisiting satisfiability and model-checking for ctlk with synchrony and perfect recall.  In CLIMA IX-2008, pages 117–131, 2009.  URL: https://doi.org/10.1007/978-3-642-02734-5_8, doi:10.1007/978-3-642-02734-5_8.
  * [11] E Allen Emerson and Chin-Laung Lei.  Modalities for model checking: Branching time logic strikes back.  Science of computer programming, 8(3):275–306, 1987.
  * [12] Ronald Fagin, Joseph Y Halpern, Yoram Moses, and Moshe Vardi.  Reasoning about knowledge.  MIT press, 2004.
  * [13] Joseph Y. Halpern and Kevin R. O’Neill.  Anonymity and information hiding in multiagent systems.  Journal of Computer Security, 13(3):483–512, 2005.  URL: http://content.iospress.com/articles/journal-of-computer-security/jcs237.
  * [14] Joseph Y. Halpern, Ron van der Meyden, and Moshe Y. Vardi.  Complete axiomatizations for reasoning about knowledge and time.  SIAM J. Comput., 33(3):674–703, 2004.  URL: https://doi.org/10.1137/S0097539797320906, doi:10.1137/S0097539797320906.
  * [15] Wojciech Jamroga and Masoud Tabatabaei.  Accumulative knowledge under bounded resources.  J. Log. Comput., 28(3):581–604, 2018.  URL: https://doi.org/10.1093/logcom/exv003, doi:10.1093/logcom/exv003.
  * [16] Jeremy Kong and Alessio Lomuscio.  Symbolic model checking multi-agent systems against CTL*K specifications.  In AAMAS, pages 114–122, 2017.  URL: http://dl.acm.org/citation.cfm?id=3091147.
  * [17] Orna Kupferman, Moshe Y Vardi, and Pierre Wolper.  An automata-theoretic approach to branching-time model checking.  Journal of the ACM (JACM), 47(2):312–360, 2000.
  * [18] Richard E. Ladner and John H. Reif.  The logic of distributed protocols.  In TARK, pages 207–222, 1986.
  * [19] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi.  Reasoning about strategies: On the model-checking problem.  ACM Trans. Comput. Log., 15(4):34:1–34:47, 2014.  URL: http://doi.acm.org/10.1145/2631917, doi:10.1145/2631917.
  * [20] Eric Pacuit.  Some comments on history based structures.  Journal of Applied Logic, 5(4):613–624, 2007.
  * [21] Franco Raimondi and Alessio Lomuscio.  The complexity of symbolic model checking temporal-epistemic logics.  In CS&P, pages 421–432, 2005.
  * [22] Meera Sampath, Raja Sengupta, Stéphane Lafortune, Kasim Sinnamohideen, and Demosthenis Teneketzis.  Diagnosability of discrete-event systems.  IEEE Transactions on automatic control, 40(9):1555–1575, 1995.
  * [23] W. van der Hoek and M. Wooldridge.  Cooperation, knowledge, and time: Alternating-time Temporal Epistemic Logic and its applications.  Studia Logica, 75(1):125–157, 2003.  doi:10.1023/A:1026185103185.
  * [24] Ron van der Meyden.  Common knowledge and update in finite environments.  Inf. Comput., 140(2):115–157, 1998.  URL: https://doi.org/10.1006/inco.1997.2679, doi:10.1006/inco.1997.2679.
  * [25] Ron van der Meyden and Nikolay V. Shilov.  Model checking knowledge and time in systems with perfect recall (extended abstract).  In FSTTCS, pages 432–445, 1999.
  * [26] Ron van der Meyden and Kaile Su.  Symbolic model checking the knowledge of the dining cryptographers.  In CSFW-17, pages 280–291, 2004.
  * [27] Ron van der Meyden and Moshe Y Vardi.  Synthesis from knowledge-based specifications.  In CONCUR, pages 34–49. Springer, 1998.
  * [28] Hans van Ditmarsch, Wiebe Van der Hoek, and Barteld Pieter Kooi.  Dynamic epistemic logic, volume 337.  Springer, 2007.
  * [29] John Von Neumann and Oskar Morgenstern.  Theory of games and economic behavior (commemorative edition).  Princeton university press, 2007.

##  Appendix A Proof of Theorem 3.5

Theorem 3.5 directly follows from the following lemma:

######  Lemma A.1.

For every history formula $\varphi$, model $M$, history $h$ and observation
record $r$ that stops at $h$,

$h,r\models\varphi\quad\mbox{iff}\quad\mbox{last}(h),I(h,r),O(h,r)\models_{I}\varphi$

and for every path formula $\psi$, every path $\pi$, point in time
$n\in\mathbb{N}$ and observation record $r$ that stops at $n$,

$\pi,n,r\models\psi\quad\mbox{iff}\quad\pi_{\geq n},I(\pi_{\leq
n},r),O(\pi_{\leq n},r)\models_{I}\psi.$

######  Proof A.2.

We prove the result by mutual induction on $\varphi$ and $\psi$. Let $M$ be a
model, $h$ a history and $r$ an observation record that stops at $h$.

$\bm{\varphi=p}$: We have $h,r\models p\quad\mbox{iff}\quad p\in
V(\mbox{last}(h))\quad\mbox{iff}\quad\mbox{last}(h),I(h,r),O(h,r)\models_{I}p$,
by applying the definitions.

$\bm{\varphi=\neg\varphi^{\prime}}$ and
$\bm{\varphi=\varphi_{1}\wedge\varphi_{2}}$: Simple application of the
induction hypothesis.

$\bm{\varphi=\mathit{A}\psi}$: We start with the left-to-right implication.
Assume that $h,r\models\mathit{A}\psi$. We need to prove that for all $\pi$
such that $\pi_{0}=\mbox{last}(h)$, $\pi,I(h,r),O(h,r)\models_{I}\psi$. If
$\pi_{0}=\mbox{last}(h)$, we have $h\preccurlyeq h\cdot\pi_{>0}$; since
$h,r\models\mathit{A}\psi$ we thus get that
$h\cdot\pi_{>0},|h|-1,r\models\psi$. By induction hypothesis we have
$(h\cdot\pi_{>0})_{>|h|-1},I((h\cdot\pi_{>0})_{\leq|h|-1},r),O((h\cdot\pi_{>0})_{\leq|h|-1},r)\models_{I}\psi$,
that is to say $\pi,I(h,r),O(h,r)\models_{I}\psi$, as
$\pi_{0}=\mbox{last}(h)$.

For the other direction, assume that
$\mbox{last}(h),I(h,r),O(h,r)\models_{I}\mathit{A}\psi$, i.e., for all $\pi$
such that $\pi_{0}=\mbox{last}(h)$, it holds that
$\pi,I(h,r),O(h,r)\models_{I}\psi$. Let $\pi$ be such that $h\preccurlyeq\pi$;
we prove that $\pi,|h|-1,r\models\psi$. Because $h\preccurlyeq\pi$, we have
that $(\pi_{\geq|h|-1})_{0}=\mbox{last}(h)$. By assumption, it follows that
$\pi_{\geq|h|-1},I(h,r),O(h,r)\models_{I}\psi$, that is
$\pi_{\geq|h|-1},I(\pi_{\leq|h|-1},r),O(\pi_{\leq|h|-1},r)\models_{I}\psi$.
Then by induction hypothesis we finally get that $\pi,|h|-1,r\models\psi$.

$\bm{\varphi=\mathit{K}\varphi^{\prime}:}$ For the first direction, assume
that $h,r\models\mathit{K}\varphi^{\prime}$, i.e., for all
$h^{\prime}\approx^{r}h$, we have $h^{\prime},r\models\varphi$. We prove that
$\mbox{last}(h),I(h,r),O(h,r)\models_{I}\mathit{K}\varphi^{\prime}$, i.e., for
all $s^{\prime}\in I(h,r)$,
$s^{\prime},I(h,r),O(h,r)\models_{I}\varphi^{\prime}$. Let $s^{\prime}\in
I(h,r)$. By definition of the information set, there exists
$h^{\prime}\approx^{r}h$ such that $h^{\prime}\approx^{r}h$ and
$\mbox{last}(h^{\prime})=s^{\prime}$. By assumption,
$h^{\prime},r\models\varphi$, and by induction hypothesis,
$\mbox{last}(h^{\prime}),I(h^{\prime},r),O(h^{\prime},r)\models_{I}\varphi$.
Because $h^{\prime}\approx^{r}h$, $I(h,r)=I(h^{\prime},r)$ and
$O(h,r)=O(h^{\prime},r)$. It follows that
$s^{\prime},I(h,r),O(h,r)\models_{I}\varphi$.

For the other direction, we assume that for all $s^{\prime}\in
I(h,r),s^{\prime},I(h,r),O(h,r)\models_{I}\varphi^{\prime}$, and we prove that
$h,r\models\mathit{K}\varphi^{\prime}$, i.e., for all
$h^{\prime}\approx^{r}h$, $h^{\prime},r\models\varphi^{\prime}$. Let
$h^{\prime}$ be such that $h^{\prime}\approx^{r}h$. By definition,
$\mbox{last}(h^{\prime})\in I(h,r)$. By assymption,
$\mbox{last}(h^{\prime}),I(h,r),O(h,r)\models_{I}\varphi^{\prime}$. Because
$h^{\prime}\approx^{r}h$, $I(h,r)=I(h^{\prime},r)$ and
$O(h,r)=O(h^{\prime},r)$, and we get that
$\mbox{last}(h^{\prime}),I(h^{\prime},r),O(h^{\prime},r)\models_{I}\varphi^{\prime}$.
By induction hypothesis, $h^{\prime},r\models\varphi^{\prime}$.

$\bm{\varphi=\Delta^{o}\varphi^{\prime}}$: By definition,
$h,r\models\Delta^{o}\varphi\quad\mbox{iff}\quad h,r.(o,|h|-1)\models\varphi$.
By induction hypothesis,
$h,r.(o,|h|-1)\models\varphi\quad\mbox{iff}\quad\mbox{last}(h),I(h,r.(o,|h|-1)),O(h,r.(o,|h|-1))\models_{I}\varphi$.
By Proposition 3.3, because $r$ stops at $|h|-1$, this is equivalent to
$\mbox{last}(h),U_{\Delta}(I(h,r),o),o\models_{I}\varphi$, which by definition
is equivalent to $\mbox{last}(h),I(h,r),O(h,r)\models_{I}\Delta^{o}\varphi$.

Let $\pi$ be a path, $n$ a natural number and $r$ an observation record that
stops at $n$.

$\bm{\psi=\varphi}$: By definition,
$\pi,n,r\models\varphi\quad\mbox{iff}\quad\pi_{\leq n},r\models\varphi$. By
induction hypothesis, the latter is equivalent to $\mbox{last}(\pi_{\leq
n}),I(\pi_{\leq n},r),O(\pi_{\leq n},r)\models_{I}\varphi$. Because
$(\pi_{\geq n})_{0}=\mbox{last}(\pi_{\leq n})$, by definition this is also
equivalent to $\pi_{\geq n},I(\pi_{\leq n},r),O(\pi_{\leq
n},r)\models_{I}\varphi$, which concludes.

$\bm{\psi=\neg\psi^{\prime}}$ and $\bm{\psi=\psi_{1}\wedge\psi_{2}}$: By
application of the induction hypothesis.

$\bm{\psi=\mathit{X}\psi^{\prime}}$: By definition,
$\pi,n,r\models\mathit{X}\psi^{\prime}\quad\mbox{iff}\quad\pi,n+1,r\models\psi^{\prime}$.
By induction hypothesis we get

$\pi,n,r\models\mathit{X}\psi^{\prime}\quad\mbox{iff}\quad\pi_{\geq(n+1)},I(\pi_{\leq(n+1)},r),O(\pi_{\leq(n+1)},r)\models_{I}\psi^{\prime}.$
(1)

Because $r$ stops at $n$, we have that $O(\pi_{\leq(n+1)},r)=O(\pi_{\leq
n},r)$. Using Proposition 3.3, we also have that
$I(\pi_{\leq(n+1)},r)=U_{T}(I(\pi_{\leq n},r),\pi_{n+1},O(\pi_{\leq n},r))$.
(1) thus becomes

$\pi,n,r\models\mathit{X}\psi^{\prime}\quad\mbox{iff}\quad\pi_{\geq(n+1)},U_{T}(I(\pi_{\leq
n},r),\pi_{n+1},O(\pi_{\leq n},r)),O(\pi_{\leq n},r)\models_{I}\psi^{\prime}.$
(2)

Because $\pi_{(n+1)}=(\pi_{\geq n})_{1}$, by definition we finally get that

$\pi,n,r\models\mathit{X}\psi\quad\mbox{iff}\quad\pi_{\geq n},I(\pi_{\leq
n},r),O(\pi_{\leq n},r)\models_{I}\mathit{X}\psi^{\prime}.$

$\bm{\psi=\psi_{1}\mathit{U}\psi_{2}}$: According to the definitions, it
suffices to prove that for all path $k\geq 0$ and
$\psi\in\\{\psi_{1},\psi_{2}\\}$,
$\pi,n+k,r\models\psi\quad\mbox{iff}\quad\pi_{\geq(n+k)},U_{T}^{k}(I(\pi_{\leq
n},r),\pi_{\geq n},O(\pi_{\leq n},r)),O(\pi_{\leq n},r)\models_{I}\psi$. This
can be proven by induction on $k$, using for the inductive step a reasoning
similar to that for $\psi=\mathit{X}\psi^{\prime}$.

##  Appendix B Proof of Proposition 5.5

######  Proposition B.5.

For every history $h\cdot s$, record tuple $\bm{r}$ that stops at $h$,
observation tuple $\bm{o}$ and integer $k$, it holds that

$\begin{array}[]{rcl}I^{k}(h\cdot
s,\bm{r})&=&U_{T}^{k}(I^{k}(h,\bm{r}),s,\bm{o}(h,\bm{r})),\mbox{ and}\\\
I^{k}(h,\bm{r}\cdot(o,|h|-1)_{a})&=&U_{\Delta}^{k}(I^{k}(h,\bm{r}),o,a).\end{array}$

######  Proof B.6.

The proof is by induction on $k$.

$\bm{k=0}$: the result is immediate from the definitions.

$\bm{k+1}$: We start with the first part of the proposition.

By definition $I^{k+1}(h\cdot s,\bm{r})=\langle
s,\mathcal{I}_{1},\ldots,\mathcal{I}_{m}\rangle$, where for each $i$,

$\mathcal{I}_{i}=\\{I^{k}(h^{\prime}\cdot s^{\prime},\bm{r})\mid
h^{\prime}\cdot s^{\prime}\approx^{\bm{r}}_{a_{i}}h\cdot s\\}.$

On the other hand, letting
$I^{k+1}(h,\bm{r})=\langle\mbox{last}(h),\mathcal{I}^{\prime}_{1},\ldots,\mathcal{I}^{\prime}_{m}\rangle$
and $\bm{o}=\bm{o}(h,\bm{r})$, we have by definition that
$U_{T}^{k+1}(I^{k+1}(h,\bm{r}),s,\bm{o})=\langle
s,\mathcal{I}^{\prime\prime}_{1},\ldots,\mathcal{I}^{\prime\prime}_{m}\rangle$,
where for each $i$,

$\mathcal{I}^{\prime\prime}_{i}=\\{U_{T}^{k}(I^{k},s^{\prime},\bm{o})\mid
I^{k}\in\mathcal{I}^{\prime}_{i}\mbox{, }s^{\prime}\sim_{\bm{o}_{i}}s\mbox{
and }r(I^{k})Ts^{\prime}\\}.$

It thus suffices to show that for each $i$,
$\mathcal{I}_{i}=\mathcal{I}^{\prime\prime}_{i}$. Observe that because
$\bm{r}$ stops at $h$, $h^{\prime}\cdot
s^{\prime}\approx^{\bm{r}}_{a_{i}}h\cdot s$ iff
$h^{\prime}\approx^{\bm{r}}_{a_{i}}h$ and $s^{\prime}\sim_{\bm{o}_{i}}s$. We
thus have that

$\mathcal{I}_{i}=\\{I^{k}(h^{\prime}\cdot s^{\prime},\bm{r})\mid
h^{\prime}\approx^{\bm{r}}_{a_{i}}h,\;s^{\prime}\sim_{\bm{o}_{i}}s\mbox{ and
}\mbox{last}(h^{\prime})Ts^{\prime}\\}.$

By induction hypothesis, this becomes

$\mathcal{I}_{i}=\\{U_{T}^{k}(I^{k}(h^{\prime},\bm{r}),s^{\prime},\bm{o}(h^{\prime},\bm{r}))\mid
h^{\prime}\approx^{\bm{r}}_{a_{i}}h,\;s^{\prime}\sim_{\bm{o}_{i}}s\mbox{ and
}\mbox{last}(h^{\prime})Ts^{\prime}\\}.$

For each $h^{\prime}\approx^{\bm{r}}_{a_{i}}h$, we have that
$\bm{o}(h^{\prime},\bm{r})=\bm{o}(h,\bm{r})=\bm{o}$.

It remains to observe that by definition, for each $i$,
$\mathcal{I}^{\prime}_{i}=\\{I^{k}(h^{\prime},\bm{r})\mid
h^{\prime}\approx^{\bm{r}}_{a_{i}}h\\}$, and we get that
$\mathcal{I}_{i}=\mathcal{I}^{\prime\prime}_{i}$, which concludes the first
part of the proposition.

We now prove the second part of the proposition, assuming that $a=a_{j}$.

By definition
$I^{k+1}(h,\bm{r}\cdot(o,|h|-1)_{a_{j}})=\langle\mbox{last}(h),\mathcal{I}_{1},\ldots,\mathcal{I}_{m}\rangle$,
where for each $i$,

$\mathcal{I}_{i}=\\{I^{k}(h^{\prime},\bm{r}\cdot(o,|h|-1)_{a_{j}})\mid
h^{\prime}\approx^{\bm{r}\cdot(o,|h|-1)_{a_{j}}}_{a_{i}}h\\}.$

On the other hand, letting
$I^{k+1}(h,\bm{r})=\langle\mbox{last}(h),\mathcal{I}^{\prime}_{1},\ldots,\mathcal{I}^{\prime}_{m}\rangle$,
we have by definition that
$U_{\Delta}^{k+1}(I^{k+1}(h,\bm{r}),o,a_{j})=\langle\mbox{last}(h),\mathcal{I}^{\prime\prime}_{1},\ldots,\mathcal{I}^{\prime\prime}_{m}\rangle$,
where for each $i\neq j$,

$\mathcal{I}^{\prime\prime}_{i}=\\{U_{\Delta}^{k}(I^{k},o,a_{j})\mid
I^{k}\in\mathcal{I}^{\prime}_{i}\\},\mbox{ and}$
$\mathcal{I}^{\prime\prime}_{j}=\\{U_{\Delta}^{k}(I^{k},o,a_{j})\mid
I^{k}\in\mathcal{I}^{\prime}_{j}\mbox{ and
}r(I^{k})\sim_{o}\mbox{last}(h)\\}.$

We now show that for all $i$,
$\mathcal{I}_{i}=\mathcal{I}^{\prime\prime}_{i}$.

First, by induction hypothesis, for each $i$ we have

$\mathcal{I}_{i}=\\{U_{\Delta}^{k}(I^{k}(h^{\prime},\bm{r}),o,a_{j})\mid
h^{\prime}\approx^{\bm{r}\cdot(o,|h|-1)_{a_{j}}}_{a_{i}}h\\}.$

Also, by definition, for each $i$ we have
$\mathcal{I}^{\prime}_{i}=\\{I^{k}(h^{\prime},\bm{r})\mid
h^{\prime}\approx^{\bm{r}}_{a_{i}}h\\}$.

Next, for $i\neq j$ we have that
$h^{\prime}\approx^{\bm{r}\cdot(o,|h|-1)_{a_{j}}}_{a_{i}}h$ iff
$h^{\prime}\approx^{\bm{r}}_{a_{i}}h$, and by definition of the perfect-recall
relation, for $i=j$, it holds that
$h^{\prime}\approx^{\bm{r}\cdot(o,|h|-1)_{a_{j}}}_{a_{i}}h$ iff
$h^{\prime}\approx^{\bm{r}}_{a_{i}}h$ and
$\mbox{last}(h^{\prime})\sim_{o}\mbox{last}(h)$. It is then easy to see that
for all $i$, $\mathcal{I}_{i}=\mathcal{I}^{\prime\prime}_{i}$, which
concludes.