# Uncertainty-Based Knowing How Logic

Carlos Areces1,2 Raul Fervari1,2,3 Andrés R. Saravia1,2 Fernando R. Velázquez-
Quesada4

(  1FAMAF, Universidad Nacional de Córdoba, Argentina
2Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET),
Argentina
3Guangdong Technion - Israel Institute of Technology (GTIIT), China
4Universitetet i Bergen, Norway )

###### Abstract

We introduce a novel semantics for a multi-agent epistemic operator of
_knowing how_ , based on an indistinguishability relation between plans. Our
proposal is, arguably, closer to the standard presentation of _knowing that_
modalities in classical epistemic logic. We study the relationship between
this new semantics and previous approaches, showing that our setting is
general enough to capture them. We also study the logical properties of the
new semantics. First, we define a sound and complete axiomatization. Second,
we define a suitable notion of bisimulation and prove correspondence theorems.
Finally, we investigate the computational complexity of the model checking and
satisfiability problems for the new logic.

##  1 Introduction

Epistemic logic (EL; [28, 13]) is a logical formalism tailored for reasoning
about the knowledge of abstract autonomous entities commonly called agents
(e.g., a human being, a robot, a vehicle). It has contributed to the formal
study of complex multi-agent epistemic notions not only in philosophy [25] but
also in computer science [13, 41] and economics [47].

Standard epistemic logics deal with an agent’s knowledge about the truth-value
of propositions (the notion of _knowing that_). Thus, they focus on the study
of sentences like _“the agent knows that it is sunny in Paris”_ or _“the robot
knows that it is standing next to a wall”_. For doing so, at the semantic
level, EL formulas are typically interpreted over relational models [9, 10]:
essentially, labeled directed graphs. The elements of the domain (called
_states_ or _worlds_) represent different possible situations, and they fix
the facts an agent might or might not know. Then, the knowledge of each agent
is given by her _epistemic indistinguishability_ relation, used to represent
her uncertainty about the truth: related states are considered
indistinguishable for the agent. Finally, an agent is said to know that a
proposition $\varphi$ is true at a given state $s$ if and only if $\varphi$
holds in all states she cannot distinguish from $s$ (i.e., in all states
accessible from $s$). In order to capture properly the properties of
knowledge, it is typically assumed that the indistinguishability relation is
an equivalence relation.

In spite of its simplicity, this indistinguishability-based representation of
knowledge has several advantages. First, it captures the agent’s _high-order_
knowledge (knowledge about her own knowledge and that of other agents).
Moreover, due to its generality, it opens the way to study other epistemic
notions, such as the notion of _belief_ [28]. Finally, it allows a very
natural representation of actions through which knowledge changes [53, 50].

In recent years, other forms of knowledge have been studied (see the
discussion in [58]). Some authors have studied knowledge of propositions using
rather the notion of _knowing whether_ [23, 14]; some others have focused in
the reasons/justifications for propositional knowledge, exploring the notion
of _knowing why_ [5, 60]; some more have looked at more general scenarios,
proposing logics for _knowing the value_ [20, 6, 54]. A further and
particularly interesting form of knowledge, motivated by different scenarios
in philosophy and AI, is one that focuses rather on the agent’s abilities: the
notion of _knowing how_ [15]. Intuitively, an agent knows how to achieve
$\varphi$ given $\psi$ if she has the _ability_ to guarantee that $\varphi$
will be the case whenever she is in a situation in which $\psi$ holds.
Arguably, this notion is particularly important as it provides the formal
foundations of automated planning and strategic reasoning within AI.

Historically, the concept of knowing how has been considered different from
knowing that, as posed e.g. in [48]. Knowing how is often seen as a reflection
of actions or abilities that agents may take, in an intelligent manner, in
order to achieve a certain goal. In turn, there is a large literature
connecting _knowing how_ with logics of knowledge and action (see, e.g., [39,
42, 31, 52, 27]). However, the way in which these proposals represent _knowing
how_ has been the target of criticisms. The main issue is that a simple
combination of standard operators expressing _knowing that_ and _ability_
(see, e.g., [51]) does not seem to lead to a natural notion of _knowing how_
(see [29, 26] for a discussion).

Taking these considerations into account, [57, 58, 59] introduced a novel
framework based on a binary _knowing how_ modality that is not defined in
terms of _knowing that_. At the semantic level, this language is also
interpreted over relational models — called in this context labeled transition
systems (LTSs). Yet, relations do not represent indistinguishability anymore;
they rather describe the actions the agent has at her disposal (similar to
what is done in, e.g., propositional dynamic logic [22]). Indeed, an edge
labeled $a$ from state $w$ to state $u$ indicates now that the agent can
execute action $a$ to transform state $w$ into $u$. In the proposed semantics,
the new modality $\mathsf{Kh}(\psi,\varphi)$ holds if and only if there is a
“plan” — a sequence of actions satisfying a constraint called strong
executability (SE) — leading from $\psi$-states to $\varphi$-states.
Intuitively, SE implies that the plan is “fail-proof” in the LTS; it
unerringly leads from every $\psi$-state only to $\varphi$-states. Other
variants of this _knowing how_ operator follow a similar approach (see [32,
34, 16, 56]). Further motivation for these semantics can be found in the
referred papers.

It is interesting to notice how LTSs have no epistemic component: their
relations are interpreted as actions, and then the abilities of an agent are
defined only in terms what these actions can achieve. This is in sharp
contrast with standard EL, where relational models provide two kinds of
information: ontic facts about the given situation (the model’s evaluation
point) and the particular way an agent ‘sees’ this situation (both the
possible states available in the model and the agent’s indistinguishability
relation among them). In particular, in a multi-agent scenario, all agents
share the same ontic information, and differ on their _epistemic
interpretation_ of it. If one wants to mirror the situation in EL, it seems
natural that _knowing how_ should be defined in terms of some kind of
indistinguishability over the actual situation. Such an extended model would
then be able to capture both the abilities of an agent as given by her
available actions (the ontic information) as well as the knowledge (or lack of
it) that arises from her uncertainty (the epistemic information).

This paper investigates a new semantics for
$\mathsf{Kh}_{\\_}i(\psi,\varphi)$, a multi-agent version of the _knowing how_
modality, first presented in [3]. These semantics introduces two ideas. The
first, the crucial, is the use of a notion of _epistemic indistinguishability
over plans_ , in the spirit of the _strategy indistinguishability_ of, e.g.,
[30, 8]. The intuition behind it is that, under the original $\mathrm{LTS}$
semantics, the only reason why an agent might not know how to achieve a goal
is because there is no adequate action available. However, one can think of
scenarios in which the lack of knowledge arises for a different reason: the
agent might have an adequate plan available (she has the ability to do
something), and yet she might not be able to distinguish it from a non-
adequate one, in the sense of not being able to tell that, in general, these
plans produce different outcomes. Section 4 provides a deeper discussion on
this. In this way, these _uncertainty-based_ ${\mathrm{LTS}}s$ reintroduce the
notion of epistemic indistinguishability.

Now, although indistinguishability over plans is the main idea behind the new
semantics, this proposal incorporates a second insight. One can also think of
scenarios in which some of the actions, despite being _ontically_ available,
are not _epistemically_ accessible to the agent. There might be several
reasons for this, but an appealing one is that the agent might not be _aware
of_ all available actions. In such cases, the epistemically inaccessible
actions are then not even under consideration when the agent looks for a plan
to reach a goal. The idea of awareness is not new in the EL literature: it has
been used for dealing with the EL problem of logical omniscience [55, 49, 21]
by allowing the agent not to be aware of all involved atoms/formulas, thus
bringing it closer to what a ‘real’ resource-bounded agent is (see [12]).

Notice that, the ideas discussed above are in line with a reading that has a
consensus among the literature (see, e.g., [24]): knowing how of an agent
entails her ability (i.e., the capacity of actually doing it); but ability
does not necessarily entail knowing how. It is equally important to notice
that, in the new semantics, the agent does not _need_ to be incapable of
distinguishing certain actions, and she does not _need_ to be unaware of some
of them. As it will be proved, the new semantics are a generalisation of the
original ones in [57, 59]. Thus, an agent in the new semantics who does not
have uncertainty among plans and has full awareness of all of them is,
knowledge-wise, exactly as an agent in the original semantics.

#### Our contributions.

Our work aims to shed new light on knowing how logics. In particular, we
investigate a new multi-agent semantics for capturing the notion of knowing
how, generalizing previous proposals [57, 58, 59, 3]. Herein, we establish a
distinction between ontic information shared by the agents (or abilities), and
epistemic information for each individual agent (or awareness), at the level
of models. In our semantics, knowing how is given by the latter, instead of by
the former, as in existing approaches [57, 58, 59]. Moreover, we present a
thorough study of the metalogical properties of the new logic, and compare it
with previous approaches. Our contributions can be summarized as follows:

  1. (1)

We introduce a new semantics for $\mathsf{Kh}_{\\_}i(\psi,\varphi)$ (for $i$
an agent) that reintroduces the notion of epistemic indistinguishability from
classical EL. This dimension captures the awareness for each particular agent
over the available abilities in the real world.

  2. (2)

We introduce a suitable notion of bisimulation for the new semantics, based on
ideas from [17, 18]. We prove an invariance result, and a Hennessy-Milner
style theorem over finite models.

  3. (3)

We show that the logic obtained is strictly weaker (and this is an advantage,
as we will discuss) than the logic from [57, 58, 59]. Still, the new semantics
is general enough to capture the original proposal by imposing adequate
conditions on the class of models. Apart from the direct correspondence
between models of each framework established already in [3], we introduce a
new general class of models that also does the job.

  4. (4)

We present a sound and complete axiomatization for the logic over the class of
all models.

  5. (5)

We study the computational properties of our logic. First, we provide a finite
model property via filtrations. I.e., we show how, given an arbitrary model,
it is possible to obtain a finite model satisfying the same set of formulas. A
more careful selection argument can be used to prove that the satisfiability
problem for the new logic is NP-complete, whereas model checking is in P.

This paper extends the work presented in [3]. Herein, we provide detailed
discussions and motivations, and full proofs. Moreover, the results about
bisimulations, expressive power and finite models via filtrations, are novel
with respect to [3].

#### Outline of the article.

Section 3 recalls the framework of [57, 58, 59], including its axiom system.
Section 4 introduces _uncertainty-based LTSs_ , indicating how they can be
used for interpreting a multi-agent version of the _knowing how_ language. In
Section 5 we introduce a suitable notion of bisimulation, together with
correspondence theorems. We provide a sound and complete axiom system in
Section 6. Section 7 studies the correspondence between our semantics and the
one in the original proposals. In particular, we present two different classes
of models that capture the original semantics. In Section 8 we investigate a
finite model property via filtrations (Subsection 8.1), and the computational
complexity of model checking and the satisfiability problem for our logic
(Subsection 8.2). We conclude in Section 9 with some conclusions and future
lines of research.

##  2 A short review of the literature

The ideas discussed in the previous section concerning the notion of _knowing
how_ introduced in [57, 58, 59] have been successful, and have lead to
different works in the literature. An earlier one is [34], which considers a
ternary modality $\mathsf{Kh}(\psi,\chi,\varphi)$ asking for a plan whose
intermediate states satisfy $\chi$. Then, [32] introduces a weaker binary
modality $\mathsf{Kh}^{\sf w}(\psi,\varphi)$ that allows plans that abort, and
in which the states reached by these aborted executions should also satisfy
the goal $\varphi$. Finally, [56] uses a semantics under which intermediate
actions in a given plan may be skipped.

The respective works introducing these variants also provide an axiom system
(interestingly, the logic for the modality with skippable plans is the same as
the logic for the original modality). Regarding computational behaviour, the
satisfiability problem has been proved to be decidable (in their respective
papers) for the basic system, the one allowing aborted executions and the one
with skippable plans. However, no complexity bounds for any of the systems
have been given. Finally, suitable notions of bisimulation for these systems
can be found in [17, 18] (for all but the one with skippable plans) and [56]
(for the one with skippable plans). These bisimilarity tools have been useful
to investigate the systems’ relative expressive power. It has been shown that
the original binary modality $\mathsf{Kh}(\psi,\varphi)$ is strictly less
expressive than the one with intermediate steps
($\mathsf{Kh}(\psi,\chi,\varphi)$), and that they are both incomparable with
the modality with aborted executions $\mathsf{Kh}^{\sf w}(\psi,\varphi)$.
Moreover, in [11] the computational complexity of the model-checking problem
for different knowing how logics is characterized. In particular, it is
established that model-checking for the basic knowing how logic from [57, 58,
59] is PSpace-complete, whereas for a variant with budget constraints is
ExpSpace-hard. Other constraints over plans are also studied therein,
concretely the variant of [3] (the one studied in this paper) with regularity
constraints and budgets, for which model-checking is in P. More recently, in
[2], the framework of knowing how is extended to a deontic setting,
formalizing the notion of _knowingly complying_.

Further proposals explore new features. For instance, a natural extension is
considering the interaction between _knowing how_ and standard _knowing that_
modalities. In [16], a single-agent logic with the two modalities is
introduced. The knowing how operator is, unlike previous approaches, a unary
local modality $\mathsf{Kh}(\varphi)$, and its interpretation allows branching
plans. The interaction between both kinds of knowledge is studied via an axiom
system, and it is proved that its satisfiability problem is decidable. The
decidability result has been recently refined in [33], where PSpace-
completeness is proved for the satisfiability problem, via a tableau-based
procedure. In [37] a neighbourhood semantics is provided for the _knowing how_
modality, as an alternative to the standard relational semantics.

Other papers incorporate multi-agent behaviour for _knowing how_ and _knowing
that_ modalities. For instance, in [43, 45] this is explored in the context of
coalitions, i.e., the logic is used to describe different notions of
collective knowledge. It is known that a fragment of this logic is
incomparable in expressive power with the logic from [16] (the proof uses
bisimulation, and it is presented in [18]). Other variants of this logic have
been explored, including those relying on _second-order knowing how_
strategies [44], and _knowing how_ with degrees of uncertainty [46]. Axiom
systems are presented for each logic.

Finally, a multi-agent knowing how logic describing the behaviour of epistemic
planning is investigated in [35]. The main peculiarity is that the execution
of an action is represented by an update in the model via epistemic action
models [7]. The logic obtained is strictly weaker than the one in [16]. Again,
its satisfiability problem is decidable. This work is extended in [38], which
provides a unified approach for planning-based knowing how. More remarkably,
the work in [36] establishes a connection between planning and knowing how,
not just from the perspective of _planning-based_ know how, but also the other
way around: a planning problem based on know how goals. To do so, the authors
introduce a model checking algorithm running in P time.

##  3 A logic of knowing how

This section recalls the basics of the _knowing how_ framework from [57, 58,
59].

Syntax and semantics. Throughout the text, let ${\rm\sf Prop}$ be a countable
non-empty set of propositional symbols.

######  Definition 3.1.

Formulas of the language $\mathsf{L}_{\mathsf{Kh}}$ are given by the grammar

$\varphi::=p\mid\neg\varphi\mid\varphi\vee\varphi\mid\mathsf{Kh}(\varphi,\varphi)$,

with $p\in{\rm\sf Prop}$. Boolean constants and other Boolean connectives are
defined as usual. Formulas of the form $\mathsf{Kh}(\psi,\varphi)$ are read as
_“when $\psi$ holds, the agent knows how to make $\varphi$ true”_. $\dashv$

In [57, 58, 59] (and variations like [34, 32]), formulas of
$\mathsf{L}_{\mathsf{Kh}}$ are interpreted over _labeled transition systems_ :
relational models in which the relations describe the state-transitions
available to the agent. Throughout the text, let ${\rm\sf Act}$ be a
denumerable set of (basic) action names.

######  Definition 3.2 (Actions and plans).

Let ${\rm\sf Act}^{*}$ be the set of finite sequences over ${\rm\sf Act}$.
Elements of ${\rm\sf Act}^{*}$ are called _plans_ , with $\epsilon$ being the
_empty plan_. Given $\sigma\in{\rm\sf Act}^{*}$, let $\lvert\sigma\rvert$ be
the length of $\sigma$ (note: $\lvert\epsilon\rvert:=0$). For a plan $\sigma$
and $0\leq k\leq\lvert\sigma\rvert$, the _plan_ $\sigma_{\\_}k$ is $\sigma$’s
initial segment up to (and including) the $k$th position (with
$\sigma_{\\_}0:=\epsilon$). For $0<k\leq\lvert\sigma\rvert$, the _action_
$\sigma[k]$ is the one in $\sigma$’s $k$th position. $\dashv$

######  Definition 3.3 (Labeled transition systems).

A _labeled transition system ( $\mathrm{LTS}$)_ for ${\rm\sf Prop}$ and
${\rm\sf Act}$ is a tuple
$\mathcal{S}=\langle\mathrm{W},\mathrm{R},\mathrm{V}\rangle$ where
$\mathrm{W}$ is a non-empty set of states (also denoted by
$\mathrm{D}_{\mathcal{S}}$),
$\mathrm{R}=\\{\mathrm{R}_{\\_}a\subseteq\mathrm{W}\times\mathrm{W}\mid a\in
A,\text{ for some }A\subseteq{\rm\sf Act}\\}$ is a collection of binary
relations on $\mathrm{W}$,111Thus, $\mathrm{R}_{\\_}a$ might not be defined
for some $a\in{\rm\sf Act}$. and $\mathrm{V}:\mathrm{W}\to 2^{\rm\sf Prop}$ is
a labelling function. Given an $\mathrm{LTS}$ $\mathcal{S}$ and
$w\in\mathrm{D}_{\mathcal{S}}$, the pair $(\mathcal{S},w)$ is a _pointed
$\mathrm{LTS}$_ (parentheses are usually dropped). $\dashv$

An $\mathrm{LTS}$ describes the _abilities_ of the agent; thus, sometimes
(e.g., [57, 58, 59]) it is also called an _ability map_. Here we introduce
some useful definitions. It is worth noticing that, although the signature is
infinite (since ${\rm\sf Act}$ is a _denumerable_ set), the relations in the
model might be defined only for a (possibly finite) subset of actions.

######  Definition 3.4.

Let $\\{\mathrm{R}_{\\_}a\subseteq\mathrm{W}\times\mathrm{W}\mid a\in A,\text{
for some }A\subseteq{\rm\sf Act}\\}$ be a collection of binary relations.
Define $\mathrm{R}_{\\_}\epsilon:=\\{(w,w)\mid w\in\mathrm{W}\\}$ and, for
$\sigma\in{\rm\sf Act}^{*}$ and $a\in{\rm\sf Act}$,
$\mathrm{R}_{\\_}{\sigma{a}}:=\\{(w,u)\in\mathrm{W}\times\mathrm{W}\mid\exists
v\in\mathrm{W}\text{ s.t. }(w,v)\in\mathrm{R}_{\\_}{\sigma}\text{ and
}(v,u)\in\mathrm{R}_{\\_}{a}\\}$. Take a plan $\sigma\in{\rm\sf Act}^{*}$: for
$u\in\mathrm{W}$ define
$\mathrm{R}_{\\_}{\sigma}(u):=\\{v\in\mathrm{W}\mid(u,v)\in\mathrm{R}_{\\_}{\sigma}\\}$,
and for $U\subseteq\mathrm{W}$ define
$\mathrm{R}_{\\_}{\sigma}(U):=\bigcup_{\\_}{u\in
U}\mathrm{R}_{\\_}{\sigma}(u)$. $\dashv$

The idea in [57, 58, 59] is that an agent knows how to achieve $\varphi$ given
$\psi$ when she has an appropriate plan that allows her to go from any state
in which $\psi$ holds only to states in which $\varphi$ holds. A crucial part
is, then, what “appropriate” is taken to be.

######  Definition 3.5 (Strong executability).

Let $\\{\mathrm{R}_{\\_}a\subseteq\mathrm{W}\times\mathrm{W}\mid a\in A,\text{
for some }A\subseteq{\rm\sf Act}\\}$ be a collection of binary relations. A
plan $\sigma\in{\rm\sf Act}^{*}$ is _strongly executable_ (SE) at
$u\in\mathrm{W}$ if and only if $\mathrm{R}_{\\_}\sigma$ is defined and,
additionally, $v\in\mathrm{R}_{\\_}{\sigma_{\\_}k}(u)$ implies
$\mathrm{R}_{\\_}{\sigma[k+1]}(v)\neq\varnothing$ for every
$k\in[0\mathbin{\ldotp\\!\ldotp}\lvert\sigma\rvert-1]$. We define the set
$\mathrm{SE}(\sigma):=\\{w\in\mathrm{W}\mid\sigma\mbox{ is SE at }w\\}$.
$\dashv$

Thus, strong executability asks for _every_ partial execution of the plan
(including $\epsilon$) to be completed. With this notion, formulas in
$\mathsf{L}_{\mathsf{Kh}}$ are interpreted over an LTS as follows. Notice that
the semantic clause for the $\mathsf{Kh}$ modality shown here is equivalent to
the one found in the original papers.

######  Definition 3.6 ($\mathsf{L}_{\mathsf{Kh}}$ over $\mathrm{LTS}$s).

The relation $\models$ between a pointed $\mathrm{LTS}$ $\mathcal{S},w$ (with
$\mathcal{S}=\langle\mathrm{W},\mathrm{R},\mathrm{V}\rangle$ an $\mathrm{LTS}$
over Act and Prop) and formulas in $\mathsf{L}_{\mathsf{Kh}}$ (over Prop) is
defined inductively as follows:

$\mathcal{S},w\models p$ | $\mbox{\it iff}_{\mbox{\tiny\it def}}$ |  $p\in\mathrm{V}(w)$,
---|---|---
$\mathcal{S},w\models\neg\varphi$ | $\mbox{\it iff}_{\mbox{\tiny\it def}}$ |  $\mathcal{S},w\not\models\varphi$,
$\mathcal{S},w\models\varphi\vee\psi$ | $\mbox{\it iff}_{\mbox{\tiny\it def}}$ |  $\mathcal{S},w\models\varphi\,\mbox{ or }\,\mathcal{S},w\models\psi$,
$\mathcal{S},w\models\mathsf{Kh}(\psi,\varphi)$ | $\mbox{\it iff}_{\mbox{\tiny\it def}}$ |  there exists $\sigma\in{\rm\sf Act}^{*}$ such that ($\bm{\mathsf{Kh}}$-1) $\llbracket\psi\rrbracket^{\mathcal{S}}\subseteq\mathrm{SE}(\sigma)$and  ($\bm{\mathsf{Kh}}$-2) $\mathrm{R}_{\\_}\sigma(\llbracket\psi\rrbracket^{\mathcal{S}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{S}}$,

with
$\llbracket\varphi\rrbracket^{\mathcal{S}}:=\\{w\in\mathrm{W}\mid\mathcal{S},w\models\varphi\\}$
(the elements of $\llbracket\varphi\rrbracket^{\mathcal{S}}$ are sometimes
called $\varphi$-states). The plan $\sigma$ in the semantic case for
$\mathsf{Kh}(\psi,\varphi)$ is often called the witness for
$\mathsf{Kh}(\psi,\varphi)$ in $\mathcal{S}$. $\dashv$

Thus, $\mathsf{Kh}(\psi,\varphi)$ holds at a given $w$ when there is a plan
$\sigma$ such that, when it is executed at any $\psi$-state, it will always
complete every partial execution (condition ($\bm{\mathsf{Kh}}$-1)), ending
unerringly in states satisfying $\varphi$ (condition ($\bm{\mathsf{Kh}}$-2)).
Since $w$ does not play any role in $\mathsf{Kh}$’s semantic clause, the
_knowing how_ operator acts _globally_. Hence,
$\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{S}}$ is either
$\mathrm{D}_{\mathcal{S}}$ or $\varnothing$.

Axiomatization. For axiomatization purposes, note that the global universal
modality [19], interpreted as truth in every state of the model, is definable
in $\mathsf{L}_{\mathsf{Kh}}$ as
$\mathsf{A}\varphi:=\mathsf{Kh}(\neg\varphi,\bot)$. This is justified by the
proposition below, whose proof relies on the fact that ${\rm\sf Act}^{*}$ is
never empty (it always contains $\epsilon$).

######  Proposition 1 ([57]).

Let $\mathcal{S},w$ be a pointed $\mathrm{LTS}$. Then,

$\mathcal{S},w\models\mathsf{Kh}(\neg\varphi,\bot)$ iff
$\llbracket\varphi\rrbracket^{\mathcal{S}}=\mathrm{D}_{\mathcal{S}}$.

$\triangleleft$

$\begin{array}[]{l@{\ \ \ \ }ll}\hline\cr\hline\cr\mbox{\text@underline{Block
$\mathcal{L}$:}}&\mathpzc{TAUT}&\vdash\varphi\mbox{ for $\varphi$ a
propositional tautology}\\\
&\mathpzc{DISTA}&\vdash\mathsf{A}(\varphi\rightarrow\psi)\rightarrow(\mathsf{A}\varphi\rightarrow\mathsf{A}\psi)\\\
&\mathpzc{TA}&\vdash\mathsf{A}\varphi\rightarrow\varphi\\\
&\mathpzc{4KhA}&\vdash\mathsf{Kh}(\psi,\varphi)\rightarrow\mathsf{A}\mathsf{Kh}(\psi,\varphi)\\\
&\mathpzc{5KhA}&\vdash\neg\mathsf{Kh}(\psi,\varphi)\rightarrow\mathsf{A}\neg\mathsf{Kh}(\psi,\varphi)\\\
&\mathpzc{MP}&\mbox{From $\vdash\varphi$ and $\vdash\varphi\rightarrow\psi$
infer $\vdash\psi$ }\\\ &\mathpzc{NECA}&\mbox{From $\vdash\varphi$ infer
$\vdash\mathsf{A}\varphi$}\\\ \hline\cr\mbox{\text@underline{Block
$\mathcal{L}_{\\_}{\mathrm{LTS}}$:}}&\mathpzc{EMP}&\vdash\mathsf{A}(\psi\rightarrow\varphi)\rightarrow\mathsf{Kh}(\psi,\varphi)\\\
&\mathpzc{COMPKh}&\vdash(\mathsf{Kh}(\psi,\varphi)\wedge\mathsf{Kh}(\varphi,\chi))\rightarrow\mathsf{Kh}(\psi,\chi)\\\
\hline\cr\hline\cr\end{array}$ Table 1: Axiom system
$\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$, for $\mathsf{L}_{\mathsf{Kh}}$
w.r.t. $\mathrm{LTS}$s.

The axiom system $\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$ (Table 1) shows
the relationship between the global universal modality $\mathsf{A}$ and the
knowing-how operator $\mathsf{Kh}$. The first block is essentially a standard
modal system for $\mathsf{A}$, additionally establishing that $\mathsf{Kh}$ is
global (see the discussion in [57]). The axioms in the second block deserve a
further comment. Axiom $\mathpzc{EMP}$ states that, if $\psi\to\varphi$ is
globally true, then given $\psi$ the agent knows how to make $\varphi$ true.
In simpler words, global ontic information turns into knowledge. This is
because the empty plan $\epsilon$ is always available. Axiom $\mathpzc{COMP}$
establishes that $\mathsf{Kh}$ is compositional: if given $\psi$ the agent
knows how to make $\varphi$ true, and given $\varphi$ she knows how to make
$\chi$ true, then given $\psi$ she knows how to make $\chi$ true.

######  Theorem 1 ([57]).

The axiom system $\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$ (Table 1) is sound
and strongly complete for $\mathsf{L}_{\mathsf{Kh}}$ w.r.t. the class of all
$\mathrm{LTS}$s. $\triangleleft$

Axioms in the second block might be questionable. First, one could argue that,
contrary to what $\mathpzc{EMP}$ states, not all global truths about what is
achievable in the model need to be considered as knowledge (how) of the agent.
Second, notice that axiom $\mathpzc{COMPKh}$ implies also a certain level of
omniscience: it might as well be that an agent knows how to make $\varphi$
true given $\psi$, and how to make $\chi$ true given $\varphi$, but still has
not worked out how to put together the two witness plans to ensure $\chi$
given $\psi$. These are the two properties that will be lost in the more
general semantics introduced in the next section. In Section 7 we will show
how these formulas become valid when, in the new semantics, one make strong
idealizations.

##  4 Uncertainty-based semantics

The $\mathrm{LTS}$-based semantics provides a reasonable representation of an
agent’s abilities: the agent knows how to achieve $\varphi$ given $\psi$ if
and only if there is a plan that, when executed at any $\psi$-state, will
always complete every partial execution, ending unerringly in states
satisfying $\varphi$. Still, one could argue that this representation involves
a certain level of idealization.

Take an agent that _lacks_ a certain ability. In the $\mathrm{LTS}$-based
semantics, this can only happen when the environment does not provide the
required (sequence of) action(s). Still, there are situations in which an
adequate plan exists, and yet the agent lacks the ability for a different
reason. Indeed, she might _fail to distinguish_ an adequate plan from a non-
adequate one, in the sense of not being able to tell that, in general, those
plans produce different outcomes. Consider, for example, an agent baking a
cake. She might have the ability to do the nine different mixing
methods222https://www.perfectlypastry.com/the-importance-of-the-mixing-method/
(beating, blending, creaming, cutting, folding, kneading, sifting, stirring,
whipping), and she might even recognize them as different actions. However,
she might not be able to perfectly distinguish one from the others: she might
not recognize that, sometimes, they produce different results. In such cases,
one would say that the agent does not know how to bake a cake: sometimes she
gets good outcomes (when she uses the adequate mixing method) and sometimes
she does not.

Indistinguishability among _basic_ actions can account for the example above
(with each mixing method a basic action). Still, one can also think of
situations in which a more general form of indistinguishability, one _among
plans_ , is involved. Consider the baking agent again. It is reasonable to
assume that she can tell the difference between “adding milk” and “adding
flour”, but perhaps she does not realize the effect that _the order_ of these
actions might have in the final result. Here, the issue is not that she cannot
distinguish between basic actions; rather, two plans are indistinguishable
because the order of their actions is being considered irrelevant. For a last
possibility, the agent might not know that, while opening the oven once to
check whether the baking goods are done is reasonable, this must not be done
in excess. In this case, the problem consists in not being able to tell the
difference between the effect of executing an action once and executing it
multiple times. Thus, plans of _different lengths_ might be considered
equivalent for the task at hand, for such an agent.

The previous examples suggest that one can devise a more general
representation of an agent’s abilities. This involves taking into account not
only the plans she has available (the $\mathrm{LTS}$ structure), but also her
skills for telling two different plans apart (a form of _indistinguishability
among plans_). As we will see, this (in)ability for distinguishing plans will
also let us define a natural model for a multi-agent scenario. In this
setting, agents share the same set of _affordances_ (provided by the actual
environment), but still have different _abilities_ depending on and how well
they can tell these affordances apart, or even which of these affordances they
have available. To drive this last point home notice that, in principle, an
agent does not need to have ‘epistemic access’ to every available plan. Some
might be so foreign to the agent, or so complex, that she might not be _aware
of_ them. Such plans are, then, out of the agent’s reach, not in the sense
that she cannot distinguish them from others, but in that she does not even
take them into consideration. This is similar to what [12] proposed for the
epistemic notion of _knowing that_ : the agent might not be aware of (i.e.,
she might not entertain) every formula of the language, and thus she does not
need to know that these formulas are indeed the case.

######  Definition 4.1 (Uncertainty-based $\mathrm{LTS}$).

Let Agt be a finite non-empty set of agents. A _multi-agent uncertainty-based
$\mathrm{LTS}$ ($\mathrm{LTS}^{U}$)_ for ${\rm\sf Prop}$, ${\rm\sf Act}$ and
${\rm\sf Agt}$ is a tuple
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\sim,\mathrm{V}\rangle$ where
$\langle\mathrm{W},\mathrm{R},\mathrm{V}\rangle$ is an $\mathrm{LTS}$ and
$\sim$ assigns, to each agent $i\in{\rm\sf Agt}$, an equivalence
_indistinguishability_ relation over a non-empty set of plans
$\mathrm{P}_{i}\subseteq{\rm\sf Act}^{*}$. Given an $\mathrm{LTS}^{U}$
$\mathcal{M}$ and $w\in\mathrm{D}_{\mathcal{M}}$, the pair $(\mathcal{M},w)$
(parenthesis usually dropped) is called a _pointed $\mathrm{LTS}^{U}$_.
$\dashv$

Intuitively, $\mathrm{P}_{i}$ is the set of plans that agent $i$ has at her
disposal; it contains the plans the agent has access to. Then, similarly as in
classical epistemic logic,
${\sim_{\\_}i}\subseteq\mathrm{P}_{i}\times\mathrm{P}_{i}$ describes agent
$i$’s indistinguishability over her available plans.

######  Remark 1.

The following change in notation will simplify some definitions later on, and
will make the comparison with the $\mathrm{LTS}$-based semantics clearer.

Let $\langle\mathrm{W},\mathrm{R},\sim,\mathrm{V}\rangle$ be an
$\mathrm{LTS}^{U}$ and take $i\in{\rm\sf Agt}$; for a plan
$\sigma\in\mathrm{P}_{i}$, let $[\sigma]_{\\_}i$ be its equivalence class in
$\sim_{\\_}i$ (i.e.,
$[\sigma]_{\\_}i:=\\{\sigma^{\prime}\in\mathrm{P}_{i}\mid\sigma\sim_{\\_}i\sigma^{\prime}\\}$).
There is a one-to-one correspondence between each $\sim_{\\_}i$ and its
induced set of equivalence classes
$\mathrm{S}_{\\_}i:=\\{[\sigma]_{\\_}i\mid\sigma\in\mathrm{P}_{i}\\}$. Hence,
from now on, an $\mathrm{LTS}^{U}$ will be presented as a tuple
$\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$. Notice the following properties of each
$\mathrm{S}_{\\_}i$:  (1) $\mathrm{S}_{\\_}i\neq\varnothing$(as
$\mathrm{P}_{i}\neq\varnothing$),  (2) if
$\uppi_{\\_}1,\uppi_{\\_}2\in\mathrm{S}_{\\_}i$ and
$\uppi_{\\_}1\neq\uppi_{\\_}2$, then
$\uppi_{\\_}1\cap\uppi_{\\_}2=\varnothing$ (equivalence classes are pairwise
disjoint),  (3)
$\mathrm{P}_{i}=\bigcup_{\\_}{\uppi\in\mathrm{S}_{\\_}i}\uppi$(their union is
exactly $\mathrm{P}_{1}$), and  (4) $\varnothing\notin\mathrm{S}_{\\_}i$(the
empty set is not an equivalence class) . $\dashv$

Given her uncertainty over ${\rm\sf Act}^{*}$ (or, more precisely, over _her_
‘domain of plans’ $\mathrm{P}_{i}\subseteq{\rm\sf Act}^{*}$), the abilities of
an agent $i$ depend not on what a single plan can achieve, but rather on what
a set of them can guarantee.

######  Definition 4.2.

For $\uppi\subseteq{\rm\sf Act}^{*}$, $u\in\mathrm{W}$ and
$U\subseteq\mathrm{W}$, define

$\mathrm{R}_{\\_}\uppi:=\bigcup_{\\_}{\sigma\in\uppi}\mathrm{R}_{\\_}{\sigma},\qquad\mathrm{R}_{\\_}{\uppi}(u):=\bigcup_{\\_}{\sigma\in\uppi}\mathrm{R}_{\\_}\sigma(u),\qquad\mathrm{R}_{\\_}{\uppi}(U):=\bigcup_{\\_}{u\in
U}\mathrm{R}_{\\_}{\uppi}(u).$

$\dashv$

We can now generalize the notion of strong executability for sets of plans.

######  Definition 4.3 (Strong executability).

A _set of plans_ $\uppi\subseteq{\rm\sf Act}^{*}$ is _strongly executable_ at
$u\in\mathrm{W}$ if and only if _every_ plan $\sigma\in\uppi$ is _strongly
executable_ at $u$. Thus,
$\mathrm{SE}(\uppi):=\bigcap_{\\_}{\sigma\in\uppi}\mathrm{SE}(\sigma)$ is the
set of the states in $\mathrm{W}$ where $\uppi$ is strongly executable.
$\dashv$

######  Definition 4.4 ($\mathsf{Kh}_{i}$ over $\mathrm{LTS}^{U}$s).

Let $\mathsf{L}_{\mathsf{Kh}_{i}}$ be the multi-agent version of the language
$\mathsf{L}_{\mathsf{Kh}}$, obtained by replacing $\mathsf{Kh}$ with
$\mathsf{Kh}_{i}$ (with $i\in{\rm\sf Agt}$ for ${\rm\sf Agt}\neq\varnothing$).
The satisfiability relation $\models$ between a pointed $\mathrm{LTS}^{U}$
$\mathcal{M},w$ (with
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$ an $\mathrm{LTS}^{U}$ over Act, Prop and Agt) and
formulas in $\mathsf{L}_{\mathsf{Kh}_{i}}$ is defined inductively. The atomic
and Boolean cases are as before. For _knowing how_ formulas,

$\mathcal{M},w\models\mathsf{Kh}_{i}(\psi,\varphi)$ | $\mbox{\it iff}_{\mbox{\tiny\it def}}$ |  there exists $\uppi\in\mathrm{S}_{\\_}i$ such that ($\bm{\mathsf{Kh}}$-1) $\llbracket\psi\rrbracket^{\mathcal{M}}\subseteq\mathrm{SE}(\uppi)$and  ($\bm{\mathsf{Kh}}$-2) $\mathrm{R}_{\\_}\uppi(\llbracket\psi\rrbracket^{\mathcal{M}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}}$,
---|---|---

with
$\llbracket\varphi\rrbracket^{\mathcal{M}}:=\\{w\in\mathrm{W}\mid\mathcal{M},w\models\varphi\\}$.
The set of plans $\pi$ in the semantic case for
$\mathsf{Kh}_{i}(\psi,\varphi)$ is often called the witness for
$\mathsf{Kh}_{i}(\psi,\varphi)$ in $\mathcal{M}$. $\dashv$

It is worth comparing Definition 3.6 and Definition 4.4. As before,
$\mathsf{Kh}_{i}(\psi,\varphi)$ acts _globally_. But now, we require _for
agent $i$_ to have a _set of plans_ satisfying strong executability in every
$\psi$-state (condition ($\bm{\mathsf{Kh}}$-1)). Still, the set of plans
should work as the single plan did before: when executed at $\psi$-states, it
should end unerringly in states satisfying $\varphi$ (condition
($\bm{\mathsf{Kh}}$-2)).

It is also important to notice that the global universal modality is also
definable within $\mathsf{L}_{\mathsf{Kh}_{i}}$ over $\mathrm{LTS}^{U}$. (For
this, it is crucial that $\mathrm{S}_{\\_}i\neq\varnothing$ and
$\varnothing\not\in\mathrm{S}_{\\_}i$, as stated in Remark 1.)

######  Proposition 2.

Let $\mathcal{M},w$ be a pointed $\mathrm{LTS}^{U}$. Then,

there is $i\in{\rm\sf Agt}$ with
$\mathcal{M},w\models\mathsf{Kh}_{i}(\neg\varphi,\bot)$ iff
$\llbracket\varphi\rrbracket^{\mathcal{M}}=\mathrm{D}_{\mathcal{M}}$.

######  Proof..

$\bm{(\Rightarrow)}$ Suppose there is $i\in{\rm\sf Agt}$ with
$\mathcal{M},w\models\mathsf{Kh}_{i}(\neg\varphi,\bot)$. Then, there is
$\uppi\in\mathrm{S}_{\\_}i$ such that  ($\bm{\mathsf{Kh}}$-1)
$\llbracket\lnot\varphi\rrbracket^{\mathcal{M}}\subseteq\mathrm{SE}(\uppi)$and
($\bm{\mathsf{Kh}}$-2)
$\mathrm{R}_{\\_}\uppi(\llbracket\lnot\varphi\rrbracket^{\mathcal{M}})\subseteq\llbracket\bot\rrbracket^{\mathcal{M}}$
. For a contradiction, suppose
$\llbracket\varphi\rrbracket^{\mathcal{M}}\neq\mathrm{D}_{\mathcal{M}}$, so
there is $u\in\llbracket\lnot\varphi\rrbracket^{\mathcal{M}}$. Then,
($\bm{\mathsf{Kh}}$-1) implies
$u\in\mathrm{SE}(\uppi)=\bigcap_{\\_}{\sigma\in\uppi}\mathrm{SE}(\sigma)$. But
$\uppi\in\mathrm{S}_{\\_}i$, so $\uppi\neq\varnothing$, that is, there is
$\sigma\in\uppi$ with $u\in\mathrm{SE}(\sigma)$; thus,
$\mathrm{R}_{\\_}\sigma(u)\neq\varnothing$, so
$\mathrm{R}_{\\_}\uppi(u)\neq\varnothing$ and hence
$\mathrm{R}_{\\_}\uppi(\llbracket\lnot\varphi\rrbracket^{\mathcal{M}})\neq\varnothing$,
that is,
$\varnothing\subset\mathrm{R}_{\\_}\uppi(\llbracket\lnot\varphi\rrbracket^{\mathcal{M}})$.
But then, from ($\bm{\mathsf{Kh}}$-2),
$\varnothing\subset\mathrm{R}_{\\_}\uppi(\llbracket\lnot\varphi\rrbracket^{\mathcal{M}})\subseteq\llbracket\bot\rrbracket^{\mathcal{M}}$,
i.e., $\varnothing\subset\llbracket\bot\rrbracket^{\mathcal{M}}$, a
contradiction. Therefore,
$\llbracket\varphi\rrbracket^{\mathcal{M}}=\mathrm{D}_{\mathcal{M}}$.

$\bm{(\Leftarrow)}$ Suppose
$\llbracket\varphi\rrbracket^{\mathcal{M}}=\mathrm{D}_{\mathcal{M}}$. Then
$\llbracket\lnot\varphi\rrbracket^{\mathcal{M}}=\varnothing$ and hence
($\bm{\mathsf{Kh}}$-1) in the semantic clause of
$\mathsf{Kh}_{i}(\lnot\varphi,\bot)$ holds for every $\uppi\in 2^{{\rm\sf
Act}^{*}}$. Moreover,
$\mathrm{R}_{\\_}\uppi(\llbracket\lnot\varphi\rrbracket^{\mathcal{M}})=\bigcup_{\\_}{u\in\llbracket\lnot\varphi\rrbracket^{\mathcal{M}}}\mathrm{R}_{\\_}\uppi(u)=\bigcup_{\\_}{u\in\varnothing}\mathrm{R}_{\\_}\uppi(u)=\varnothing$,
so ($\bm{\mathsf{Kh}}$-2) also holds for any such $\uppi$. Finally,
$\mathrm{S}_{\\_}i\neq\varnothing$ (so there is $\uppi\in\mathrm{S}_{\\_}i$)
and ${\rm\sf Agt}\neq\varnothing$ (so there is $i\in{\rm\sf Agt}$); therefore,
there is $i\in{\rm\sf Agt}$ with
$\mathcal{M},w\models\mathsf{Kh}_{i}(\neg\varphi,\bot)$. $\blacksquare$

$\triangleleft$

Hence, one can take $\mathsf{A}\varphi:=\bigvee_{\\_}{i\in{\rm\sf
Agt}}\mathsf{Kh}_{i}(\neg\varphi,\bot)$ (recall: ${\rm\sf Agt}$ is non-empty
and finite) and $\mathsf{E}\varphi:=\neg\mathsf{A}\neg\varphi$.

Now, clearly different agents have different awareness about their own
abilities. At the same time, because of the global nature of the modality of
knowing how, it holds that

$\mathcal{M},w\models\mathsf{Kh}_{\\_}i(\psi,\varphi)$ if and only if
$\mathcal{M},w\models\mathsf{A}\mathsf{Kh}_{\\_}i(\psi,\varphi)$,

or equivalenty,

$\mathcal{M},w\models\mathsf{Kh}_{\\_}j(\neg\mathsf{Kh}_{\\_}i(\psi,\varphi),\bot)$,
for some agent $j$.

But this does not imply that agents _know that_ “agent $i$ knows how to achive
$\varphi$ given $\psi$.” It is only the case that
$\mathsf{Kh}_{\\_}i(\psi,\varphi)$ becomes an objective true, and hence
assuming its negation naturally leads to contradiction. There is no notion of
epistemic indistinguishability over states in our models, which could lead to
a notion of “knows that”.

Lastly, one can argue that since models are equipped with a notion of
epistemic indistinguishability between plans, an agent should know that a
certain plan is (or is not) distinguishable from another, or that an agent is
aware of the availability of a certain course of action. However, knowing how
modalities cannot talk about the relation itself, only about the existence of
a set of indistinguishable plans, and the effects of executing those plans.

##  5 Bisimulations

Bisimulation is a crucial tool for understanding the expressive power of a
formal language. In [17, 18], bisimulation notions for
$\mathsf{L}_{\mathsf{Kh}}$ over $\mathrm{LTS}$s have been introduced. This
section discusses similar ideas for $\mathsf{L}_{\mathsf{Kh}_{i}}$ over
$\mathrm{LTS}^{U}$s.

First, a useful abbreviation.

######  Definition 5.1.

Let
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$ be an $\mathrm{LTS}^{U}$ over Prop, Act and Agt. Take
a set of plans $\uppi\in 2^{({\rm\sf Act}^{*})}$, sets of states
$U,T\subseteq\mathrm{W}$ and an agent $i\in{\rm\sf Agt}$.

  * •

Write
$U\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle\uppi$\cr\kern
1.07639pt\cr$\Rightarrow$\cr}}}$}}T$ $\;\mbox{\it iff}_{\mbox{\tiny\it
def}}\;$ $U\subseteq\mathrm{SE}(\uppi)$ and
$\mathrm{R}_{\\_}{\uppi}(U)\subseteq T$.

  * •

Write
$U\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T$ $\;\mbox{\it
iff}_{\mbox{\tiny\it def}}\;$ there is $\uppi\in\mathrm{S}_{\\_}i$ such that
$U\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle\uppi$\cr\kern
1.07639pt\cr$\Rightarrow$\cr}}}$}}T$.

Additionally, $U\subseteq\mathrm{W}$ is
$\mathsf{L}_{\mathsf{Kh}_{i}}$-definable (respectively, propositionally
definable) in $\mathcal{M}$ if and only if there is an
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formula (propositional formula) $\varphi$ such
that $U=\llbracket\varphi\rrbracket^{\mathcal{M}}$. $\dashv$

Two quick observations. First, note how the abbreviation simplifies the
semantic clause for _knowing how_ formulas:
$\mathcal{M},w\models\mathsf{Kh}_{i}(\psi,\varphi)$ if and only if
$\llbracket\psi\rrbracket^{\mathcal{M}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern
1.07639pt\cr$\Rightarrow$\cr}}}$}}\llbracket\varphi\rrbracket^{\mathcal{M}}$.
Second, under the $\mathrm{LTS}^{U}$-based semantics,
$\mathsf{L}_{\mathsf{Kh}_{i}}$-definability implies propositional
definability. Its proof, analogous to the $\mathrm{LTS}$-based semantics case
in [17, 18], relies on the fact that $\mathsf{Kh}_{i}$ acts globally.

######  Proposition 3.

Let $\mathcal{M}$ be an $\mathrm{LTS}^{U}$. For all
$U\subseteq\mathrm{D}_{\mathcal{M}}$, if $U$ is
$\mathsf{L}_{\mathsf{Kh}_{i}}$-definable, then it is propositionally
definable. $\triangleleft$

We now introduce the notion of bisimulation. Note how, although the collection
of binary relations of a model is not explicitly mentioned, it is referred to
through the abstract relation
“$\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}$” (Definition 5.1).

######  Definition 5.2 ($\mathsf{L}_{\mathsf{Kh}_{i}}$-bisimulation).

Let $\mathcal{M}$ and $\mathcal{M}^{\prime}$ be two ${\mathrm{LTS}^{U}}s$,
their domains being $\mathrm{W}$ and $\mathrm{W}^{\prime}$, respectively. Take
$Z\subseteq\mathrm{W}\times\mathrm{W}^{\prime}$.

  * •

For $u\in\mathrm{W}$ and $U\subseteq\mathrm{W}$, define

$Z(u):=\\{u^{\prime}\in\mathrm{W}^{\prime}\mid uZu^{\prime}\\}$,
$Z(U):=\bigcup_{\\_}{u\in U}Z(u)$.
---

  * •

For $u^{\prime}\in\mathrm{W}^{\prime}$ and
$U^{\prime}\subseteq\mathrm{W}^{\prime}$, define

$Z^{-1}(u^{\prime}):=\\{u\in\mathrm{W}\mid uZu^{\prime}\\}$;
$Z^{-1}(U^{\prime}):=\bigcup_{\\_}{u^{\prime}\in U^{\prime}}Z(u^{\prime})$.
---

A non-empty $Z\subseteq\mathrm{W}\times\mathrm{W}^{\prime}$ is called an
$\mathsf{L}_{\mathsf{Kh}_{i}}$-bisimulation between $\mathcal{M}$ and
$\mathcal{M}^{\prime}$ if and only if $wZw^{\prime}$ implies all of the
following.

  * •

Atom: $\mathrm{V}(w)=\mathrm{V}^{\prime}(w^{\prime})$.

  * •

$\mathsf{Kh}_{i}$-Zig: for any _propositionally_ definable
$U\subseteq\mathrm{W}$, if
$U\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T$ for some
$T\subseteq\mathrm{W}$, then there is $T^{\prime}\subseteq\mathrm{W}^{\prime}$
satisfying both

    1. (B1)

$Z(U)\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$,

    2. (B2)

$T^{\prime}\subseteq Z(T)$.

  * •

$\mathsf{Kh}_{i}$-Zag: for any _propositionally_ definable
$U^{\prime}\subseteq\mathrm{W}^{\prime}$, if
$U^{\prime}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$ for some
$T^{\prime}\subseteq\mathrm{W}^{\prime}$, then there is $T\subseteq\mathrm{W}$
satisfying both

    1. (B1)

$Z^{-1}(U^{\prime})\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T$,

    2. (B2)

$T\subseteq Z^{-1}(T^{\prime})$.

  * •

$\mathsf{A}$-Zig: for all $u$ in $\mathrm{W}$ there is a $u^{\prime}$ in
$\mathrm{W}^{\prime}$ such that $uZu^{\prime}$.

  * •

$\mathsf{A}$-Zag: for all $u^{\prime}$ in $\mathrm{W}^{\prime}$ there is a $u$
in $\mathrm{W}$ such that $uZu^{\prime}$.

We write
$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M}^{\prime},w^{\prime}$
when there is an $\mathsf{L}_{\mathsf{Kh}}$-bisimulation $Z$ between
$\mathcal{M}$ and $\mathcal{M}^{\prime}$ such that $wZw^{\prime}$. $\dashv$

The two requirements in $\mathsf{Kh}_{i}$-Zig are equivalent to a single one:
$Z(U)\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}Z(T)$. They are split to resemble
more closely the definition of a standard bisimulation: if $U$ has an
‘$i$-successor’ $T$, then its ‘bisimulation image’ $U^{\prime}$ also has an
‘$i$-successor’, namely $T^{\prime}$ (clause
$Z(U)\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$), and these
successors are a ‘bisimilar match’ (clause $T^{\prime}\subseteq Z(T)$). The
case of $\mathsf{Kh}_{i}$-Zag is analogous.

In order to formalize the crucial properties of a bisimulation, we define the
notion of model equivalence with respect to $\mathsf{L}_{\mathsf{Kh}_{i}}$.

######  Definition 5.3 ($\mathsf{L}_{\mathsf{Kh}_{i}}$-equivalence).

Two pointed ${\mathrm{LTS}^{U}}s$ $\mathcal{M},w$ and
$\mathcal{M}^{\prime},w^{\prime}$ are _$\mathsf{L}_{\mathsf{Kh}_{i}}$
-equivalent_ (written
$\mathcal{M},w\mathrel{\leftrightsquigarrow}\mathcal{M}^{\prime},w^{\prime}$)
if and only if, for every $\varphi\in\mathsf{L}_{\mathsf{Kh}_{i}}$,

$\mathcal{M},w\models\varphi$ iff
$\mathcal{M}^{\prime},w^{\prime}\models\varphi$.

$\dashv$

Then, we can state the intended correspondence between
$\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}$
and $\mathrel{\leftrightsquigarrow}$.

######  Theorem 2 ($\mathsf{L}_{\mathsf{Kh}_{i}}$-bisimilarity implies
$\mathsf{L}_{\mathsf{Kh}_{i}}$-equivalence).

Let $\mathcal{M},w$ and $\mathcal{M}^{\prime},w^{\prime}$ be pointed
$\mathrm{LTS}^{U}$s. Then,

$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M}^{\prime},w^{\prime}\quad\text{implies}\quad\mathcal{M},w\mathrel{\leftrightsquigarrow}\mathcal{M}^{\prime},w^{\prime}$.

######  Proof..

Take
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$ and
$\mathcal{M}^{\prime}=\langle\mathrm{W}^{\prime},\mathrm{R}^{\prime},\\{\mathrm{S}^{\prime}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},$ $\mathrm{V}^{\prime}\rangle$. From the given
$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M}^{\prime},w^{\prime}$,
there is an $\mathsf{L}_{\mathsf{Kh}_{i}}$-bisimulation
$Z\subseteq(\mathrm{W}\times\mathrm{W}^{\prime})$ with $wZw^{\prime}$. The
proof of $\mathsf{L}_{\mathsf{Kh}_{i}}$-equivalence is by structural induction
on $\mathsf{L}_{\mathsf{Kh}_{i}}$-formulas. The cases for atomic propositions
and Boolean operators are standard, and only formulas of the form
$\mathsf{Kh}_{i}(\psi,\varphi)$ are left. Note how, for this case, the
inductive hypothesis (IH) states that, for $u\in\mathrm{W}$,
$u^{\prime}\in\mathrm{W}^{\prime}$ and $\chi$ a subformula of
$\mathsf{Kh}_{i}(\psi,\varphi)$, if $uZu^{\prime}$ then
$u\in\llbracket\chi\rrbracket^{\mathcal{M}}$ iff
$u^{\prime}\in\llbracket\chi\rrbracket^{\mathcal{M}^{\prime}}$.

Suppose $w\in\llbracket\mathsf{Kh}_{i}(\psi,\varphi)\rrbracket^{\mathcal{M}}$.
Then, by semantic interpretation,
$\llbracket\psi\rrbracket^{\mathcal{M}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern
1.07639pt\cr$\Rightarrow$\cr}}}$}}\llbracket\varphi\rrbracket^{\mathcal{M}}$.
It is useful to notice that
$Z(\llbracket\chi\rrbracket^{\mathcal{M}})=\llbracket\chi\rrbracket^{\mathcal{M}^{\prime}}$
holds for $\chi\in\\{\psi,\varphi\\}$.

  * $\bm{(\subseteq)}$

If $v^{\prime}\in Z(\llbracket\chi\rrbracket^{\mathcal{M}})$, then there is
$v\in\llbracket\chi\rrbracket^{\mathcal{M}}$ such that $vZv^{\prime}$. Thus,
from IH we have
$v^{\prime}\in\llbracket\chi\rrbracket^{\mathcal{M}^{\prime}}$.

  * $\bm{(\supseteq)}$

If $v^{\prime}\in\llbracket\chi\rrbracket^{\mathcal{M}^{\prime}}$ then, by
$\mathsf{A}$-Zag, there is $v$ with $vZv^{\prime}$; thus, from IH we have
$v\in\llbracket\chi\rrbracket^{\mathcal{M}}$. Hence, $v^{\prime}\in
Z(\llbracket\chi\rrbracket^{\mathcal{M}})$.

Now, the proof. We have
$\llbracket\psi\rrbracket^{\mathcal{M}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern
1.07639pt\cr$\Rightarrow$\cr}}}$}}\llbracket\varphi\rrbracket^{\mathcal{M}}$.
The set $\llbracket\psi\rrbracket^{\mathcal{M}}$ is obviously
$\mathsf{L}_{\mathsf{Kh}_{i}}$-definable, and hence propositionally definable
too (Proposition 3). Then, from the $\mathsf{Kh}_{i}$-Zig clause, there is
$T^{\prime}\subseteq\mathrm{W}^{\prime}$ such that  (B1)
$Z(\llbracket\psi\rrbracket^{\mathcal{M}})\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$and  (B2)
$T^{\prime}\subseteq Z(\llbracket\varphi\rrbracket^{\mathcal{M}})$ .
Therefore,
$Z(\llbracket\psi\rrbracket^{\mathcal{M}})\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern
1.07639pt\cr$\Rightarrow$\cr}}}$}}Z(\llbracket\varphi\rrbracket^{\mathcal{M}})$
and hence, by the result above,
$\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern
1.07639pt\cr$\Rightarrow$\cr}}}$}}\llbracket\varphi\rrbracket^{\mathcal{M}^{\prime}}$.
Thus,
$w^{\prime}\in\llbracket\mathsf{Kh}_{i}(\psi,\varphi)\rrbracket^{\mathcal{M}^{\prime}}$.

The direction from
$w^{\prime}\in\llbracket\mathsf{Kh}_{i}(\psi,\varphi)\rrbracket^{\mathcal{M}^{\prime}}$
to $w\in\llbracket\mathsf{Kh}_{i}(\psi,\varphi)\rrbracket^{\mathcal{M}}$
follows a similar argument, using $\mathsf{A}$-Zig and $\mathsf{Kh}_{i}$-Zag
instead. $\blacksquare$

$\triangleleft$

It is easy to see that the converse of Theorem 2 does not hold over arbitrary
models: in fact, the counterexample provided in [18, Section 2] serves also
here to make our point. To satisfy the converse, we usually need to restrict
ourselves to some particular classes of models, that are in general known as
Hennessy-Milner classes. In many modal logics, one typically works only with
image-finite models: those in which, at every state, every basic relation has
only finitely many successors. For languages in which the global universal
modality $\mathsf{A}$ is definable, as $\mathsf{L}_{\mathsf{Kh}_{i}}$, this
requirement needs to be strengthened, as every state can reach (via the
relation underlying $\mathsf{A}$) every other state. For instance, we can take
the class of models with a finite domain. Precisely, here we show that the
class of finite models (taken as those with a finite domain) forms a Hennessy-
Milner class. Note that we do not impose any restriction over the uncertainty
relation of the models (or the sets $\mathrm{S}_{\\_}i$).

######  Theorem 3 ($\mathsf{L}_{\mathsf{Kh}_{i}}$-equivalence implies
$\mathsf{L}_{\mathsf{Kh}_{i}}$-bisimilarity).

Let $\mathcal{M},w$ and $\mathcal{M}^{\prime},w^{\prime}$ be _finite_ pointed
$\mathrm{LTS}^{U}$s. Then,

$\mathcal{M},w\mathrel{\leftrightsquigarrow}\mathcal{M}^{\prime},w^{\prime}\quad\text{implies}\quad\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M}^{\prime},w^{\prime}$.

######  Proof..

Take
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$ and
$\mathcal{M}^{\prime}=\langle\mathrm{W}^{\prime},\mathrm{R}^{\prime},\\{\mathrm{S}^{\prime}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}^{\prime}\rangle$. The strategy is to show that the relation
$\mathrel{\leftrightsquigarrow}$ is already a
$\mathsf{L}_{\mathsf{Kh}_{i}}$–bisimulation. Thus, define

$Z:=\\{(v,v^{\prime})\in(\mathrm{W}\times\mathrm{W}^{\prime})\mid\mathcal{M},v\mathrel{\leftrightsquigarrow}\mathcal{M}^{\prime},v^{\prime}\\}$

so $wZw^{\prime}$ implies $w$ and $w^{\prime}$ satisfy exactly the same
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formulas. In order to show that $Z$ satisfies
the requirements, take any $(w,w^{\prime})\in Z$.

  * •

Atom. States $w$ and $w^{\prime}$ agree in all
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formulas, and thus in all atoms.

  * •

$\mathsf{A}$-Zig. Take $v\in\mathrm{W}$ and suppose, for the sake of a
contradiction, that there is no $v^{\prime}\in\mathrm{W}^{\prime}$ such that
$vZv^{\prime}$. Then, from $Z$’s definition, for each
$v_{\\_}i^{\prime}\in\mathrm{W}^{\prime}=\\{v^{\prime}_{\\_}1,\ldots,v^{\prime}_{\\_}n\\}$
(recall: $\mathcal{M}^{\prime}$ is finite) there is an
$\mathsf{L}_{\mathsf{Kh}}$-formula $\theta_{\\_}i$ such that
$\mathcal{M},v\models\theta_{\\_}i$ but
$\mathcal{M}^{\prime},v^{\prime}_{\\_}i\not\models\theta_{\\_}i$. Now take
$\theta:=\theta_{\\_}1\land\cdots\land\theta_{\\_}n$. Clearly,
$\mathcal{M},v\models\theta$; however,
$\mathcal{M}^{\prime},v_{\\_}i^{\prime}\not\models\theta$ for each
$v_{\\_}i^{\prime}\in\mathrm{W}^{\prime}$, as each one of them makes ‘its’
conjunct $\theta_{\\_}i$ false. Then, $\mathcal{M},w\models\mathsf{E}\theta$
but $\mathcal{M}^{\prime},w^{\prime}\not\models\mathsf{E}\theta$,
contradicting the assumption $wZw^{\prime}$.

  * •

$\mathsf{A}$-Zag. Analogous to the $\mathsf{A}$-Zig case.

  * •

$\mathsf{Kh}_{i}$-Zig. Take any propositionally definable set
$\llbracket\psi\rrbracket^{\mathcal{M}}\subseteq\mathrm{W}$ (thus, $\psi$ is
propositional), and suppose
$\llbracket\psi\rrbracket^{\mathcal{M}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T$ for some
$T\subseteq\mathrm{W}$. We need to find a
$T^{\prime}\subseteq\mathrm{W}^{\prime}$ satisfying both

    1. (B1)

$Z(\llbracket\psi\rrbracket^{\mathcal{M}})\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$,

    2. (B2)

$T^{\prime}\subseteq Z(T)$.

Note that
$Z(\llbracket\psi\rrbracket^{\mathcal{M}})=\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}$.
For $\bm{(\supseteq)}$, suppose
$u^{\prime}\in\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}$. From
$\mathsf{A}$-Zag (proved above), there is $u\in\mathrm{W}$ such that
$uZu^{\prime}$; then, from $Z$’s definition,
$u\in\llbracket\psi\rrbracket^{\mathcal{M}}$ so $u^{\prime}\in
Z(\llbracket\psi\rrbracket^{\mathcal{M}})$. For $\bm{(\subseteq)}$, suppose
$u^{\prime}\in Z(\llbracket\psi\rrbracket^{\mathcal{M}})$. Then, there is
$u\in\llbracket\psi\rrbracket^{\mathcal{M}}$ such that $uZu^{\prime}$, and
therefore, from $Z$’s definition,
$u^{\prime}\in\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}$. Thus, we
actually require a $T^{\prime}\subseteq\mathrm{W}^{\prime}$ satisfying both

    1. (B1)

$\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$,

    2. (B2)

$T^{\prime}\subseteq Z(T)$.

Now, consider two alternatives.

    1. (1)

Assume $\llbracket\psi\rrbracket^{\mathcal{M}}=\varnothing$. Then,
$\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}=Z(\llbracket\psi\rrbracket^{\mathcal{M}})=\varnothing$
and hence $T^{\prime}=\varnothing$ does the job, as the following hold

      1. (B1)

$\varnothing\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}\varnothing$ (as
$\mathrm{S}_{\\_}i\neq\varnothing$),

      2. (B2)

$\varnothing\subseteq Z(T)$.

    2. (2)

Assume $\llbracket\psi\rrbracket^{\mathcal{M}}\neq\varnothing$. This gives us
$T\neq\varnothing$ (from
$\llbracket\psi\rrbracket^{\mathcal{M}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T$), which will be useful later.
To show that there is a $T^{\prime}\subseteq\mathrm{W}^{\prime}$ satisfying
both (B1) and (B2), we proceed by contradiction, so suppose there is no
$T^{\prime}$ satisfying both requirements: every
$T^{\prime}\subseteq\mathrm{W}^{\prime}$ satisfying (B1) fails at (B2). In
other words, every $T^{\prime}\subseteq\mathrm{W}^{\prime}$ satisfying
$\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$ has a state
$v^{\prime}_{\\_}{T^{\prime}}\in T^{\prime}$ that is not the $Z$-image of some
state $v\in T$ (i.e., $vZv^{\prime}_{\\_}{T^{\prime}}$ fails for every $v\in
T$). From $Z$’s definition, the latter means that every state in $T$ can be
distinguished from this $v^{\prime}_{\\_}{T^{\prime}}$ by an
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formula. Thus, given any
$T^{\prime}\subseteq\mathrm{W}^{\prime}$ with
$\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$, one can find a state
$v^{\prime}_{\\_}{T^{\prime}}\in T^{\prime}$ such that, for each $v\in T$,
there is a formula $\theta^{v}_{\\_}{v^{\prime}_{\\_}{T^{\prime}}}$ with
$\mathcal{M},v\models\theta^{v}_{\\_}{v^{\prime}_{\\_}{T^{\prime}}}$ but
$\mathcal{M}^{\prime},v^{\prime}_{\\_}{T^{\prime}}\not\models\theta^{v}_{\\_}{v^{\prime}_{\\_}{T^{\prime}}}$.
Then, for each such $v^{\prime}_{\\_}{T^{\prime}}$ in each such $T^{\prime}$
define

$\displaystyle\theta_{\\_}{T^{\prime}}:=\bigvee_{\\_}{v\in T}\theta^{v}_{\\_}{v^{\prime}_{\\_}{T^{\prime}}}$ and then |  $\displaystyle\theta:=\bigwedge_{\\_}{\\{T^{\prime}\subseteq\mathrm{W}^{\prime}\mid\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}\\}}\theta_{\\_}{T^{\prime}}$,
---|---

Observe the following. First, $\theta_{\\_}{T^{\prime}}$ is indeed a formula,
as $\mathrm{W}$ is finite and thus so is $T$. Equally important,
$T\neq\varnothing$, and thus $\theta_{\\_}{T^{\prime}}$ does not collapse to
$\bot$. Second, $\theta$ is also a formula, as $\mathrm{W}^{\prime}$ is finite
and thus so is
$\\{T^{\prime}\subseteq\mathrm{W}^{\prime}\mid\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}\\}$. However, the
latter set might be empty. This is what creates the following two cases.

       * –

Suppose
$\\{T^{\prime}\subseteq\mathrm{W}^{\prime}\mid\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}\\}=\varnothing$. Then,
consider the formula $\mathsf{Kh}_{i}(\psi,\top)$. Since
$\llbracket\psi\rrbracket^{\mathcal{M}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T$ and
$T\subseteq\mathrm{W}=\llbracket\top\rrbracket^{\mathcal{M}}$, it follows that
$\mathcal{M},w\models\mathsf{Kh}_{i}(\psi,\top)$. However,
$\mathcal{M}^{\prime},w^{\prime}\not\models\mathsf{Kh}_{i}(\psi,\top)$ as,
according to this case, there is no $T^{\prime}\subseteq\mathrm{W}^{\prime}$
with
$\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$. This contradicts the
$\mathsf{L}_{\mathsf{Kh}_{i}}$-equivalence of $w$ and $w^{\prime}$.

       * –

Suppose
$\\{T^{\prime}\subseteq\mathrm{W}^{\prime}\mid\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}\\}\neq\varnothing$.
Then, $\theta$ does not collapse to $\top$. Now, note how every $v\in T$
satisfies its ‘own’ disjunct $\theta^{v}_{\\_}{v^{\prime}_{\\_}{T^{\prime}}}$
in each conjunct $\theta_{\\_}{T^{\prime}}$, and thus it satisfies $\theta$.
Thus, $T\subseteq\llbracket\theta\rrbracket^{\mathcal{M}}$ and hence, from
$\llbracket\psi\rrbracket^{\mathcal{M}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T$ and the fact that
$\mathsf{Kh}_{i}$-formulas are global, it follows that
$\mathcal{M},w\models\mathsf{Kh}_{i}(\psi,\theta)$. However, for each
$T^{\prime}$ in
$\\{T^{\prime}\subseteq\mathrm{W}^{\prime}\mid\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}\\}$, the state
$v^{\prime}_{\\_}{T^{\prime}}$ that cannot be matched with any state $v\in T$
makes all disjuncts in $\theta_{\\_}{T^{\prime}}$ false, thus falsifying
$\theta_{\\_}{T^{\prime}}$ and therefore falsifying $\theta$ too. In other
words, every $T^{\prime}\subseteq\mathrm{W}^{\prime}$ with
$\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$ contains a state
$t^{\prime}_{\\_}{T^{\prime}}$ with
$\mathcal{M}^{\prime},t^{\prime}_{\\_}{T^{\prime}}\not\models\theta$, that is,
$\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}\mathrel{\raisebox{-0.86108pt}{$\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
i$\cr\kern 1.07639pt\cr$\Rightarrow$\cr}}}$}}T^{\prime}$ implies
$T^{\prime}\not\subseteq\llbracket\theta\rrbracket^{\mathcal{M}}$. Hence,
using again the fact that $\mathsf{Kh}_{i}$-formulas are global,
$\mathcal{M}^{\prime},w^{\prime}\not\models\mathsf{Kh}_{i}(\psi,\theta)$,
contradicting the $\mathsf{L}_{\mathsf{Kh}_{i}}$-equivalence of $w$ and
$w^{\prime}$.

  * •

$\mathsf{Kh}_{i}$-Zag. Analogous to the $\mathsf{Kh}_{i}$-Zig case.

$\blacksquare$

$\triangleleft$

##  6 Axiomatization

We now present a sound and complete axiom system for
$\mathsf{L}_{\mathsf{Kh}_{i}}$ under the $\mathrm{LTS}^{U}$-based semantics.
Recall that $\mathsf{A}\varphi:=\bigvee_{\\_}{i\in{\rm\sf
Agt}}\mathsf{Kh}_{i}(\neg\varphi,\bot)$ and
$\mathsf{E}\varphi:=\neg\mathsf{A}\neg\varphi$. With this, it turns out that
formulas and rules in $\mathcal{L}$ (the first block of Table 1) are still
sound under $\mathrm{LTS}^{U}$ (provided $\mathsf{Kh}$ is replaced by
$\mathsf{Kh}_{i}$). They will constitute the first part of an axiom system for
$\mathsf{L}_{\mathsf{Kh}_{i}}$ over $\mathrm{LTS}^{U}$ (first block in Table
2). Still, this is not enough for a complete axiom system. The axioms on the
second block of Table 2, $\mathpzc{KhE}$ and $\mathpzc{KhA}$, are the missing
pieces333$\mathpzc{KhE}$ and $\mathpzc{KhA}$ are also valid under
$\mathrm{LTS}$ semantics (Proposition 10). In fact, the next section will show
that $\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$ (for
$\mathrm{LTS}^{U}$) is strictly weaker than
$\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$ (for $\mathrm{LTS}$)..

$\begin{array}[]{l@{\quad\quad}l@{\quad}l}\hline\cr\hline\cr\mbox{\text@underline{Block
$\mathcal{L}$:}}&\mathpzc{TAUT}&\vdash\varphi\mbox{ for $\varphi$ a
propositional tautology}\\\
&\mathpzc{DISTA}&\vdash\mathsf{A}(\varphi\rightarrow\psi)\rightarrow(\mathsf{A}\varphi\rightarrow\mathsf{A}\psi)\\\
&\mathpzc{TA}&\vdash\mathsf{A}\varphi\rightarrow\varphi\\\
&\mathpzc{4KhA}&\vdash\mathsf{Kh}_{i}(\psi,\varphi)\rightarrow\mathsf{A}\mathsf{Kh}_{i}(\psi,\varphi)\\\
&\mathpzc{5KhA}&\vdash\neg\mathsf{Kh}_{i}(\psi,\varphi)\rightarrow\mathsf{A}\neg\mathsf{Kh}_{i}(\psi,\varphi)\\\
&\mathpzc{MP}&\mbox{From $\vdash\varphi$ and $\vdash\varphi\rightarrow\psi$
infer $\vdash\psi$ }\\\ &\mathpzc{NECA}&\mbox{From $\vdash\varphi$ infer
$\vdash\mathsf{A}\varphi$}\\\ \hline\cr\mbox{\text@underline{Block
$\mathcal{L}_{\\_}{\mathrm{LTS}^{U}}$:}}&\mathpzc{KhE}&\vdash\left(\mathsf{E}\psi\land\mathsf{Kh}_{i}(\psi,\varphi)\right)\rightarrow\mathsf{E}\varphi\\\
&\mathpzc{KhA}&\vdash\left(\mathsf{A}(\chi\rightarrow\psi)\land\mathsf{Kh}_{i}(\psi,\varphi)\land\mathsf{A}(\varphi\rightarrow\theta)\right)\rightarrow\mathsf{Kh}_{i}(\chi,\theta)\\\
\hline\cr\hline\cr\end{array}$ Table 2: Axioms
$\mathcal{L}_{\\_}{\mathrm{LTS}^{U}}$, for $\mathsf{L}_{\mathsf{Kh}_{i}}$
w.r.t. ${\mathrm{LTS}^{U}}s$ .

We should start by discussing the newly introduced axioms. On the one hand,
axiom $\mathpzc{KhA}$ can be subjected to some of the criticisms that apply to
$\mathpzc{EMP}$ and $\mathpzc{COMPKh}$ but, in our opinion, to a lesser
extent. It implies certain level of idealization, as it entails that the
abilities of the agent are, in a sense, closed under global entailment. On the
other hand, axiom $\mathpzc{KhE}$ states a simple reasonable requirement: if
$\mathsf{Kh}_{i}(\psi,\varphi)$ is not trivial (given that $\mathsf{E}\psi$
holds), then $\mathsf{E}\varphi$ should be assured.

Define the system $\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$ :=
$\mathcal{L}$ (first block of Table 2) + $\mathcal{L}_{\\_}{\mathrm{LTS}^{U}}$
(second block of Table 2). Now we will show that
$\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$ is sound and strongly
complete for $\mathsf{L}_{\mathsf{Kh}_{i}}$ over $\mathrm{LTS}^{U}$s. Proving
soundness is rather straightforward, so we will focus on strong completeness.
Following [9, Proposition 4.12], the strategy is to build, for any
$\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$-consistent set of formulas,
an $\mathrm{LTS}^{U}$ satisfying them. In particular, the notions of
theoremhood, (local) consequence, inconsistency, and maximally consistent sets
are defined as usual [9]. We will rely on ideas from [57, 59]; the following
theorems will be useful.

######  Proposition 4.

Formulas $\mathsf{A}\lnot\psi\rightarrow\mathsf{Kh}_{i}(\psi,\varphi)$ (called
$\mathpzc{SCOND}$) and $\mathsf{Kh}_{i}(\bot,\varphi)$ (called
$\mathpzc{COND}$) are
$\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$-derivable. That is,  (1)
$\vdash\mathsf{A}\lnot\psi\rightarrow\mathsf{Kh}_{i}(\psi,\varphi)$and  (2)
$\vdash\mathsf{Kh}_{i}(\bot,\varphi)$ .

######  Proof..

(1) Take
$\vdash\mathsf{A}(\psi\rightarrow\psi)\rightarrow\left(\mathsf{A}(\bot\rightarrow\varphi)\rightarrow(\mathsf{Kh}_{i}(\psi,\bot)\rightarrow\mathsf{Kh}_{i}(\psi,\varphi))\right)$,
an instance of $\mathpzc{KhA}$. Using $\mathpzc{TAUT}$ and $\mathpzc{NECA}$ we
get $\vdash\mathsf{A}(\psi\rightarrow\psi)$; analogously, we get
$\vdash\mathsf{A}(\bot\rightarrow\varphi)$. Then, using $\mathpzc{MP}$ twice
yields
$\vdash\mathsf{Kh}_{i}(\psi,\bot)\rightarrow\mathsf{Kh}_{i}(\psi,\varphi)$,
which by $\mathsf{A}$’s definition is
$\vdash\mathsf{A}\lnot\psi\rightarrow\mathsf{Kh}_{i}(\psi,\varphi)$.  (2) Take
$\vdash\mathsf{A}\lnot\bot\rightarrow\mathsf{Kh}_{i}(\bot,\varphi)$, an
instance of the previous item. Using $\mathpzc{TAUT}$ and $\mathpzc{NECA}$ we
get $\vdash\mathsf{A}\lnot\bot$ so, by $\mathpzc{MP}$,
$\vdash\mathsf{Kh}_{i}(\bot,\varphi)$.

$\blacksquare$

$\triangleleft$

Here it is, then, the definition of the required $\mathrm{LTS}^{U}$.

######  Definition 6.1.

Let $\bm{\Upphi}$ be the set of all maximally
$\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$-consistent sets (MCS) of
formulas in $\mathsf{L}_{\mathsf{Kh}_{i}}$. For any $\Delta\in\bm{\Upphi}$,
define

$\begin{array}[]{r@{\;:=\;}l@{\qquad\qquad}r@{\;:=\;}l}\Delta|_{\mathsf{Kh}_{i}}&\\{\xi\in\Delta\mid\xi\;\text{is
of the
form}\;\mathsf{Kh}_{i}(\psi,\varphi)\\},&\Delta|_{\mathsf{Kh}}&\bigcup_{\\_}{i\in{\rm\sf
Agt}}\Delta|_{\mathsf{Kh}_{i}}.\\\
\Delta|_{\lnot\mathsf{Kh}_{i}}&\\{\xi\in\Delta\mid\xi\;\text{is of the
form}\;\lnot\mathsf{Kh}_{i}(\psi,\varphi)\\},&\Delta|_{\lnot\mathsf{Kh}}&\bigcup_{\\_}{i\in{\rm\sf
Agt}}\Delta|_{\lnot\mathsf{Kh}_{i}}.\\\ \end{array}$

Let $\Gamma$ be a set in $\bm{\Upphi}$; we will define a structure satisfying
its formulas. Define a set of basic actions ${\rm\sf
Act}^{\Gamma}_{\\_}i:=\\{\langle\psi,\varphi\rangle\mid\mathsf{Kh}_{i}(\psi,\varphi)\in\Gamma\\}$
associated to each agent $i\in{\rm\sf Agt}$, and then their union ${\rm\sf
Act}^{\Gamma}:=\bigcup_{\\_}{i\in{\rm\sf Agt}}{\rm\sf Act}^{\Gamma}_{\\_}i$.
Notice that $\mathsf{Kh}_{i}(\bot,\varphi)\in\Gamma$ for every $i\in{\rm\sf
Agt}$ and every $\varphi\in\mathsf{L}_{\mathsf{Kh}_{i}}$ (by
$\mathpzc{COND}$); since ${\rm\sf Agt}$ is finite and non-empty, this implies
that ${\rm\sf Act}^{\Gamma}$ is denumerable, and thus it is an adequate set of
actions for building a model. It is worth noticing that ${\rm\sf
Act}^{\Gamma}$ fixes a new signature. However, since the operators of the
language cannot talk explicitly about the names of the actions, we can define
a mapping from ${\rm\sf Act}^{\Gamma}$ to any particular ${\rm\sf Act}$, to
preserve the original signature, provided that the cardinalities match.

Then, the structure
$\mathcal{M}^{\Gamma}=\langle\mathrm{W}^{\Gamma},\mathrm{R}^{\Gamma},\\{\mathrm{S}^{\Gamma}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}^{\Gamma}\rangle$ over ${\rm\sf Act}^{\Gamma}$, ${\rm\sf Agt}$
and ${\rm\sf Prop}$ is defined as follows.

  * •

$\mathrm{W}^{\Gamma}:=\\{\Delta\in\bm{\Upphi}\mid\Delta|_{\mathsf{Kh}}=\Gamma|_{\mathsf{Kh}}\\}$.

  * •

$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle}:=\bigcup_{\\_}{i\in{\rm\sf
Agt}}\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle^{i}}$, with

$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle^{i}}:=\\{(\Delta_{\\_}1,\Delta_{\\_}2)\in\mathrm{W}^{\Gamma}\times\mathrm{W}^{\Gamma}\mid\mathsf{Kh}_{i}(\psi,\varphi)\in\Gamma,\psi\in\Delta_{\\_}1,\varphi\in\Delta_{\\_}2\\}$.

  * •

$\mathrm{S}^{\Gamma}_{\\_}i:=\left\\{\\{\langle\psi,\varphi\rangle\\}\mid\langle\psi,\varphi\rangle\in{\rm\sf
Act}^{\Gamma}_{\\_}i\right\\}$.

  * •

$\mathrm{V}^{\Gamma}(\Delta):=\\{p\in{\rm\sf Prop}\mid p\in\Delta\\}$.

$\dashv$

Since $\Gamma\in\bm{\Upphi}$, the structure $\mathcal{M}^{\Gamma}$ is of the
required type, as the following proposition states.

######  Proposition 5.

The structure
$\mathcal{M}^{\Gamma}=\langle\mathrm{W}^{\Gamma},\mathrm{R}^{\Gamma},\\{\mathrm{S}^{\Gamma}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}^{\Gamma}\rangle$ is an $\mathrm{LTS}^{U}$.

######  Proof..

It is enough to show that each $\mathrm{S}^{\Gamma}_{\\_}i$ defines a
partition over a non-empty subset of $2^{({\rm\sf Act}^{*})}$. First,
$\mathpzc{COND}$ implies $\mathsf{Kh}_{i}(\bot,\bot)\in\Gamma$, so
$\langle\bot,\bot\rangle\in{\rm\sf Act}^{\Gamma}_{\\_}i$ and hence
$\\{\langle\bot,\bot\rangle\\}\in\mathrm{S}^{\Gamma}_{\\_}i$; thus,
$\bigcup_{\\_}{\uppi\in\mathrm{S}_{\\_}i}\uppi\neq\varnothing$. Then,
$\mathrm{S}_{\\_}i$ indeed defines a partition over
$\bigcup_{\\_}{\uppi\in\mathrm{S}_{\\_}i}\uppi$: its elements are mutually
disjoint (they are singletons with different elements), collective
exhaustiveness is immediate and, finally,
$\varnothing\notin\mathrm{S}^{\Gamma}_{\\_}i$. $\blacksquare$

$\triangleleft$

Let $\Gamma\in\bm{\Upphi}$; the following properties of $\mathcal{M}^{\Gamma}$
will be useful (proofs are similar to the ones in [59]).

######  Proposition 6.

For any $\Delta_{\\_}1,\Delta_{\\_}2\in\mathrm{W}^{\Gamma}$ we have
$\Delta_{\\_}1|_{\mathsf{Kh}}=\Delta_{\\_}2|_{\mathsf{Kh}}$.

######  Proof..

Straightforward from the definition of $\mathrm{W}^{\Gamma}$. $\blacksquare$

$\triangleleft$

######  Proposition 7.

Take $\Delta\in\mathrm{W}^{\Gamma}$. If $\Delta$ has a
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle}$-successor, then every
$\Delta^{\prime}\in\mathrm{W}^{\Gamma}$ with $\varphi\in\Delta^{\prime}$ can
be $\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle}$-reached from
$\Delta$.

######  Proof..

If $\Delta$ has a
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle}$-successor, then it has
a $\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle^{i}}$-successor for
some $i\in{\rm\sf Agt}$; thus, $\psi\in\Delta$ and
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Gamma$. Hence, every
$\Delta^{\prime}\in\mathrm{W}^{\Gamma}$ with $\varphi\in\Delta^{\prime}$ is
such that
$(\Delta,\Delta^{\prime})\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle^{i}}$,
and thus such that
$(\Delta,\Delta^{\prime})\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle}$.
$\blacksquare$

$\triangleleft$

######  Proposition 8.

Let $\varphi$ be an $\mathsf{L}_{\mathsf{Kh}_{i}}$-formula. If
$\varphi\in\Delta$ for every $\Delta\in\mathrm{W}^{\Gamma}$, then
$\mathsf{A}\varphi\in\Delta$ for every $\Delta\in\mathrm{W}^{\Gamma}$.

######  Proof..

First, some facts for any $\Delta$ in
$\mathrm{W}^{\Gamma}\subseteq\bm{\Upphi}$. By definition,
$\Delta|_{\mathsf{Kh}}\cup\Delta|_{\lnot\mathsf{Kh}}$ is a subset of $\Delta$,
and therefore it is consistent. Moreover: any maximally consistent extension
of $\Delta|_{\mathsf{Kh}}\cup\Delta|_{\lnot\mathsf{Kh}}$, say
$\Delta^{\prime}$, should satisfy
$\Delta|_{\mathsf{Kh}}=\Delta^{\prime}|_{\mathsf{Kh}}$. For
$\bm{(\subseteq)}$, note that
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Delta|_{\mathsf{Kh}}$ implies
$\mathsf{Kh}_{i}(\psi,\varphi)\in(\Delta|_{\mathsf{Kh}}\cup\Delta|_{\lnot\mathsf{Kh}})$,
and thus $\mathsf{Kh}_{i}(\psi,\varphi)\in\Delta^{\prime}$, i.e.,
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Delta^{\prime}|_{\mathsf{Kh}}$. For
$\bm{(\supseteq)}$, use the contrapositive. If
$\mathsf{Kh}_{i}(\psi,\varphi)\not\in\Delta|_{\mathsf{Kh}}$ then
$\mathsf{Kh}_{i}(\psi,\varphi)\not\in\Delta$, so
$\lnot\mathsf{Kh}_{i}(\psi,\varphi)\in\Delta$ (as $\Delta$ is an MCS). Thus,
$\lnot\mathsf{Kh}_{i}(\psi,\varphi)\in(\Delta|_{\mathsf{Kh}}\cup\Delta|_{\lnot\mathsf{Kh}})$
and hence $\lnot\mathsf{Kh}_{i}(\psi,\varphi)\in\Delta^{\prime}$; therefore,
$\mathsf{Kh}_{i}(\psi,\varphi)\not\in\Delta^{\prime}$ (as $\Delta$ is
consistent) and thus
$\mathsf{Kh}_{i}(\psi,\varphi)\not\in\Delta^{\prime}|_{\mathsf{Kh}}$.

For the proof of the proposition, suppose $\varphi\in\Delta$ for every
$\Delta\in\mathrm{W}^{\Gamma}$. Take any $\Delta\in\mathrm{W}^{\Gamma}$, and
note how $\Delta|_{\mathsf{Kh}}=\Gamma|_{\mathsf{Kh}}$. Then, the set
$\Delta|_{\mathsf{Kh}}\cup\Delta|_{\lnot\mathsf{Kh}}\cup\\{\lnot\varphi\\}$ is
inconsistent. Otherwise it could be extended into an MCS
$\Delta^{\prime}\in\bm{\Upphi}$. By the result in the previous paragraph, this
would imply $\Delta^{\prime}|_{\mathsf{Kh}}=\Delta|_{\mathsf{Kh}}$, so
$\Delta^{\prime}|_{\mathsf{Kh}}=\Gamma|_{\mathsf{Kh}}$ and therefore
$\Delta^{\prime}\in\mathrm{W}^{\Gamma}$. But then, by the assumption,
$\varphi\in\Delta^{\prime}$, and by construction,
$\lnot\varphi\in\Delta^{\prime}$. This would make $\Delta^{\prime}$
inconsistent, a contradiction.

Thus, given that
$\Delta|_{\mathsf{Kh}}\cup\Delta|_{\lnot\mathsf{Kh}}\cup\\{\lnot\varphi\\}$ is
inconsistent, there should be sets
$\\{\mathsf{Kh}_{\\_}{b_{\\_}1}(\psi_{\\_}1,\varphi_{\\_}1),\ldots,\mathsf{Kh}_{\\_}{b_{\\_}n}(\psi_{\\_}n,\varphi_{\\_}n)\\}\subseteq\Delta|_{\mathsf{Kh}}$
and
$\\{\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}1}(\psi^{\prime}_{\\_}1,\varphi^{\prime}_{\\_}1),\ldots,\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}m}(\psi^{\prime}_{\\_}m,\varphi^{\prime}_{\\_}m)\\}\subseteq\Delta|_{\lnot\mathsf{Kh}}$
such that

$\vdash\displaystyle\left(\bigwedge_{\\_}{k=1}^{n}\mathsf{Kh}_{\\_}{b_{\\_}k}(\psi_{\\_}k,\varphi_{\\_}k)\land\bigwedge_{\\_}{k=1}^{m}\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}k}(\psi^{\prime}_{\\_}k,\varphi^{\prime}_{\\_}k)\right)\rightarrow\varphi$.
---

Hence, by $\mathpzc{NECA}$,

$\vdash\displaystyle\mathsf{A}\left(\left(\bigwedge_{\\_}{k=1}^{n}\mathsf{Kh}_{\\_}{b_{\\_}k}(\psi_{\\_}k,\varphi_{\\_}k)\land\bigwedge_{\\_}{k=1}^{m}\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}k}(\psi^{\prime}_{\\_}k,\varphi^{\prime}_{\\_}k)\right)\rightarrow\varphi\right)$
---

and then, by $\mathpzc{DISTA}$ and $\mathpzc{MP}$,

$\vdash\displaystyle\mathsf{A}\left(\bigwedge_{\\_}{k=1}^{n}\mathsf{Kh}_{\\_}{b_{\\_}k}(\psi_{\\_}k,\varphi_{\\_}k)\land\bigwedge_{\\_}{k=1}^{m}\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}k}(\psi^{\prime}_{\\_}k,\varphi^{\prime}_{\\_}k)\right)\rightarrow\mathsf{A}\varphi$.
---

Now,
$\mathsf{Kh}_{\\_}{b_{\\_}k}(\psi_{\\_}k,\varphi_{\\_}k)\in\Delta|_{\mathsf{Kh}}$
implies ($\mathpzc{4KhA}$ and $\mathpzc{MP}$) that
$\mathsf{A}\mathsf{Kh}_{\\_}{b_{\\_}k}(\psi_{\\_}k,\varphi_{\\_}k)\in\Delta$
(for each $k\in[1\mathbin{\ldotp\\!\ldotp}n]$). Similarly,
$\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}k}(\psi^{\prime}_{\\_}k,\varphi^{\prime}_{\\_}k)\in\Delta|_{\mathsf{Kh}}$
implies ($\mathpzc{5KhA}$ and $\mathpzc{MP}$) that
$\mathsf{A}\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}k}(\psi^{\prime}_{\\_}k,\varphi^{\prime}_{\\_}k)\in\Delta$
(for each $k\in[1\mathbin{\ldotp\\!\ldotp}m]$). Thus,

$\displaystyle\bigwedge_{\\_}{k=1}^{n}\mathsf{A}\mathsf{Kh}_{\\_}{b_{\\_}k}(\psi_{\\_}k,\varphi_{\\_}k)\in\Delta\qquad\text{and}\qquad\bigwedge_{\\_}{k=1}^{m}\mathsf{A}\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}k}(\psi^{\prime}_{\\_}k,\varphi^{\prime}_{\\_}k)\in\Delta$
---

and hence

$\displaystyle\bigwedge_{\\_}{k=1}^{n}\mathsf{A}\mathsf{Kh}_{\\_}{b_{\\_}k}(\psi_{\\_}k,\varphi_{\\_}k)\land\bigwedge_{\\_}{k=1}^{m}\mathsf{A}\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}k}(\psi^{\prime}_{\\_}k,\varphi^{\prime}_{\\_}k)\in\Delta,\,\text{so}\,\mathsf{A}\left(\bigwedge_{\\_}{k=1}^{n}\mathsf{Kh}_{\\_}{b_{\\_}k}(\psi_{\\_}k,\varphi_{\\_}k)\land\bigwedge_{\\_}{k=1}^{m}\lnot\mathsf{Kh}_{\\_}{b^{\prime}_{\\_}k}(\psi^{\prime}_{\\_}k,\varphi^{\prime}_{\\_}k)\right)\in\Delta$
---

and therefore $\mathsf{A}\varphi\in\Delta$. $\blacksquare$

$\triangleleft$

######  Proposition 9.

Take $\psi,\psi^{\prime},\varphi^{\prime}$ in $\mathsf{L}_{\mathsf{Kh}_{i}}$.
Suppose that every $\Delta\in\mathrm{W}^{\Gamma}$ with $\psi\in\Delta$ has a
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}$-successor.
Then, $\mathsf{A}(\psi\rightarrow\psi^{\prime})\in\Delta$ for all
$\Delta\in\mathrm{W}^{\Gamma}$.

######  Proof..

Take any $\Delta\in\mathrm{W}^{\Gamma}$. On the one hand, if $\psi\in\Delta$
then, by the supposition,
$(\Delta,\Delta^{\prime})\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}$
for some $\Delta^{\prime}$. Hence, from
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}$’s
definition, $\psi^{\prime}\in\Delta$ and thus (maximal consistency)
$\psi\rightarrow\psi^{\prime}\in\Delta$. On the other hand, if
$\psi\not\in\Delta$ then $\lnot\psi\in\Delta$ (again, maximal consistency) and
thus $\psi\rightarrow\psi^{\prime}\in\Delta$. Thus,
$\psi\rightarrow\psi^{\prime}\in\Delta$ for every
$\Delta\in\mathrm{W}^{\Gamma}$; then, by Proposition 8,
$\mathsf{A}(\psi\rightarrow\psi^{\prime})\in\Delta$ for every
$\Delta\in\mathrm{W}^{\Gamma}$. $\blacksquare$

$\triangleleft$

With these properties at hand, we can prove the truth lemma for
$\mathcal{M}^{\Gamma}$.

######  Lemma 1 (Truth lemma for $\mathcal{M}^{\Gamma}$).

Given $\Gamma\\!\in\\!\bm{\Upphi}$, take
$\mathcal{M}^{\Gamma}=\langle\mathrm{W}^{\Gamma},\mathrm{R}^{\Gamma},\\{\mathrm{S}^{\Gamma}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}^{\Gamma}\rangle$. Then, for every
$\Theta\in\mathrm{W}^{\Gamma}$ and every
$\varphi\in\mathsf{L}_{\mathsf{Kh}_{i}}$,

$\mathcal{M}^{\Gamma},\Theta\models\varphi$ if and only if |  $\varphi\in\Theta$.
---|---

######  Proof..

The proof is by induction on $\varphi$. The atom and Boolean cases as usual,
so we focus on the _knowing how_ case.

1

Case $\bm{\mathsf{Kh}_{i}(\psi,\varphi)}$. $\bm{(\Rightarrow)}$ Suppose
$\mathcal{M}^{\Gamma},\Theta\models\mathsf{Kh}_{i}(\psi,\varphi)$, and
consider two cases.

  * •

$\bm{\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}=\varnothing}$. Then, each
$\Delta\in\mathrm{W}^{\Gamma}$ is such that
$\Delta\not\in\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$, which implies
$\psi\not\in\Delta$ (by IH) and thus $\lnot\psi\in\Delta$ (by maximal
consistency). Hence, by Proposition 8, $\mathsf{A}\lnot\psi\in\Delta$ for
every $\Delta\in\mathrm{W}^{\Gamma}$. In particular,
$\mathsf{A}\lnot\psi\in\Theta$ and thus, by $\mathpzc{SCOND}$ and
$\mathpzc{MP}$, $\mathsf{Kh}_{i}(\psi,\varphi)\in\Theta$.

  * •

$\bm{\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing}$. From
$\mathcal{M}^{\Gamma},\Theta\models\mathsf{Kh}_{i}(\psi,\varphi)$, there is
$\\{\langle\psi^{\prime},\varphi^{\prime}\rangle\\}\in\mathrm{S}^{\Gamma}_{\\_}i$
such that

($\bm{\mathsf{Kh}}$-1)
$\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}\subseteq\mathrm{SE}(\\{\langle\psi^{\prime},\varphi^{\prime}\rangle\\})$and
($\bm{\mathsf{Kh}}$-2)
$\mathrm{R}^{\Gamma}_{\\_}{\\{\langle\psi^{\prime},\varphi^{\prime}\rangle\\}}(\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}^{\Gamma}}$

.

In other words, there is
$\langle\psi^{\prime},\varphi^{\prime}\rangle\in{\rm\sf Act}^{\Gamma}_{\\_}a$
such that

    1. ($\bm{\mathsf{Kh}}$-1)

for all $\Delta\in\mathrm{W}^{\Gamma}$, if
$\Delta\in\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$ then
$\Delta\in\mathrm{SE}(\\{\langle\psi^{\prime},\varphi^{\prime}\rangle\\})$, so
$\Delta\in\mathrm{SE}(\langle\psi^{\prime},\varphi^{\prime}\rangle)$ and
therefore $\Delta$ has a
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}$-successor.

    2. ($\bm{\mathsf{Kh}}$-2)

for all $\Delta^{\prime}\in\mathrm{W}^{\Gamma}$, if
$\Delta^{\prime}\in\mathrm{R}^{\Gamma}_{\\_}{\\{\langle\psi^{\prime},\varphi^{\prime}\rangle\\}}(\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}})$
then $\Delta^{\prime}\in\llbracket\varphi\rrbracket^{\mathcal{M}^{\Gamma}}$.

This case requires three pieces.

    1. (1)

Take any $\Delta\in\mathrm{W}^{\Gamma}$ with $\psi\in\Delta$. Then, by IH,
$\Delta\in\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$ and thus, by
($\bm{\mathsf{Kh}}$-1), $\Delta$ has a
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}$-successor.
Thus, every $\Delta\in\mathrm{W}^{\Gamma}$ with $\psi\in\Delta$ has such
successor; then (Proposition 9), it follows that
$\mathsf{A}(\psi\rightarrow\psi^{\prime})\in\Delta$ for every
$\Delta\in\mathrm{W}^{\Gamma}$. In particular,
$\mathsf{A}(\psi\rightarrow\psi^{\prime})\in\Theta$.

    2. (2)

From $\langle\psi^{\prime},\varphi^{\prime}\rangle\in{\rm\sf
Act}^{\Gamma}_{\\_}i$ it follows that
$\mathsf{Kh}_{i}(\psi^{\prime},\varphi^{\prime})\in\Gamma$. But
$\Theta\in\mathrm{W}^{\Gamma}$, so
$\Theta|_{\mathsf{Kh}}=\Gamma|_{\mathsf{Kh}}$ (by definition of
$\mathrm{W}^{\Gamma}$). Hence,
$\mathsf{Kh}_{i}(\psi^{\prime},\varphi^{\prime})\in\Theta$.

    3. (3)

Since $\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing$, there
is $\Delta\in\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$. By
($\bm{\mathsf{Kh}}$-1), $\Delta$ should have at least one
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}$-successor.
Then, by Proposition 7, every $\Delta^{\prime}\in\mathrm{W}^{\Gamma}$
satisfying $\varphi^{\prime}\in\Delta^{\prime}$ can be
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}$-reached
from $\Delta$; in other words, every $\Delta^{\prime}\in\mathrm{W}^{\Gamma}$
satisfying $\varphi^{\prime}\in\Delta^{\prime}$ is in
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}(\Delta)$.
But $\Delta\in\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$, so every
$\Delta^{\prime}\in\mathrm{W}^{\Gamma}$ satisfying
$\varphi^{\prime}\in\Delta^{\prime}$ is in
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi^{\prime},\varphi^{\prime}\rangle}(\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}})$.
Then, by ($\bm{\mathsf{Kh}}$-2), every $\Delta^{\prime}\in\mathrm{W}^{\Gamma}$
satisfying $\varphi^{\prime}\in\Delta^{\prime}$ is in
$\llbracket\varphi\rrbracket^{\mathcal{M}^{\Gamma}}$. By IH on the latter
part, every $\Delta^{\prime}\in\mathrm{W}^{\Gamma}$ satisfying
$\varphi^{\prime}\in\Delta^{\prime}$ is such that $\varphi\in\Delta^{\prime}$.
Thus, $\varphi^{\prime}\rightarrow\varphi\in\Delta^{\prime}$ for every
$\Delta^{\prime}\in\mathrm{W}^{\Gamma}$, and hence (Proposition 8)
$\mathsf{A}(\varphi^{\prime}\rightarrow\varphi)\in\Delta^{\prime}$ for every
$\Delta^{\prime}\in\mathrm{W}^{\Gamma}$. In particular,
$\mathsf{A}(\varphi^{\prime}\rightarrow\varphi)\in\Theta$.

Thus,
$\\{\mathsf{A}(\psi\rightarrow\psi^{\prime}),\mathsf{Kh}_{i}(\psi^{\prime},\varphi^{\prime}),\mathsf{A}(\varphi^{\prime}\rightarrow\varphi)\\}\subset\Theta$.
Therefore, by $\mathpzc{KhA}$ and $\mathpzc{MP}$,
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Theta$.

$\bm{(\Leftarrow)}$ Suppose $\mathsf{Kh}_{i}(\psi,\varphi)\in\Theta$. Thus
(Proposition 6), $\mathsf{Kh}_{i}(\psi,\varphi)\in\Gamma$, so
$\langle\psi,\varphi\rangle\in{\rm\sf Act}^{\Gamma}_{\\_}i$ and therefore
$\\{\langle\psi,\varphi\rangle\\}\in\mathrm{S}^{\Gamma}_{\\_}i$. The rest of
the proof is split into two cases.

  * •

Suppose there is no $\Delta_{\\_}\psi\in\mathrm{W}^{\Gamma}$ with
$\psi\in\Delta$. Then, by IH, there is no
$\Delta_{\\_}\psi\in\mathrm{W}^{\Gamma}$ with
$\Delta_{\\_}\psi\in\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$, that is,
$\llbracket\lnot\psi\rrbracket^{\mathcal{M}^{\Gamma}}=\mathrm{D}_{\mathrm{W}^{\Gamma}}$.
Since $\mathcal{M}^{\Gamma}$ is an $\mathrm{LTS}^{U}$ (Proposition 5), the
latter yields $(\mathcal{M}^{\Gamma},\Delta)\models\mathsf{Kh}_{i}(\psi,\chi)$
for any $i\in{\rm\sf Agt}$, $\chi\in\mathsf{L}_{\mathsf{Kh}_{i}}$ and
$\Delta\in\mathrm{W}^{\Gamma}$ (cf. Proposition 2); hence,
$(\mathcal{M}^{\Gamma},\Theta)\models\mathsf{Kh}_{i}(\psi,\varphi)$.

  * •

Suppose there is $\Delta_{\\_}\psi\in\mathrm{W}^{\Gamma}$ with
$\psi\in\Delta_{\\_}\psi$. It will be shown that the set of plans
$\\{\langle\psi,\varphi\rangle\\}\in\mathrm{S}^{\Gamma}_{\\_}i$ satisfies the
requirements.

    1. ($\bm{\mathsf{Kh}}$-1)

Take any $\Delta\in\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$. By IH,
$\psi\in\Delta$. Moreover, from $\mathsf{Kh}_{i}(\psi,\varphi)\in\Theta$ and
Proposition 6 it follows that $\mathsf{Kh}_{i}(\psi,\varphi)\in\Delta$. Then,
from $\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle^{i}}$’s definition,
every $\Delta^{\prime}\in\mathrm{W}^{\Gamma}$ with $\varphi\in\Delta^{\prime}$
is such that
$(\Delta,\Delta^{\prime})\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle^{i}}$,
and therefore such that
$(\Delta,\Delta^{\prime})\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle}$.
Now note how, since there is $\Delta_{\\_}\psi\in\mathrm{W}^{\Gamma}$ with
$\psi\in\Delta_{\\_}\psi$, there should be
$\Delta_{\\_}\varphi\in\mathrm{W}^{\Gamma}$ with
$\varphi\in\Delta_{\\_}\varphi$. Suppose otherwise, i.e., suppose there is no
$\Delta^{\prime\prime}\in\mathrm{W}^{\Gamma}$ with
$\varphi\in\Delta^{\prime\prime}$. Then,
$\lnot\varphi\in\Delta^{\prime\prime}$ for every
$\Delta^{\prime\prime}\in\mathrm{W}^{\Gamma}$, and hence (Proposition 8)
$\mathsf{A}\lnot\varphi\in\Delta^{\prime\prime}$ for every
$\Delta^{\prime\prime}\in\mathrm{W}^{\Gamma}$. In particular,
$\mathsf{A}\lnot\varphi\in\Delta_{\\_}\psi$. Moreover, from
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Theta$ and Proposition 6 it follows that
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Delta_{\\_}\psi$. Then, $\mathpzc{KhE}$
(written as
$\mathsf{Kh}_{i}(\psi,\varphi)\rightarrow(\mathsf{A}\lnot\varphi\rightarrow\mathsf{A}\lnot\psi)$)
and $\mathpzc{MP}$ yield $\mathsf{A}\lnot\psi\in\Delta_{\\_}\psi$, and thus
(axiom $\mathpzc{TA}$) $\lnot\psi\in\Delta_{\\_}\psi$. Hence,
$\\{\psi,\lnot\psi\\}\subset\Delta_{\\_}\psi$, contradicting
$\Delta_{\\_}\psi$’s consistency.

Let us continue with the proof of the lemma. The existence of
$\Delta_{\\_}\varphi\in\mathrm{W}^{\Gamma}$ with
$\varphi\in\Delta_{\\_}\varphi$ implies that
$(\Delta,\Delta_{\\_}\varphi)\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle}$
and thus, since $\langle\psi,\varphi\rangle$ is a basic action,
$\Delta\in\mathrm{SE}(\langle\psi,\varphi\rangle)$, and so
$\Delta\in\mathrm{SE}(\\{\langle\psi,\varphi\rangle\\})$. Since $\Delta$ is an
arbitrary state in $\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$, the
required
$\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}\subseteq\mathrm{SE}(\\{\langle\psi,\varphi\rangle\\})$
follows.

    2. ($\bm{\mathsf{Kh}}$-2)

Take any
$\Delta^{\prime}\in\mathrm{R}^{\Gamma}_{\\_}{\\{\langle\psi,\varphi\rangle\\}}(\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}})$.
Then, there is $\Delta\in\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}}$ such
that
$(\Delta,\Delta^{\prime})\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi,\varphi\rangle}$.
By definition of $\mathrm{R}^{\Gamma}$, it follows that
$\varphi\in\Delta^{\prime}$ so, by IH,
$\Delta^{\prime}\in\llbracket\varphi\rrbracket^{\mathcal{M}^{\Gamma}}$. Since
$\Delta^{\prime}$ is an arbitrary state in
$\mathrm{R}^{\Gamma}_{\\_}{\\{\langle\psi,\varphi\rangle\\}}(\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}})$,
the required
$\mathrm{R}^{\Gamma}_{\\_}{\\{\langle\psi,\varphi\rangle\\}}(\llbracket\psi\rrbracket^{\mathcal{M}^{\Gamma}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}^{\Gamma}}$
follows.

$\blacksquare$

$\triangleleft$

Finally, we present the intended result.

######  Theorem 4.

The axiom system $\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$ (Table 2)
is sound and strongly complete for $\mathsf{L}_{\mathsf{Kh}_{i}}$ w.r.t. the
class of all ${\mathrm{LTS}^{U}}s$.

######  Proof..

For soundness, it is enough to show that the system’s axioms are valid and
that its rules preserve validity (which, as mentioned before, is
straightforward). For completeness, take any
$\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$-consistent set of formulas
$\Gamma^{\prime}\subseteq\mathsf{L}_{\mathsf{Kh}_{i}}$. Since
$\mathsf{L}_{\mathsf{Kh}_{i}}$ is enumerable, $\Gamma^{\prime}$ can be
extended into a maximally
$\mathcal{L}^{\mathrm{LTS}^{U}}_{\mathsf{Kh}_{i}}$-consistent set
$\Gamma\supseteq\Gamma^{\prime}$ by a standard Lindenbaum’s construction (see,
e.g., [9, Lemma 4.17]). By Lemma 1, $\Gamma^{\prime}$ is satisfiable in
$\mathcal{M}^{\Gamma}$ at $\Gamma$. The fact that $\mathcal{M}^{\Gamma}$ is an
$\mathrm{LTS}^{U}$ (Proposition 5) completes the proof. $\blacksquare$

$\triangleleft$

One detail in the construction of the canonical model might be surprising:
each set of indistinguishable plans for a given agent is a singleton set.
Hence, the logic is also complete with respect to this particular class of
models. On the other hand, ${\mathrm{LTS}^{U}}s$ are a more general and
accurate representation from a conceptual point of view. We could, for
instance, extend the language so that this representation is also reflected by
the logic (i.e., the language can explicitly refer to plans), or define public
announcements-like modalities to refine the indistinguishability relation of
each agent (see, e.g., [4]).

##  7 Expressive power

This section compares the original logic from [57, 58, 59] with the one
introduced in this paper. More precisely, first it will be shown that our
logic is weaker than the original one. Then, we will explore two different
classes of $\mathrm{LTS}^{U}$s under which we can capture the exact semantics
of [57, 58, 59]. As a consequence, the axiom system in Table 1 is sound and
complete for these two classes of models. This shows that our framework
generalizes the one based on $\mathrm{LTS}$s.

For the comparison to be meaningful, we will restrict the $\mathrm{LTS}^{U}$
setting to its single-agent case: a single modality $\mathsf{Kh}$ and no
subindexes for $\mathrm{P}_{i}$ and $\mathrm{S}_{\\_}i$.

The provided axiom system can be used to compare the notion of _knowing how_
under $\mathrm{LTS}$s with that under $\mathrm{LTS}^{U}$s. Here is a first
observation.

######  Proposition 10.

$\mathpzc{KhE}$ and $\mathpzc{KhA}$ are theorems of
$\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$.

######  Proof..

$\mathpzc{KhE}$ can be rewritten as
$\left(\mathsf{Kh}(\psi,\varphi)\land\mathsf{A}\lnot\varphi\right)\rightarrow\mathsf{A}\lnot\psi$,
which is an instance of $\mathpzc{COMPKh}$ in
$\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$ (just unfold $\mathsf{A}$). For
$\mathpzc{KhA}$, use $\mathpzc{EMP}$ and then $\mathpzc{COMPKh}$ [59,
Proposition 2]. $\blacksquare$

$\triangleleft$

Hence, the _knowing how_ operator under $\mathrm{LTS}$s is at least as strong
as its $\mathrm{LTS}^{U}$-based counterpart: every formula valid under
$\mathrm{LTS}^{U}$s is also valid under $\mathrm{LTS}$s. The following fact
shows that the converse is not the case.

######  Proposition 11.

Within $\mathrm{LTS}^{U}$, axioms $\mathpzc{EMP}$ and $\mathpzc{COMPKh}$ are
not valid.

######  Proof..

Consider the $\mathrm{LTS}^{U}$ shown below, with the collection of sets of
plans for the agent (i.e., the set $\mathrm{S}$) depicted on the right. Recall
that $\mathsf{Kh}$ acts globally.

$p$$w$$q$$r$$a$$c$$b$$\mathrm{S}=\left\\{\begin{array}[]{c}\\{a\\},\
\\{b\\}\\\ \\{ab,c\\}\end{array}\right\\}$

With respect to $\mathpzc{EMP}$, notice that $\mathsf{A}(p\rightarrow p)$
holds; yet, $\mathsf{Kh}(p,p)$ fails since there is no $\uppi\in\mathrm{S}$
leading from $p$-states to $p$-states. More generally, $\mathpzc{EMP}$ is
valid over $\mathrm{LTS}$s because the empty plan $\epsilon$, strongly
executable everywhere, is always available. However, in an $\mathrm{LTS}^{U}$,
the plan $\epsilon$ might not be available to the agent (i.e.,
$\epsilon\notin\mathrm{P}$), and even if it is, it might be indistinguishable
from other plans with different behaviour.

With respect to $\mathpzc{COMPKh}$, notice that $\mathsf{Kh}(p,q)$ and
$\mathsf{Kh}(q,r)$ hold, witness $\\{a\\}$ and $\\{b\\}$, respectively.
However, there is no $\uppi\in\mathrm{S}$ containing only plans that, when
started on $p$-states, lead only to $r$-states. Thus, $\mathsf{Kh}(p,r)$
fails. More generally, $\mathpzc{COMPKh}$ is valid over $\mathrm{LTS}$ because
the sequential composition of the plans that make true the conjuncts in the
antecedent is a witness that makes true the consequent. However, in an
$\mathrm{LTS}^{U}$, this composition might be unavailable or else
indistinguishable from other plans. $\blacksquare$

$\triangleleft$

From these two observations it follows that $\mathsf{Kh}$ under
${\mathrm{LTS}^{U}}s$ is strictly weaker than $\mathsf{Kh}$ under
$\mathrm{LTS}$s: adding uncertainty about plans changes the logic.

###  7.1 A very simple class of $\mathrm{LTS}^{U}$s

Still, the uncertainty-based framework is general enough to capture the
$\mathrm{LTS}$ semantics. Given the discussion in Proposition 11, there is an
obvious class of $\mathrm{LTS}^{U}$s in which $\mathpzc{EMP}$ and
$\mathpzc{COMPKh}$ are valid: the class of $\mathrm{LTS}^{U}$s in which the
agent has every plan available and can distinguish between any two of them.
Below, we define formally this class.

######  Definition 7.1.

Define the class of models:
$\bm{\mathrm{M}_{\mathrm{NU}}}:=\\{\mathcal{M}\mid\mathcal{M}\mbox{ is an
}\mathrm{LTS}^{U}\mbox{ and }\mathrm{S}=\\{\\{\sigma\\}\mid\sigma\in{\rm\sf
Act}^{*}\\}\\}$. $\dashv$

Indeed, for models in $\bm{\mathrm{M}_{\mathrm{NU}}}$, the plan $\epsilon$ is
available and distinguishable from other plans (witnessing $\mathpzc{EMP}$)
and from $\\{\sigma_{\\_}1\\}\in\mathrm{S}$ and
$\\{\sigma_{\\_}2\\}\in\mathrm{S}$ it follows that
$\\{\sigma_{\\_}1\sigma_{\\_}2\\}\in\mathrm{S}$ (witnessing
$\mathpzc{COMPKh}$). Thus, as the following proposition states, an agent in
$\mathrm{LTS}$ is exactly an agent in $\mathrm{LTS}^{U}$ that can use every
plan and has no uncertainty and full awareness about them. This class is
enough to show how the uncertainty-based framework can capture the original
one.

######  Proposition 12.

The following properties hold.

  1. (1)

Given a model
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\mathrm{S},\mathrm{V}\rangle$ in
$\bm{\mathrm{M}_{\mathrm{NU}}}$, the $\mathrm{LTS}$
$\mathcal{S}_{\\_}\mathcal{M}=\langle\mathrm{W},\mathrm{R},\mathrm{V}\rangle$
is such that
$\llbracket\varphi\rrbracket^{\mathcal{M}}=\llbracket\varphi\rrbracket^{\mathcal{S}_{\\_}{\mathcal{M}}}$
for every $\varphi\in\mathsf{L}_{\mathsf{Kh}}$.

  2. (2)

Given an $\mathrm{LTS}$
$\mathcal{S}=\langle\mathrm{W},\mathrm{R},\mathrm{V}\rangle$, the model
$\mathcal{M}_{\\_}\mathcal{S}=\langle\mathrm{W},\mathrm{R},\mathrm{S},\mathrm{V}\rangle$
with $\mathrm{S}=\\{\\{\sigma\\}\mid\sigma\in{\rm\sf Act}^{*}\\}$, is in
$\bm{\mathrm{M}_{\mathrm{NU}}}$ and is such that
$\llbracket\varphi\rrbracket^{\mathcal{S}}=\llbracket\varphi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$
for every $\varphi\in\mathsf{L}_{\mathsf{Kh}}$.

$\triangleleft$

This correspondence, showing that every $\mathrm{LTS}$ has a point-wise
equivalent model in $\bm{\mathrm{M}_{\mathrm{NU}}}$ and vice-versa, gives us a
direct completeness result.

######  Theorem 5.

The axiom system $\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$ (Table 1) is sound
and strongly complete for $\mathsf{L}_{\mathsf{Kh}}$ w.r.t. the class
$\bm{\mathrm{M}_{\mathrm{NU}}}$.

######  Proof..

For soundness, we look at both blocks in Table 1. For the first, Theorem 4
shows that those axioms and rules are sound for all $\mathrm{LTS}^{U}$, and
thus in particular sound for those in the class
$\bm{\mathrm{M}_{\mathrm{NU}}}$. For the second, Item (1) of Proposition 12
shows that every model in $\bm{\mathrm{M}_{\mathrm{NU}}}$ is point-wise
$\mathsf{L}_{\mathsf{Kh}}$-equivalent to an $\mathrm{LTS}$, thus (Theorem 1)
making sound such axioms.

To prove that $\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$ is strongly complete
over the class $\bm{\mathrm{M}_{\mathrm{NU}}}$, we need to show that, given
$\Gamma\cup\\{\varphi\\}$ a set of formulas in $\mathsf{L}_{\mathsf{Kh}}$,
$\Gamma\models\varphi$ implies $\Gamma\vdash\varphi$. Let $\Gamma$ be a
consistent set of formulas. As in [59, Lemma 1], $\Gamma$ can be extended to
an MCS $\Gamma^{\prime}$, and as a consequence, there exists an LTS
$\mathcal{S}^{\Gamma^{\prime}}$ such that
$\mathcal{S}^{\Gamma^{\prime}},\Gamma^{\prime}\models\Gamma$ (notice that
states in the canonical model are MCS). Then, by Item (2) of Proposition 12,
we can obtain an $\mathrm{LTS}^{U}$
$\mathcal{M}_{\\_}{\mathcal{S}^{\Gamma^{\prime}}}$, such that
$\mathcal{M}_{\\_}{\mathcal{S}^{\Gamma^{\prime}}},\Gamma^{\prime}\models\Gamma$.
Moreover, from Item (2) of Proposition 12 we also know that
$\mathcal{M}_{\\_}{\mathcal{S}^{\Gamma^{\prime}}}$ is in
$\bm{\mathrm{M}_{\mathrm{NU}}}$. $\blacksquare$

$\triangleleft$

###  7.2 Active and $\mathrm{SE}$-compositional $\mathrm{LTS}^{U}$s

We presented above a very simple class of models that enables us to establish
a direct relation between both semantics. However, the result is somewhat
trivial: $\mathrm{LTS}^{U}$s generalize $\mathrm{LTS}$s by adding uncertainty
among plans, and the class $\bm{\mathrm{M}_{\mathrm{NU}}}$ contains those
$\mathrm{LTS}^{U}$s in which the agent does not have uncertainty. The rest of
this section will discuss a larger and very general class (with very weak
constraints) for which the same correspondence holds.

Let us start by introducing some preliminary definitions.

######  Definition 7.2.

Let $\mathcal{M}=\langle\mathrm{W},\mathrm{R},\mathrm{S},\mathrm{V}\rangle$ be
an $\mathrm{LTS}^{U}$.

  * •

The _composition_ of $\uppi_{\\_}1,\uppi_{\\_}2\in 2^{{\rm\sf Act}^{*}}$ is
the set of plans $\uppi_{\\_}1\uppi_{\\_}2\in 2^{{\rm\sf Act}^{*}}$ given by

$\uppi_{\\_}1\uppi_{\\_}2:=\\{\sigma_{\\_}1\sigma_{\\_}2\in{\rm\sf
Act}^{*}\mid\sigma_{\\_}1\in\uppi_{\\_}1\text{ and
}\sigma_{\\_}2\in\uppi_{\\_}2\\}.$

  * •

The _$\mathrm{SE}$ -composition_ of $\uppi_{\\_}1,\uppi_{\\_}2\in 2^{{\rm\sf
Act}^{*}}$ _in $\mathcal{M}$_ is the set of plans
$\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2\in 2^{{\rm\sf Act}^{*}}$ given by

$\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2:=\begin{cases*}\uppi_{\\_}1\uppi_{\\_}2&if
$\mathrm{SE}(\uppi_{\\_}1)\neq\varnothing$ and
$\mathrm{R}_{\\_}{\uppi_{\\_}1}(\mathrm{SE}(\uppi_{\\_}1))\subseteq\mathrm{SE}(\uppi_{\\_}2)$\\\
\varnothing&otherwise.\end{cases*}$

$\dashv$

Thus, the $\mathrm{SE}$-composition $\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2$
is the sequential composition of $\uppi_{\\_}1$ and then $\uppi_{\\_}2$ (i.e.,
$\uppi_{\\_}1\uppi_{\\_}2$) when $\uppi_{\\_}1$ is strongly executable
somewhere in the model and $\uppi_{\\_}2$ is strongly executable at all the
states that are reachable via $\uppi_{\\_}1$ from states where $\uppi_{\\_}1$
is strongly executable. Otherwise,
$\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2=\varnothing$. This guarantees that
$\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2$ contains only suitable plans. For
multiple sets of plans $\uppi_{\\_}1,\dots,\uppi_{\\_}k\in\mathrm{S}$, the
$\mathrm{SE}$-composition
$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k$ is the set of
plans $\uppi_{\\_}1\cdots\uppi_{\\_}k$ if and only if
$\mathrm{SE}(\uppi_{\\_}1)\neq\varnothing$ and
$\mathrm{R}_{\\_}{\uppi_{\\_}i}(\mathrm{SE}(\uppi_{\\_}i))\subseteq\mathrm{SE}(\uppi_{\\_}{i+1})$
for all $i=1,\dots,k-1$, and $\varnothing$ otherwise.

The following lemma establishes important properties of the just defined
$\mathrm{SE}$-composition. They will be helpful in the rest of the section.

######  Lemma 2.

Let $\mathcal{M}=\langle\mathrm{W},\mathrm{R},\mathrm{S},\mathrm{V}\rangle$ be
an $\mathrm{LTS}^{U}$ with $\uppi_{\\_}1,\dots,\uppi_{\\_}k\in\mathrm{S}$.
Then,

  1. (1)

$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k\neq\varnothing$
if and only if $\uppi_{\\_}i\mathbin{\bm{;}}\uppi_{\\_}{i+1}\neq\varnothing$
for all $i=1,\dots,k-1$.

  2. (2)

$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k\neq\varnothing$
implies
$\mathrm{SE}(\uppi_{\\_}1)=\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}k)$.

######  Proof..

For the first, consider the left-to-right direction. If
$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k\neq\varnothing$,
then $\mathrm{SE}(\uppi_{\\_}1)\neq\varnothing$. Moreover, for all
$i=1,\dots,k-1$, if $\mathrm{SE}(\uppi_{\\_}i)\neq\varnothing$, then
$\mathrm{SE}(\uppi_{\\_}{i+1})\neq\varnothing$ (because
$\mathrm{R}_{\\_}{\uppi_{\\_}i}(\mathrm{SE}(\uppi_{\\_}i))\subseteq\mathrm{SE}(\uppi_{\\_}{i+1})$).
Therefore, $\mathrm{SE}(\uppi_{\\_}i)\neq\varnothing$ for all $i=1,\dots,k-1$.
Using Definition 7.2, for all $i=1,\dots,k-1$ we have
$\uppi_{\\_}i\mathbin{\bm{;}}\uppi_{\\_}{i+1}\neq\varnothing$. The other
direction is direct.

For the second, suppose
$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k\neq\varnothing$.
For $\bm{(\subseteq)}$, proceed by contradiction: assume there is
$w\in\mathrm{SE}(\uppi_{\\_}1)$ with
$w\not\in\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k)$.
From the latter, $w\not\in\mathrm{SE}(\sigma)$ for some
$\sigma=\sigma_{\\_}1\dots\sigma_{\\_}k\in\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k$.
Thus, there are $d<k$ and $w=v_{\\_}1,\dots,v_{\\_}{d+1}=v$ such that
$v_{\\_}{i+1}\in\mathrm{R}_{\\_}{\sigma_{\\_}i}(v_{\\_}i)$ and
$v\not\in\mathrm{SE}(\sigma_{\\_}{d+1})$. By hypothesis,
$v_{\\_}1=w\in\mathrm{SE}(\uppi_{\\_}1)$ and for all $i=1,\dots,d$, if
$v_{\\_}i\in\mathrm{SE}(\uppi_{\\_}i)$, then we have
$v_{\\_}{i+1}\in\mathrm{SE}(\uppi_{\\_}{i+1})$ (since
$v_{\\_}{i+1}\in\mathrm{R}_{\\_}{\uppi_{\\_}i}(v_{\\_}i)$ and
$\mathrm{R}_{\\_}{\uppi_{\\_}i}(\mathrm{SE}(\uppi_{\\_}i))\subseteq\mathrm{SE}(\uppi_{\\_}{i+1})$).
Hence, $v_{\\_}{d+1}=v\in\mathrm{SE}(\uppi_{\\_}{d+1})$ and therefore
$v\in\mathrm{SE}(\sigma_{\\_}{d+1})$, a contradiction. Thus,
$w\in\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}k)$,
and therefore
$\mathrm{SE}(\uppi_{\\_}1)\subseteq\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}k)$.
The direction $\bm{(\supseteq)}$ is rather immediate. $\blacksquare$

$\triangleleft$

Now, here are the crucial properties we will require of $\mathrm{LTS}^{U}$, to
establish the intended correspondence with $\mathrm{LTS}$s.

######  Definition 7.3.

We say that an $\mathrm{LTS}^{U}$
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\mathrm{S},\mathrm{V}\rangle$ is:

  * •

_active_ if and only if there exists $\uppi\in\mathrm{S}$ such that
$\mathrm{SE}(\uppi)=\mathrm{W}$ and, for all $u,v\in\mathrm{W}$,
$v\in\mathrm{R}_{\\_}{\uppi}(u)$ implies
$\mathcal{M},u\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v$.

  * •

_$\mathrm{SE}$ -compositional_ if and only if for all
$\uppi_{\\_}1,\uppi_{\\_}2\in\mathrm{S}$ with
$\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2\neq\varnothing$ there exists
$\uppi\in\mathrm{S}$ such that:

    1. (1)

$\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2}\subseteq\mathrm{R}_{\\_}{\uppi}$,

    2. (2)

$\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2)\subseteq\mathrm{SE}(\uppi)$,
and

    3. (3)

for all $(w,v)\in\mathrm{R}_{\\_}\uppi$ there exists
$(w^{\prime},v^{\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\uppi_{\\_}2}$
such that
$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},w^{\prime}$
and
$\mathcal{M},v\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime}$.

We define the class
$\bm{\mathrm{M}_{\mathrm{AC}}}:=\\{\mathcal{M}\mid\mathcal{M}\mbox{ is active
and $\mathrm{SE}$-compositional}\\}$. $\dashv$

While activeness ensures that there is a set of plans doing what the empty
plan $\epsilon$ does in an $\mathrm{LTS}$, $\mathrm{SE}$-compositionality
ensures that $\mathrm{S}$ is closed under a suitable notion of composition of
sets of plans. The use of bisimilarity gives us a slightly more general class
of models.

The next lemma establishes that the requirements for
$\mathrm{SE}$-compositionality generalize to an arbitrary number of sets of
plans.

######  Lemma 3.

Let $\mathcal{M}=\langle\mathrm{W},\mathrm{R},\mathrm{S},\mathrm{V}\rangle$ be
an $\mathrm{SE}$-compositional $\mathrm{LTS}^{U}$, and take
$\uppi_{\\_}1,\dots,\uppi_{\\_}k\in\mathrm{S}$ (with $k\geq 2$) such that
$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k\neq\varnothing$.
Then, there is $\uppi\in\mathrm{S}$ such that:

  1. (1)

$\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}k}\subseteq\mathrm{R}_{\\_}{\uppi}$,

  2. (2)

$\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}k)\subseteq\mathrm{SE}(\uppi)$,
and

  3. (3)

for all $(w,v)\in\mathrm{R}_{\\_}\uppi$, there exists
$(w^{\prime},v^{\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}k}$
such that
$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},w^{\prime}$
and
$\mathcal{M},v\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime}$.

######  Proof..

We prove the existence of $\uppi$ by induction on $k\geq 2$; then we will show
that this witness does the work. The base case $k=2$ follows from the
definition, so take sets of plans in $\mathrm{S}$ such that
$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k\mathbin{\bm{;}}\uppi_{\\_}{k+1}\neq\varnothing$.
By Lemma 2,
$\uppi_{\\_}2\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k\mathbin{\bm{;}}\uppi_{\\_}{k+1}\neq\varnothing$
and thus, by inductive hypothesis, there is a $\uppi^{\prime}\in\mathrm{S}$
such that  (1)
$\mathrm{R}_{\\_}{\uppi_{\\_}2\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1}}\subseteq\mathrm{R}_{\\_}{\uppi^{\prime}}$,
(2)
$\mathrm{SE}(\uppi_{\\_}2\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1})\subseteq\mathrm{SE}(\uppi^{\prime})$,
and  (3) for all $(w,v)\in\mathrm{R}_{\\_}{\uppi^{\prime}}$ there exists
$(w^{\prime},v^{\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}2\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1}}$
such that
$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},w^{\prime}$
and
$\mathcal{M},v\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime}$.
Note also how $\mathrm{SE}(\uppi_{\\_}1)\neq\varnothing$ and
$\mathrm{R}_{\\_}{\uppi_{\\_}1}(\mathrm{SE}(\uppi_{\\_}1))\subseteq\mathrm{SE}(\uppi_{\\_}2)=\mathrm{SE}(\uppi_{\\_}2\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1})\subseteq\mathrm{SE}(\uppi^{\prime})$
(by definition of $\mathrm{SE}$-composition, Lemma 2 and the second property
of $\uppi^{\prime}$). Thus,
$\uppi_{\\_}1\mathbin{\bm{;}}\uppi^{\prime}\neq\varnothing$ and hence there is
a $\uppi\in\mathrm{S}$ such that  (1)
$\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\uppi^{\prime}}\subseteq\mathrm{R}_{\\_}{\uppi}$,
(2)
$\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\uppi^{\prime})\subseteq\mathrm{SE}(\uppi)$,
and  (3) for all $(w,v)\in\mathrm{R}_{\\_}{\uppi}$ there exists
$(w^{\prime},v^{\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\uppi^{\prime}}$
such that
$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},w^{\prime}$
and
$\mathcal{M},v\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime}$.
We will prove that $\uppi$ is the witness we are looking for.

For Item (1), take
$(w,v)\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1}}$.
Then, there exists $u\in\mathrm{W}$ such that
$(w,u)\in\mathrm{R}_{\\_}{\uppi_{\\_}1}$ and
$(u,v)\in\mathrm{R}_{\\_}{\uppi_{\\_}2\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1}}$.
Hence, we have $(w,u)\in\mathrm{R}_{\\_}{\uppi_{\\_}1}$ and
$(u,v)\in\mathrm{R}_{\\_}{\uppi^{\prime}}$, so
$(w,v)\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\uppi^{\prime}}$ and
therefore $(w,v)\in\mathrm{R}_{\\_}{\uppi}$.

For Item (2), take
$w\in\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1})$.
By Lemma 2, $w\in\mathrm{SE}(\uppi_{\\_}1)$ and, by the same lemma,
$w\in\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\uppi^{\prime})$. Hence,
$w\in\mathrm{SE}(\uppi)$.

For Item (3), take $(w,v)\in\mathrm{R}_{\\_}{\uppi}$. Then, there exists
$(w^{\prime},v^{\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\uppi^{\prime}}$
such that
$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},w^{\prime}$
and
$\mathcal{M},v\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime}$.
Thus, $(w^{\prime},u^{\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}1}$ and
$(u^{\prime},v^{\prime})\in\mathrm{R}_{\\_}{\uppi^{\prime}}$ for some
$u^{\prime}\in\mathrm{W}$. Again, since
$(u^{\prime},v^{\prime})\in\mathrm{R}_{\\_}{\uppi^{\prime}}$, there exists
$(u^{\prime\prime},v^{\prime\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}2\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1}}$
such that
$\mathcal{M},u^{\prime}\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},u^{\prime\prime}$
and
$\mathcal{M},v^{\prime}\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime\prime}$.
Using that
$\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}$
is transitive, there exists
$(w^{\prime},v^{\prime\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\dots\mathbin{\bm{;}}\uppi_{\\_}{k+1}}$
such that
$\mathcal{M},w\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},w^{\prime}$
and
$\mathcal{M},v\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime\prime}$.
$\blacksquare$

$\triangleleft$

With these tools at hand, we will show that for every $\mathrm{LTS}$ there is
an $\mathsf{L}_{\mathsf{Kh}}$-equivalent $\mathrm{LTS}^{U}$ in
$\bm{\mathrm{M}_{\mathrm{AC}}}$, and vice-versa. First, we present the mapping
from $\mathrm{LTS}^{U}$s to $\mathrm{LTS}$s.

######  Proposition 13.

Let $\mathcal{M}=\langle\mathrm{W},\mathrm{R},\mathrm{S},\mathrm{V}\rangle$ be
an $\mathrm{LTS}^{U}$ in $\bm{\mathrm{M}_{\mathrm{AC}}}$, over ${\rm\sf Act}$.
Take ${\rm\sf Act}^{\prime}:=\\{a_{\\_}{\uppi}\mid\uppi\in\mathrm{S}\\}$, and
then define the $\mathrm{LTS}$
$\mathcal{S}_{\\_}{\mathcal{M}}=\langle\mathrm{W},\mathrm{R}^{\prime},\mathrm{V}\rangle$
over ${\rm\sf Act}^{\prime}$ by taking
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi}}:=\\{(w,v)\in\mathrm{R}_{\\_}{\uppi}\mid
w\in\mathrm{SE}(\uppi)\\}$ (so basic actions in $\mathcal{S}_{\\_}\mathcal{M}$
correspond to sets of SE plans in $\mathcal{M}$). Then,
$\llbracket\varphi\rrbracket^{\mathcal{M}}=\llbracket\varphi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$
for every $\varphi\in\mathsf{L}_{\mathsf{Kh}}$.

######  Proof..

It is clear that $\mathcal{S}_{\\_}\mathcal{M}$ is an $\mathrm{LTS}$. To
obtain a proper signature, we can extend ${\rm\sf Act}^{\prime}$ (in case it
is finite) into an arbitrary ${\rm\sf Act}$.

The rest of the proof of is by structural induction on the formulas in
$\mathsf{L}_{\mathsf{Kh}}$. The cases for the Boolean fragment are
straightforward. We will discuss the case for formulas of the shape
$\mathsf{Kh}(\psi,\varphi)$. In doing so, the following property will be
useful: for every $\uppi\in S$, we have
$\mathrm{SE}(\uppi)=\mathrm{SE}(a_{\\_}{\uppi})$. Indeed, $\bm{(\subseteq)}$
if $u\in\mathrm{SE}(\uppi)$ then there is $v\in\mathrm{W}$ such that
$(u,v)\in\mathrm{R}_{\\_}\uppi$, so
$(u,v)\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}\uppi}$ and therefore, being
$a_{\\_}\uppi$ a basic action, $u\in\mathrm{SE}(a_{\\_}\uppi)$. Moreover,
$\bm{(\supseteq)}$, if $u\in\mathrm{SE}(a_{\\_}\uppi)$ then there is
$v\in\mathrm{W}$ such that $(u,v)\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}\uppi}$,
so $u\in\mathrm{SE}(\uppi)$.

$\bm{(\subseteq)}$ Suppose
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{M}}$; then there
is $\uppi\in\mathrm{S}$ satisfying both

  1. ($\bm{\mathsf{Kh}}$-1)

$\llbracket\psi\rrbracket^{\mathcal{M}}\subseteq\mathrm{SE}(\uppi)$ and

  2. ($\bm{\mathsf{Kh}}$-2)

$\mathrm{R}_{\\_}\uppi(\llbracket\psi\rrbracket^{\mathcal{M}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}}$.

We will prove
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$
using $a_{\\_}\uppi\in{\rm\sf Act}^{\prime}$ as our witness. First, for
showing that $a_{\\_}\uppi$ has the right properties, suppose
$v\in\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$. Then
$v\in\llbracket\psi\rrbracket^{\mathcal{M}}$ (by IH), so
$v\in\mathrm{SE}(\uppi)$ (by ($\bm{\mathsf{Kh}}$-1)) and hence
$v\in\mathrm{SE}(a_{\\_}{\uppi})$ (property discussed above). Therefore,
$\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}\subseteq\mathrm{SE}(a_{\\_}\uppi)$.
Second, for showing that $a_{\\_}{\uppi}$ does the required work, suppose
$u\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi}}(\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}})$.
Then,
$u\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi}}(\llbracket\psi\rrbracket^{\mathcal{M}})$
(by IH), hence
$u\in\mathrm{R}_{\\_}{\uppi}(\llbracket\psi\rrbracket^{\mathcal{M}})$ (by
definition of $\mathrm{R}^{\prime}$) so
$u\in\llbracket\varphi\rrbracket^{\mathcal{M}}$ (by ($\bm{\mathsf{Kh}}$-2)),
and then $u\in\llbracket\varphi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$ (by
IH). Thus,
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi}}(\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$.
From the two pieces, it follows that
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$.

$\bm{(\supseteq)}$ Suppose
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$;
then there is $\sigma\in({\rm\sf Act}^{\prime})^{*}$ satisfying both

  1. ($\bm{\mathsf{Kh}}$-1)

$\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}\subseteq\mathrm{SE}(\sigma)$
and

  2. ($\bm{\mathsf{Kh}}$-2)

$\mathrm{R}^{\prime}_{\\_}\sigma(\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$.

There are two main cases. First, assume $\sigma=\epsilon$. Since $\mathcal{M}$
is active, there is $\uppi\in\mathrm{S}$ s.t. $\mathrm{SE}(\uppi)=\mathrm{W}$
and for all $u,v\in\mathrm{W}$, $v\in\mathrm{R}_{\\_}{\uppi}(u)$ implies
$\mathcal{M},u\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v$.
It is not hard to show that this is the witness we need.

Second, assume $\sigma\neq\epsilon$, i.e.,
$\sigma=a_{\\_}{\uppi_{\\_}1}{\cdots}a_{\\_}{\uppi_{\\_}k}$ with
$a_{\\_}{\uppi_{\\_}i}\in{\rm\sf Act}^{\prime}$ (so
$\uppi_{\\_}i\in\mathrm{S}$). Then, there are two possibilities.

  * •

If
$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k=\varnothing$,
by Lemma 2 there is $i\in\\{1,\ldots,k-1\\}$ s.t.
$\uppi_{\\_}i\mathbin{\bm{;}}\uppi_{\\_}{i+1}=\varnothing$. Then (by
Definition 7.2), either $\mathrm{SE}(\uppi_{\\_}i)=\varnothing$ (hence
$\mathrm{SE}(a_{\\_}{\uppi_{\\_}i})=\varnothing$) or
$\mathrm{R}_{\\_}{\uppi_{\\_}i}(\mathrm{SE}(\uppi_{\\_}i))\not\subseteq\mathrm{SE}(\uppi_{\\_}{i+1})$
(so there is $v\in\mathrm{R}_{\\_}{\uppi_{\\_}i}(\mathrm{SE}(\uppi_{\\_}i))$
with $v\notin\mathrm{SE}(\uppi_{\\_}{i+1})$, i.e., there are $u,v\in W$ such
that $u\in\mathrm{SE}(\uppi_{\\_}i)$, $(u,v)\in\mathrm{R}_{\\_}{\uppi_{\\_}i}$
and $v\notin\mathrm{SE}(\uppi_{\\_}{i+1})$, and hence
$u\in\mathrm{SE}(a_{\\_}{\uppi_{\\_}i})$ [from the first],
$(u,v)\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi_{\\_}i}}$ [from the first and
the second] and $v\notin\mathrm{SE}(a_{\\_}{\uppi_{\\_}{i+1}})$ [from the
third]; thus,
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi_{\\_}i}}(\mathrm{SE}(a_{\\_}{\uppi_{\\_}i}))\not\subseteq\mathrm{SE}(a_{\\_}{\uppi_{\\_}{i+1}})$).
In both cases we get
$\mathrm{SE}(\sigma)=\mathrm{SE}(a_{\\_}{\uppi_{\\_}1}{\cdots}a_{\\_}{\uppi_{\\_}k})=\varnothing$,
and hence
$\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}=\varnothing$ (by
($\bm{\mathsf{Kh}}$-1)). By IH, this implies
$\llbracket\psi\rrbracket^{\mathcal{M}}=\varnothing$, so to get
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{M}}$ we only need
$\mathrm{S}\neq\varnothing$, which we have as $\mathcal{M}$ is an
$\mathrm{LTS}^{U}$.

  * •

If
$\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k\neq\varnothing$,
we contemplate two scenarios. If
$\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}=\varnothing$ then, by
IH, $\llbracket\psi\rrbracket^{\mathcal{M}}=\varnothing$; thus, as before, any
$\uppi\in\mathrm{S}$ works as a witness. Otherwise,
$\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}\neq\varnothing$ and
then, since $\mathcal{M}$ is $\mathrm{SE}$-compositional, by Lemma 3 there
exists $\uppi\in\mathrm{S}$ such that
$\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k}\subseteq\mathrm{R}_{\\_}\uppi$,
$\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k)\subseteq\mathrm{SE}(\uppi)$,
and for all $(v,u)\in\mathrm{R}_{\\_}{\uppi}$, we have
$(v^{\prime},u^{\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k}$
for some $v^{\prime},u^{\prime}\in\mathrm{W}$ satisfying
$\mathcal{M},v\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime}$
and
$\mathcal{M},u\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},u^{\prime}$.
Let’s show that this $\uppi$ does the work.

For the first $\mathsf{Kh}$-clause, take
$w\in\llbracket\psi\rrbracket^{\mathcal{M}}$. Then, by IH,
$w\in\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$, and by
($\bm{\mathsf{Kh}}$-1),
$w\in\mathrm{SE}(a_{\\_}{\uppi_{\\_}1}{\cdots}a_{\\_}{\uppi_{\\_}k})$. For a
contradiction, suppose
$w\not\in\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k)$;
then $w\not\in\mathrm{SE}(\uppi_{\\_}1)$ (by Lemma 2), so
$w\not\in\mathrm{SE}(a_{\\_}{\uppi_{\\_}1})$ and hence
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi_{\\_}1}}(w)=\varnothing$. Hence,
$w\not\in\mathrm{SE}(a_{\\_}{\uppi_{\\_}1}{\cdots}a_{\\_}{\uppi_{\\_}k})$,
which is a contradiction. Therefore,
$w\in\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k)$,
so $w\in\mathrm{SE}(\uppi)$ (since $\mathcal{M}$ is
$\mathrm{SE}$-compositional). Thus,
$\llbracket\psi\rrbracket^{\mathcal{M}}\subseteq\mathrm{SE}(\uppi)$.

For the second $\mathsf{Kh}$-clause, take $u,v\in\mathrm{W}$ such that
$v\in\llbracket\psi\rrbracket^{\mathcal{M}}$ and
$(v,u)\in\mathrm{R}_{\\_}{\uppi}$. By Definition 7.3, there are
$(v^{\prime},u^{\prime})\in\mathrm{R}_{\\_}{\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k}$
such that
$\mathcal{M},v\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},v^{\prime}$
and
$\mathcal{M},u\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},u^{\prime}$.
By Theorem 2, $v^{\prime}\in\llbracket\psi\rrbracket^{\mathcal{M}}$ so, by
inductive hypothesis,
$v^{\prime}\in\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$. By
Definition 7.2,
$u^{\prime}\in(\mathrm{R}_{\\_}{\uppi_{\\_}1}\circ\cdots\circ\mathrm{R}_{\\_}{\uppi_{\\_}k})(v^{\prime})$.
Now, let $v^{\prime}=w_{\\_}1,\dots,w_{\\_}{k+1}=u^{\prime}$ be such that
$w_{\\_}{i+1}\in\mathrm{R}_{\\_}{\uppi_{\\_}i}(w_{\\_}i)$ for all
$i=1,\dots,k$. Since $w_{\\_}1\in\llbracket\psi\rrbracket^{\mathcal{M}}$, from
$\llbracket\psi\rrbracket^{\mathcal{M}}\subseteq\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k)$
(proved in the paragraph above) and Lemma 2, we have
$w_{\\_}1\in\mathrm{SE}(\uppi_{\\_}1\mathbin{\bm{;}}\cdots\mathbin{\bm{;}}\uppi_{\\_}k)=\mathrm{SE}(\uppi_{\\_}1)$.
Moreover, for all $i=1,\dots,k-1$, if $w_{\\_}i\in\mathrm{SE}(\uppi_{\\_}i)$,
since
$\mathrm{R}_{\\_}{\uppi_{\\_}i}(\mathrm{SE}(\uppi_{\\_}i))\subseteq\mathrm{SE}(\uppi_{\\_}{i+1})$
and $w_{\\_}{i+1}\in\mathrm{R}_{\\_}{\uppi_{\\_}i}(w_{\\_}i)$, then
$w_{\\_}{i+1}\in\mathrm{SE}(\uppi_{\\_}{i+1})$. Therefore,
$w_{\\_}i\in\mathrm{SE}(\uppi_{\\_}i)$ for all $i=1,\dots,k$. Since we assume
$(w_{\\_}i,w_{\\_}{i+1})\in\mathrm{R}_{\\_}{\uppi_{\\_}i}$ for all
$i=1,\dots,k$, we have that
$(w_{\\_}i,w_{\\_}{i+1})\in\mathrm{R}_{\\_}{a_{\\_}{\uppi_{\\_}i}}$. Hence,
$u^{\prime}\in(\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi_{\\_}1}}\circ\cdots\circ\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi_{\\_}k}})(v^{\prime})$.
In other words, since
$v^{\prime}\in\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$,
$u^{\prime}\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\uppi_{\\_}1}{\cdots}a_{\\_}{\uppi_{\\_}k}}(\llbracket\psi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}})$.
Thus, by ($\bm{\mathsf{Kh}}$-2) we get
$u^{\prime}\in\llbracket\varphi\rrbracket^{\mathcal{S}_{\\_}\mathcal{M}}$. By
IH, $u^{\prime}\in\llbracket\varphi\rrbracket^{\mathcal{M}}$, which implies
that $u\in\llbracket\varphi\rrbracket^{\mathcal{M}}$ (by
$\mathcal{M},u\mathrel{\,\raisebox{2.15277pt}{\small$\underline{\\!\leftrightarrow\\!}$}\,}\mathcal{M},u^{\prime}$,
and Theorem 2). Therefore
$\mathrm{R}_{\\_}{\uppi}(\llbracket\psi\rrbracket^{\mathcal{M}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}}$.
From the two pieces,
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{M}}$.

This finishes the proof. $\blacksquare$

$\triangleleft$

Now we will prove the other direction. From an $\mathrm{LTS}$ we can obtain an
active, $\mathrm{SE}$-compositional and point-wise equivalent
$\mathrm{LTS}^{U}$.

######  Proposition 14.

Let $\mathcal{S}=\langle\mathrm{W},\mathrm{R},\mathrm{V}\rangle$ be an
$\mathrm{LTS}$ over ${\rm\sf Act}$. Take ${\rm\sf
Act}^{\prime}:=\\{a_{\\_}{\sigma}\mid\sigma\in{\rm\sf
Act}^{*}\;\text{and}\;\mathrm{SE}(\sigma)\neq\varnothing\\}$, and then define
the $\mathrm{LTS}^{U}$
$\mathcal{M}_{\\_}{\mathcal{S}}=\langle\mathrm{W},\mathrm{R}^{\prime},\mathrm{S}^{\prime},\mathrm{V}\rangle$
over ${\rm\sf Act}^{\prime}$ by taking
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma}}:=\\{(w,v)\in\mathrm{R}_{\\_}{\sigma}\mid
w\in\mathrm{SE}(\sigma)\\}$ (so basic actions in
$\mathcal{M}_{\\_}{\mathcal{S}}$ are strongly executable plans in
$\mathcal{S}$) and $\mathrm{S}^{\prime}:=\\{\\{a_{\\_}\sigma\\}\mid
a_{\\_}\sigma\in{\rm\sf Act}^{\prime}\\}$. Then,

  1. (1)

$\mathcal{M}_{\\_}{\mathcal{S}}$ is an active and $\mathrm{SE}$-compositional