2.1 The language ${\mathcal {L}_{\mathsf {Kh}}}$ and its semantics

This subsection introduces the most basic knowing how setting, presented in [Reference Wang59, Reference Wang62]. Through the text, let $\Pi $ be a countable nonempty set of propositional symbols.

Definition 2.1 (Language ${\mathcal {L}_{\mathsf {Kh}}}$ )

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

$$ \begin{align*} \varphi ::= p \mid \neg \varphi \mid \varphi \wedge \varphi \mid \mathsf{Kh}(\varphi,\varphi), \end{align*} $$

with $p \in \Pi $ . The language $ {\mathcal {L}_{P}}$ denotes the propositional fragment of ${\mathcal {L}_{\mathsf {Kh}}}$ .

The formula $\mathsf {Kh}(\psi ,\varphi )$ expresses that the agent knows how to achieve $\varphi $ when $\psi $ is the case. Other Boolean constants and connectives ( $\top $ , $\bot $ , $\vee $ , $\rightarrow $ , $\leftrightarrow $ ) are defined as usual. Additionally, define $\mathsf {A}\varphi := \mathsf {Kh}(\neg \varphi ,\bot )$ and $\mathsf {E}\varphi := \neg \mathsf {A}\neg \varphi $ . As we will see later, $\mathsf {A}$ is a global universal modality, with $\mathsf {A}\varphi $ stating that $\varphi $ holds in all the states.

Following [Reference Wang59], a relational model is also called an ability map. It represents the ability of the agent by indicating not only the actions she can perform at each state, but also the (potentially nondeterministic) outcome of such actions. There can also be terminating states without outgoing relations. Note how the models allow loops, and thus it should not be understood as a temporal model in the traditional sense. Also, since a model describes the agent’s abilities, any learning (and, in general, any action through which the abilities of the agent change) should correspond to an operation that transforms the model, typically by changing the relation for atomic actions (thus allowing the existence of new sequences of actions).

To define the semantics for $\mathsf {Kh}$ , we need a notion of strong executability of a plan (a sequence of actions) in a model, which intuitively means that the plan can always be executed successfully to the end. Before the formal definition of strong executability, we introduce some basic notions.

Definition 2.3. Let $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ be a relational model for $\Pi $ ; let $\sigma \in \Sigma ^*$ be a (possibly empty) finite sequence of actions in $\Sigma $ , with the empty sequence denoted by $\epsilon $ . For $\sigma =\epsilon $ , define $\operatorname {R}_{\epsilon } := \{ (w, w) \mid w \in W \}$ ; for $\sigma = a_1 \ldots a_n$ , define

$$ \begin{align*} \operatorname{R}_{a_1 \ldots a_n} := \operatorname{R}_{a_1}\circ \cdots \circ \operatorname{R}_{a_n} \quad \text{where } \circ \text{ is the composition of relations.} \end{align*} $$

Take a state $w \in W$ . The set $\{ v \in W \mid (w, v) \in \operatorname {R}_{\sigma } \}$ , containing the states $\operatorname {R}_{\sigma }$ -reachable from $w$ , is denoted by $\operatorname {R}_{\sigma }[w]$ .

Note how, if $\sigma =a \in \Sigma $ , then $\operatorname {R}_{\sigma }$ is the relation given by the model, as expected.

Example 2.4. Consider the following relational model.

According to the previous definition, $ \operatorname {R}_{\epsilon }=\{ (w_1,w_1),(w_2,w_2),(w_3,w_3),(w_4,w_4) \}$ . For $\sigma _1= a$ , $\operatorname {R}_{\sigma _1}=\{ (w_1,w_2),(w_1,w_4) \}$ , and for $\sigma _2 = b$ , $\operatorname {R}_{\sigma _2}=\{ (w_2,w_3) \}$ . Finally, $\operatorname {R}_{ab}=\operatorname {R}_{\sigma _1\sigma _2}= \operatorname {R}_{\sigma _1} \circ \operatorname {R}_{\sigma _2}=\{ (w_1,w_3) \}$ .

The notion of strong executability adds one further requirement to Definition 2.5: each time the execution of a strategy starts, it must finish.

Definition 2.6 (Strong Executability)

Let $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ be a relational model for $\Pi $ . Given a nonempty sequence $\sigma = a_1 \ldots a_n \in \Sigma ^*$ and $k \leq |\sigma |$ , denote by $\sigma _k$ the initial segment of $\sigma $ up to $a_k$ (i.e., $\sigma _k := a_1 \ldots a_k$ ). In particular, $\sigma _0 := \epsilon $ (for the empty sequence, $\epsilon _0 := \epsilon $ ).

A sequence $\sigma = a_1 \ldots a_n$ is strongly executable (SE) at $w \in W$ if and only if

$$ \begin{align*} \text{for any } 0 \leq k < n, \quad v \in \operatorname{R}_{\sigma_k}[w] \text{ implies } \operatorname{R}_{a_{k+1}}[v] \neq \varnothing. \end{align*} $$

In other words, $\sigma = a_1 \ldots a_n$ is strongly executable at $w \in W$ if and only if, for any $0 \leq k < n$ , any state $\operatorname {R}_{\sigma _k}$ -reachable from $w$ has at least one $a_{k+1}$ -successor. Note that if $\sigma $ is strongly executable at $w$ , then it is executable at $w$ but the other way around does not hold in general.

With these tools defined, it is possible to provide the semantic interpretation for the language ${\mathcal {L}_{\mathsf {Kh}}}$ .

Definition 2.8 (Semantics)

Let $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ be a relational model, and let $w \in W$ . The satisfaction relation

between the pointed model $\mathcal {M}, w$ and a formula $\varphi $ in ${\mathcal {L}_{\mathsf {Kh}}}$ is inductively defined as follows:

A formula $\varphi $ is satisfiable if and only if there exists a pointed model $\mathcal {M},w$ such that

. As usual, $\varphi $ is valid if and only if

for every pointed model $\mathcal {M},w$ . Additionally, define the set

, typically called the extension of $\varphi $ in $\mathcal {M}$ . The elements of

are also referred to as $\varphi $ -states.

It is worthwhile to notice how, even though the semantic interpretation of $\mathsf {Kh}$ relies on the existence of a sequence $\sigma \in \Sigma ^*$ , such $\sigma $ is not a part of the formula. In fact, no formula in ${\mathcal {L}_{\mathsf {Kh}}}$ refers to actions in $\Sigma $ .

For the semantic interpretation of the knowing how formulas $\mathsf {Kh}(\psi ,\varphi )$ , the definition establishes that, at state $w$ of model $\mathcal {M}$ , the agent knows how to achieve $\varphi $ given $\psi $ , written as , if and only if there is a sequence $\sigma $ that is strongly executable from any $\psi $ -state, and any of such executions leads to a $\varphi $ -state. Note how the evaluation point $w$ does not play any role in the semantic clause, which focuses rather on global model properties. Because of this, a formula of the form $\mathsf {Kh}(\psi ,\varphi )$ is either true in every state (i.e., ) or else false in every state (i.e., ). Thus, this form of knowing how relies not on the actual state of affairs, but rather on ‘global’ abilities, just as knowing how to open a safe given that it is closed does not rely on the current state of the safe.

To give the reader a better grasp of the knowing how formula $\mathsf {Kh}(\psi ,\varphi )$ , it is useful to delve into the semantic interpretation of the abbreviation $\mathsf {A}\varphi := \mathsf {Kh}(\neg \varphi ,\bot )$ . The following proposition states that $\mathsf {A}$ behaves exactly as the global universal modality discussed in [Reference Goranko and Passy25].

Proof. Let $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ be a relational model; given a sequence $\sigma \in \Sigma ^*$ and a state $u \in W$ , use $\mathit {SE}(\sigma ,u)$ as a shortcut for ‘ $\sigma $ is strongly executable at u’. By unfolding the definition of $\mathsf {A}$ , we get that

if and only if

which reduces to

Note that the statement $\mathit {SE}(\sigma , u) \land \forall v \in W \,.\, v \notin \operatorname {R}_{\sigma }[u]$ is contradictory: if $\sigma \in \Sigma ^*$ is SE at u, the set $\operatorname {R}_{\sigma }[u]$ cannot be empty. Then, the statement becomes

Hence, since $\Sigma ^*$ is never empty,

Thus, $\mathsf {A}$ is the global universal modality; as a corollary, $\mathsf {E}\varphi $ is its existential dual.

For a sound and complete axiomatization of validities in ${\mathcal {L}_{\mathsf {Kh}}}$ over the class of relational models, the reader is referred to [Reference Wang59].

In order to finish with the preliminaries, we discuss here two further concepts. First, we introduce the notion of ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalence between pointed models.

Definition 2.10 ( ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalence)

Let $\mathcal {M},w$ and $\mathcal {M}',w'$ be two pointed models. We say $\mathcal {M},w$ and $\mathcal {M}',w'$ are ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalent (notation: $\mathcal {M},w \equiv _{{\mathcal {L}_{\mathsf {Kh}}}} \mathcal {M}',w'$ ) if and only if they satisfy the same ${\mathcal {L}_{\mathsf {Kh}}}$ -formulas, i.e., if and only if, for all $\varphi $ in ${\mathcal {L}_{\mathsf {Kh}}}$ ,

Note that, by Definition 2.8, this is equivalent to checking, for all $\varphi $ in ${\mathcal {L}_{\mathsf {Kh}}}$ , that

For the later discussions, we need a notion of definability of a set of states in a model w.r.t. a given formal language:

Since $\mathsf {Kh}$ formulas are global (either uniformly true or uniformly false throughout the state space), it is a straightforward exercise to show the following proposition.

2.2 Bisimulation for knowing how

This section introduces a notion of bisimulation for the knowing how language ${\mathcal {L}_{\mathsf {Kh}}}$ . We show that this notion is appropriate to prove two classical results: the invariance theorem, and over finite models, a Hennessy-Milner-style theorem. Also, it allows us to compare ${\mathcal {L}_{\mathsf {Kh}}}$ with other approaches of knowing how.

When looking for a notion of bisimulation for a given language, one needs to be careful in formulating the conditions: they should be strong enough to guarantee that the language cannot distinguish bisimilar models, but they should also be weak enough to hold between two models that cannot be distinguished by the language. In other words, a bisimulation should be a notion of structural equivalence matching (in appropriate classes of models) the notion of language indistinguishability. In many cases, the definition will look natural after being provided, but the conditions might not have been obvious at all before.

Let us first review the standard notion of bisimulation for multi-modal logic over models with the same set of actions $\Sigma $ ([Reference Blackburn, de Rijke and Venema12], Section 2.2).

It is clear that the standard bisimulation for the basic multi-modal language is not adequate for our purposes. First of all, the standard bisimulation is only defined between models with the same set of actions $\Sigma $ . However, in our case, the language ${\mathcal {L}_{\mathsf {Kh}}}$ does not explicitly talk about the concrete actions in the models. We will define a variant of bisimulation between models with different $\Sigma $ , which does not match the actions as in the standard bisimulation. As another (obvious) difference, the universal modality is not definable within the basic multi-modal language, but it is definable within ${\mathcal {L}_{\mathsf {Kh}}}$ . Therefore, only matching the connected states is not enough. Still, some of the basic ingredients of the standard bisimulation should appear. From the fact that ${\mathcal {L}_{\mathsf {Kh}}}$ involves atomic propositions and Boolean operators, it is obvious that an appropriate bisimulation relation $Z \subseteq W \times W'$ should only contain pairs of states with matching atomic valuation.

Now, let us discuss the Zig and Zag conditions (also called forth and back). They should match the only modal operator of the language, $\mathsf {Kh}$ . As we are in a modal setting, one might be tempted to require that, if $(w,w')$ is in Z, then these states should have ‘matching’ successors (for an appropriate definition of ‘matching’). However, as it has been emphasized, the actual evaluation point does not play any role in the semantic interpretation of $\mathsf {Kh}$ . In fact, as the universal modality is definable in ${\mathcal {L}_{\mathsf {Kh}}}$ , every state in W should have a ‘matching’ state in $W'$ , and vice-versa, regardless of whether they are accessible from the ‘evaluation point’ $w$ .

But this is clearly not enough: relations between states have not been considered so far, and they are crucial when deciding whether the agent has some strongly executable strategy to achieve a given goal. Further restrictions should be imposed, so the proposed notion of bisimilarity indeed implies ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalence.

When looking for these additional conditions, a crucial observation is that the $\mathsf {Kh}$ operator does not connect a state with another state (as, e.g., the standard $\Diamond $ and $\Box $ modal operators do); it actually connects a set of states (those satisfying the precondition) with another set of states (those that can be reached via the strong execution of some given strategy). Conditions similar to what ${\mathcal {L}_{\mathsf {Kh}}}$ requires can be found in the literature for bisimulations over neighbourhood models (e.g., [Reference Areces and Figueira5, Reference Bakhtiari, van Ditmarsch and Hansen7, Reference Hansen27–Reference Hansen, Kupke and Pacuit29, Reference Pauly51, Reference van Benthem, Bezhanishvili, Enqvist and Yu54]), also related to those for alternating-time temporal logic (e.g., [Reference Ågotnes, Goranko and Jamroga2]) and for conditional modalities (e.g., [Reference Baltag and Ciná9]). For this paper’s definition, the following notions will be useful.

The relation ‘ $\to $ ’ between sets of states captures the essence of the modal operator $\mathsf {Kh}$ : it relates a set $U \subseteq W$ with a set $V \subseteq W$ exactly when there is a sequence in $\Sigma ^*$ that it is strongly executable at every $u \in U$ and whose execution at some $u \in U$ leads to some $v \in V$ . This relation is the crucial notion on the $\mathsf {Kh}$ -Zig and $\mathsf {Kh}$ -Zag clauses (those designed to deal with equivalence for $\mathsf {Kh}$ -formulas) of the ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimulation.

Definition 2.15. Let $\mathcal {M} = \langle W, \Sigma , \operatorname {R}, \operatorname {V} \rangle $ and $\mathcal {M}' = \langle W',\Sigma ', \operatorname {R}', \operatorname {V}' \rangle $ be two relational models; let $Z \subseteq W \times W'$ be a nonempty relation. Define the set of states in $W'$ that are reachable via Z from states in $U \subseteq W$ as

$$ \begin{align*} Z[U] := \{ v' \in W' \mid uZv' \textit{ for } \text{ some } u \in U \}, \end{align*} $$

and the set of states in W that are reachable via the converse of Z from states in $U' \subseteq W'$ as

$$ \begin{align*} Z^{-1}[U'] := \{ v \in W \mid vZu' \textit{ for } \text{ some } u' \in U' \}. \end{align*} $$

The diagram below shows the requirement the $\mathsf {Kh}$ -Zig condition imposes (the dashed lines indicate what the condition demands). Let U be a propositionally definable subset of W; if $U \to V$ (i.e., if $V = \operatorname {R}_{\sigma }[U]$ for some $\sigma \in \Sigma ^*$ strongly executable at all $u \in U$ ), then there should exist a set $V' \subseteq W'$ such that

1. (i) $Z[U] \to V'$ , that is, $V' = \operatorname {R}^{\prime }_{\sigma '}[Z[U]]$ (the set $V'$ contains exactly all those states that are $\sigma '$ -reachable from some state in $Z[U]$ ) for some $\sigma ' \in \Sigma ^{\prime *}$ strongly executable at all $u' \in Z[U]$ and

2. (ii) each state in $V'$ is the Z-image of some state in V.

The $\mathsf {Kh}$ -Zag clause works in the other direction: for every propositionally definable set $U' \subseteq W'$ satisfying $U' \to V'$ there should be a set $V \subseteq W$ such that V satisfies both $\boldsymbol {(i)}$ $Z^{-1}[U'] \to V$ , and $\boldsymbol {(ii)}$ $V \subseteq Z^{-1}[V']$ . The diagram is analogous to the previous one.

Observe how the $\mathsf {Kh}$ -Zig and $\mathsf {Kh}$ -Zag clauses of a ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimulation work globally with arbitrary propositionally definable subsets of the domain. That they act globally over sets of states is natural, given the semantic interpretation of ${\mathcal {L}_{\mathsf {Kh}}}$ ’s only modal operator, $\mathsf {Kh}$ . The requirement of definable sets is also reasonable, as we are only interested in sets of states the language can distinguish. Finally, requiring propositionally definable sets is the same as requiring ${\mathcal {L}_{\mathsf {Kh}}}$ -definable ones (Proposition 2.12). The reason for choosing the former in the formulation is that, in this way, a bisimulation is more ‘structural’, defined only in terms of the model (in particular, in terms of valuations).

Because of their definitions, the clauses guarantee that any ‘ $\to $ ’ transition in one model can be matched by some ‘ $\to $ ’ transition in the other. This is exactly what is needed, as ‘ $U \to V$ ’ is essentially the semantic counterpart of the knowing how modality $\mathsf {Kh}(\psi , \varphi )$ : both require the existence of a strongly executable sequence of actions that, when started at any element of one set (U and , respectively), ends up invariably in some element of the other (V and , respectively).

In the next example we show two bisimilar models, together with the conditions to be checked according to Definition 2.16.

Example 2.17. Let $\mathcal {M} = \langle W, \Sigma , \operatorname {R}, \operatorname {V} \rangle $ and $\mathcal {M}' = \langle W', \Sigma ', \operatorname {R}' ,\operatorname {V}' \rangle $ be the relational models of the diagram below, with nodes specified by both their names and the atoms true at them, and arrows describing the relations $\operatorname {R}_a$ and $\operatorname {R}^{\prime }_a$ . Take the relation $Z \subseteq W \times W'$ to be as depicted by the dotted lines.

Note how Z is a ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimulation between $\mathcal {M}$ and $\mathcal {M}'$ . First, Z clearly satisfies the Atom clause, and also $\mathsf {A}$ -Zig and $\mathsf {A}$ -Zag. Moreover, it satisfies $\mathsf {Kh}$ -Zig too: every ${\mathcal {L}_{P}}$ -definable subset $U \subseteq D(\mathcal {M})$ satisfies the given requirements, as shown in the table below. Therein, we list the sets U, V and $V'$ in the model, and also the corresponding bisimulation images $Z[U]$ and $Z[V]$ . The second column specifies which ${\mathcal {L}_{P}}$ -formula defines the set U, whereas the fourth and the sixth columns enumerate the witness sequences for each relation $U\to V$ and $Z[U]\to V'$ , respectively. Notice that on each row, the set in column $V'$ is included in the set in column $Z[V]$ , as requested for the satisfaction of $\mathsf {Kh}$ -Zig.

An analogous argument shows that Z satisfies $\mathsf {Kh}$ -Zag too.

Observe also the $\mathsf {A}$ -Zig and $\mathsf {A}$ -Zag clauses, which simply state that a bisimulation needs to be total for both models (the global universal modality is definable), and which are required to obtain modal equivalence (the proof of Theorem 2.20 will show this). Note how, although $\mathsf {A}$ is definable in terms of $\mathsf {Kh}$ , the clauses $\mathsf {A}$ -Zig and $\mathsf {A}$ -Zag do not follow from $\mathsf {Kh}$ -Zig and $\mathsf {Kh}$ -Zag, as shown by the following example.

Finally, note how the relation of ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimilarity is indeed an equivalence relation among relational models, a fact that is sometimes used implicitly.

In order to simplify some steps in our proofs below, we introduce the following notation:

(or, equivalently by Definition 2.8,

) if and only if

The statement is equivalent to the semantic clause for $\mathsf {Kh}$ (Definition 2.8):

Both statements are indeed equivalent: from the latter, distribute first the antecedent of the outermost implication, and then the outermost universal quantifier. Using the new notation from Definition 2.14 does the job.

With these tools on the table, it is now time to show that is indeed an appropriate notion of bisimulation for ${\mathcal {L}_{\mathsf {Kh}}}$ . The first result states that ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimilarity implies ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalence.

Theorem 2.20 ( ${\mathcal {L}_{\mathsf {Kh}}}$ Invariance)

Let $\mathcal {M}, w$ and $\mathcal {M}', w'$ be two pointed models, with $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ and $\mathcal {M}'=\langle W',\Sigma ',\operatorname {R}',\operatorname {V}' \rangle $ . Then,

Proof. If , then there is a ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimulation $Z \subseteq W\times W'$ such that $wZw'$ . The proof of ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalence is by structural induction on ${\mathcal {L}_{\mathsf {Kh}}}$ -formulas. The case for atomic propositions follows immediately from the Atom clause, and the cases for the Boolean operators follow from their inductive hypotheses.

The missing piece, the $\mathsf {Kh}(\psi ,\varphi )$ case, uses the auxiliary result .

1. (⊂) Take any state . Then, there is a state such that $vZv'$ . By inductive hypothesis ( $\psi $ is a subformula of $\mathsf {Kh}(\psi ,\varphi )$ ), we have .

2. (⊃) Take any state . By $\mathsf {A}$ -Zag, there is a state $v$ with $vZv'$ ; by inductive hypothesis ( $\psi $ is a subformula of $\mathsf {Kh}(\psi ,\varphi )$ ), . Hence, .

For the actual proof, suppose

. From the semantic interpretation, and using the notation of Definition 2.14, it follows that

The set is clearly ${\mathcal {L}_{\mathsf {Kh}}}$ -definable, and thus ${\mathcal {L}_{P}}$ -definable (Proposition 2.12). Moreover: there is a sequence $\sigma \in \Sigma ^*$ such that , so . Then, from clause $\mathsf {Kh}$ -Zig, there is a set $V' \subseteq W'$ such that $\boldsymbol {(i)}$ (i.e., , given the auxiliary result $(\dagger )$ ) and $\boldsymbol {(ii)}$ $V' \subseteq Z[V]$ .

Now, from and we know that . But the inductive hypothesis states that, for proper subformulas of $\mathsf {Kh}(\psi ,\varphi )$ , ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimilarity implies ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalence; then, from it follows that . This, together with $\boldsymbol {(ii)}$ , yields . Thus, we have both and ; therefore, .

The other direction, from to , follows a symmetric argument, using $\mathsf {A}$ -Zig (for the auxiliary result ) and $\mathsf {Kh}$ -Zag (for the actual proof) instead.

Theorem 2.20 tells us that the semantic condition described by is strong enough to guarantee ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalence. The other direction, showing that is weak enough to hold between any ${\mathcal {L}_{\mathsf {Kh}}}$ -equivalent pointed models, does not hold in general. A typical strategy when dealing with the basic modal language is to focus on a weaker result, showing instead that the desired property holds for image-finite models: those in which each state has, for every $a \in \Sigma $ , only a finite number of a-successors [Reference Blackburn, de Rijke and Venema12, Reference Blackburn and van Benthem13]. Here we will focus rather on models with finite domain; this is because the universal modality is definable in our language, and thus a finite domain is required in order to ensure that each state has only finitely many ‘successors’.

Theorem 2.21. Let $\mathcal {M}, w$ and $\mathcal {M}', w'$ be two pointed finite-domain models, with $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ and $\mathcal {M}'=\langle W',\Sigma ',\operatorname {R}',\operatorname {V}' \rangle $ . Then,

Note that, without the finite domain condition, Theorem 2.21 does not hold. To see this, consider two pointed models $\mathcal {M},w$ and ${\mathcal {M}}',w'$ , both over a set of atoms $\{ p_i \mid i \in \mathbb {N} \}$ . Assume that, in $\mathcal {M}$ , state $w$ has countably infinite a-successors $w_0, w_1, \dots $ , with each atom $p_k$ true at some $w_n$ iff $n \geq k$ ; assume $\mathcal {M}', w'$ is just as $\mathcal {M}, w$ , but with $w'$ having one more successor, $w_{\omega }$ , where all the propositional letters are true. It is not hard to see that $\mathcal {M},w\equiv _{{\mathcal {L}_{\mathsf {Kh}}}}\mathcal {M}',w'$ holds (any [recall: finite] sequence starting at $w'$ can be matched by a sequence starting at $w$ ), but it is not the case that since we can never match $w_{\omega }$ in $\mathcal {M}'$ by $\mathsf {A}$ -Zig. To weaken the finiteness condition, some notion of saturation is needed, but it is out of the scope of the present paper (cf., e.g., [Reference Blackburn, de Rijke and Venema12]).

It is worthwhile to emphasize that a ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimulation works by checking that the discussed models coincide at the abstract level of the ‘ $\to $ ’ transition (Definition 2.14). This emphasizes the imbalance in the framework (rich models described by weak languages), but also suggests that a better balance can be achieved by using a coarser semantic structure where ‘ $\to $ ’ is the primitive notion.

3.1 The language ${\mathcal {L}_{\mathsf {Khm}}}$ and its semantics

Definition 3.22 (Language ${\mathcal {L}_{\mathsf {Khm}}}$ )

Formulas $\varphi $ of the language ${\mathcal {L}_{\mathsf {Khm}}}$ are given by the grammar:

$$ \begin{align*} \varphi ::= p \mid \neg \varphi \mid \varphi \wedge \varphi \mid \mathsf{Khm}(\varphi,\varphi,\varphi), \end{align*} $$

with $p \in \Pi $ . The abbreviation $\mathsf {A}\varphi $ is defined now as $\mathsf {A}\varphi := \mathsf {Khm}(\lnot \varphi , \top , \bot )$ (with $\mathsf {E}\varphi := \neg \mathsf {A}\neg \varphi $ , as before).

In the language ${\mathcal {L}_{\mathsf {Khm}}}$ , the binary knowing how modality $\mathsf {Kh}$ from ${\mathcal {L}_{\mathsf {Kh}}}$ is replaced by a ternary modality $\mathsf {Khm}$ , understood as knowing how while maintaining. A formula $\mathsf {Khm}(\psi ,\chi ,\varphi )$ expresses that, given $\psi $ , the agent knows how to achieve $\varphi $ while maintaining $\chi $ . Formulas of the language are still interpreted in relational models (Definition 2.2). However, their interpretation requires a refinement of the notion of strong executability: now one should take care of what happens at intermediate states.

Definition 3.23. Let $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ be a relational model for $\Pi $ ; let $\chi $ be a formula in ${\mathcal {L}_{\mathsf {Khm}}}$ . A sequence $\sigma = a_1 \ldots a_n \in \Sigma ^*$ is strongly $\chi $ -executable ( $\mathit {SE}{-}\chi $ ) at $w \in W$ if and only if

Note how strong $\chi $ -executability does not require for $\chi $ to hold at either end of the paths; it is enough for it to hold at the intermediate states. With this definition at hand, we are in a position to introduce the language’s semantic interpretation.

Definition 3.24 (Semantics)

Let $\mathcal {M} = \langle W,\Sigma , \operatorname {R},\operatorname {V} \rangle $ be a relational model, and let $w \in W$ . The satisfaction relation

between the pointed model $\mathcal {M}, w$ and atoms, negations and conjunctions is as in Definition 2.8. For $\mathsf {Khm}$ ,

Note how, under this semantic interpretation, the new definition of the modality $\mathsf {A}$ (as, recall, an abbreviation for $\mathsf {Khm}(\lnot \varphi , \top , \bot )$ ) also makes it the global universal modality: the condition that should be maintained, $\top $ , is true at every state.

We use an example from [Reference Wang and Li63] to emphasize the differences between the basic knowing how operator of the previous section and the one with intermediate constraints discussed in this one.

Example 3.25. Consider the following relational model.

Note how, in this model, $\mathsf {Kh}(p, q)$ holds: if the agent is at a p-state, she knows how to reach a situation where q holds. This is because there exists a sequence of actions (namely, $ru$ ) that, when executed at any p-state ( $w_2$ or $w_3$ ), is always completed, and always ending up in a q-state ( $w_7$ and $w_8$ , respectively).

However, $\mathsf {Khm}(p, p, q)$ fails: if the agent is at a p-state, she does not know how to reach a q-state by only passing through p-states. The only strongly executable sequence that ends up in q-states when executed at p-ones, namely $ru$ , has to travel through a $\neg p$ -state ( $w_4$ ) in the case in which the agent starts at $w_3$ .

3.2 Bisimulation for knowing how with intermediate constraints

Clearly, an appropriate notion of bisimulation for the language ${\mathcal {L}_{\mathsf {Khm}}}$ should have some similarities with the notion of bisimulation for ${\mathcal {L}_{\mathsf {Kh}}}$ (Definition 2.16). Still, here one should be careful about the states visited by the sequence $\sigma \in \Sigma ^*$ when going from a $\psi $ -state to one satisfying $\varphi $ . The definition below refines the previously used concepts by taking into account these intermediate states.

Analogous to the ‘simpler’ knowing how case, is the crucial notion on the $\mathsf {Khm}$ -Zig and $\mathsf {Khm}$ -Zig clauses of a ${\mathcal {L}_{\mathsf {Khm}}}$ -bisimulation.

Note the difference between clauses $\mathsf {Kh}$ -Zig/Zag and $\mathsf {Khm}$ -Zig/Zag: the latter also require for the ‘travelled states’ to be bisimilar. Note also how the propositional definability requirement is kept since, just as with ${\mathcal {L}_{\mathsf {Kh}}}$ , a set $U \subseteq D(\mathcal {M})$ is ${\mathcal {L}_{\mathsf {Khm}}}$ -definable if and only if it is propositionally definable. On the other hand, we do not need the intermediate condition X to be propositionally definable in the definition (we only need $Z[X]$ to be propositional definable in the proof of Theorem 3.29, which can be proved).

The next theorems establish that is an appropriate notion of bisimulation for ${\mathcal {L}_{\mathsf {Khm}}}$ over relational models. For modal equivalence, the notion of ${\mathcal {L}_{\mathsf {Khm}}}$ -equivalence ( $\equiv _{{\mathcal {L}_{\mathsf {Khm}}}}$ ) is defined as in Definition 2.10, but for formulas in ${\mathcal {L}_{\mathsf {Khm}}}$ .

First: ${\mathcal {L}_{\mathsf {Khm}}}$ -bisimilarity ( ) implies ${\mathcal {L}_{\mathsf {Khm}}}$ -equivalence ( $\equiv _{{\mathcal {L}_{\mathsf {Khm}}}}$ ).

Theorem 3.28 ( ${\mathcal {L}_{\mathsf {Khm}}}$ Invariance)

Let $\mathcal {M}, w$ and $\mathcal {M}', w'$ be two pointed models, with $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ and $\mathcal {M}'=\langle W',\Sigma ',\operatorname {R}',\operatorname {V}' \rangle $ . Then,

Proof. From , there is a ${\mathcal {L}_{\mathsf {Khm}}}$ -bisimulation $Z \subseteq W\times W'$ such that $wZw'$ . The proof of ${\mathcal {L}_{\mathsf {Khm}}}$ -equivalence is by structural induction on ${\mathcal {L}_{\mathsf {Khm}}}$ -formulas, with the case for atomic propositions being immediate from the Atom clause, and the cases for Boolean operators following from the inductive hypotheses.

For formulas of the form $\mathsf {Khm}(\psi ,\chi ,\varphi )$ , suppose

. Then, by semantic interpretation, and using the new notation (Definition 3.26),

The set

is clearly ${\mathcal {L}_{\mathsf {Khm}}}$ -definable, and thus ${\mathcal {L}_{P}}$ -definable (Proposition 2.12). Moreover: there is a sequence $\sigma \in \Sigma ^*$ such that

, so

. Then, from clause $\mathsf {Khm}$ -Zig it follows that there are sets $X', V' \subseteq W'$ such that

, $\boldsymbol {(ii)} \ \ X' \subseteq Z[X]$ , and $\boldsymbol {(iii)} \ \ V' \subseteq Z[V]$ .

The following three points will be used to show that

. First: using

,Footnote ³ $\boldsymbol {(i)}$ yields

. Second: using inductive hypothesis on $\chi $ (for proper subformulas of $\mathsf {Khm}(\psi ,\chi ,\varphi )$ , ${\mathcal {L}_{\mathsf {Khm}}}$ -bisimilarity implies ${\mathcal {L}_{\mathsf {Khm}}}$ -equivalence), the

of before implies

; this, together with $\boldsymbol {(ii)}$ , implies

. Third, from the assumed

and the previous

, the semantic interpretation of $\mathsf {Khm}$ implies that

. By inductive hypothesis on $\varphi $ , this implies

; hence, from $\boldsymbol {(iii)}$ , it follows that

. Thus, summarizing, we have

which together imply the required

.

The other direction, from to , follows from a symmetric argument, using $\mathsf {A}$ -Zig (for the auxiliary result ) and $\mathsf {Khm}$ -Zag (for the actual proof) instead.

Second: ${\mathcal {L}_{\mathsf {Khm}}}$ -equivalence ( $\equiv _{{\mathcal {L}_{\mathsf {Khm}}}}$ ) implies ${\mathcal {L}_{\mathsf {Khm}}}$ -bisimilarity ( ) in finite relational models.

Theorem 3.29. Let $\mathcal {M}, w$ and $\mathcal {M}', w'$ be two pointed finite-domain models, with $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ and $\mathcal {M}'=\langle W',\Sigma ',\operatorname {R}',\operatorname {V}' \rangle $ . Then,

3.3 Relative expressive power of ${\mathcal {L}_{\mathsf {Kh}}}$ and ${\mathcal {L}_{\mathsf {Khm}}}$

Bisimulations are very useful for investigating the expressive power of a logic. In this subsection, we make use of the tools defined in the previous sections to compare the expressive power of ${\mathcal {L}_{\mathsf {Kh}}}$ and ${\mathcal {L}_{\mathsf {Khm}}}$ . Notice that in order to compare the expressive power of two frameworks, they should rely on the same class of models. We use the following standard definitions for comparing the expressive power of two languages.

A typical proof for showing ${\cal L}_1 \leq {\cal L}_2$ consists on providing a translation $\operatorname {tr}:{\cal L}_1 \to {\cal L}_2$ that assigns, to any formula $\varphi $ in ${\cal L}_1$ , a formula $\operatorname {tr}(\varphi )$ in ${\cal L}_2$ such that, in any given semantic structure for the languages, $\varphi $ holds if and only if $\operatorname {tr}(\varphi )$ holds. A typical (simple) proof for showing ${\cal L}_1 \not \leq {\cal L}_2$ consists on providing two semantic structures that satisfy exactly the same formulas in ${\cal L}_2$ , and then provide a formula in ${\cal L}_1$ that holds in one structure but fails in the other. In more complicated cases, you may need to find two classes of models, $\{\mathcal {M}_i\mid i\in \mathbb {N}\}$ and $\{\mathcal {N}_i \mid i\in \mathbb {N}\}$ respectively, such that a formula in ${\cal L}_1$ can distinguish $\mathcal {M}_i$ and $\mathcal {N}_i$ for all $i\in \mathbb {N}$ but any ${\cal L}_2$ -formula cannot distinguish all of them.

4.1 The language ${\mathcal {L}_{\mathsf {Khw}}}$ and its semantics

Definition 4.32 (Language ${\mathcal {L}_{\mathsf {Khw}}}$ )

Formulas $\varphi $ of the language ${\mathcal {L}_{\mathsf {Khw}}}$ are given by the grammar:

$$ \begin{align*} \varphi ::= p \mid \neg \varphi \mid \varphi \wedge \varphi \mid \mathsf{Khw}(\varphi,\varphi), \end{align*} $$

with $p \in \Pi $ .

Formulas of the form $\mathsf {Khw}(\psi ,\varphi )$ express that, given $\psi $ , the agent weakly knows how to achieve $\varphi $ . The abbreviation $\mathsf {A}\varphi $ is defined as $\mathsf {A}\varphi := \mathsf {Khw}(\lnot \varphi , \bot )$ , as it was done within ${\mathcal {L}_{\mathsf {Kh}}}$ (with $\mathsf {E}\varphi := \neg \mathsf {A}\neg \varphi $ , as usual).

For $\mathsf {Khw}$ ’s semantic interpretation, a further definition is required.

Definition 4.33. Let $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ be a relational model; take a sequence $\sigma \in \Sigma ^*$ and a state $w \in W$ . The set $\mathsf {TerSt}(w,\sigma )$ is the set of states at which the execution of $\sigma $ from $w$ terminates. More precisely, $\mathsf {TerSt}(w,\epsilon ) := \{w\}$ and

$$ \begin{align*} \begin{array}{l@{\;}l} \mathsf{TerSt}(w, a_1\ldots a_n) :=\operatorname{R}_{a_1\ldots a_n}[w]\cup\{ v \in W \mid & v \in \operatorname{R}_{a_1\ldots a_i}[w] \text{ and } \\ & \operatorname{R}_{a_{i+1}}[v] = \varnothing, \text{ for some } i<n \}. \end{array} \end{align*} $$

Definition 4.34 (Semantics)

Let $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ be a relational model; take $w \in W$ . The satisfaction relation

between the pointed model $\mathcal {M}, w$ and atoms, negations and conjunctions is as in Definition 2.8. For $\mathsf {Khw}$ ,

Thus, weakly knowing how to achieve a given $\varphi $ corresponds to the sketched notion of weak conformant plan: the agent weakly knows how to achieve $\varphi $ given the condition $\psi $ , written as $\mathsf {Khw}(\psi ,\varphi )$ , if and only if there is a finite sequence of actions $\sigma \in \Sigma ^*$ that, when started on any state satisfying $\psi $ (for all $u \in W$ with ), it always ends on states satisfying $\varphi $ , regardless of whether the sequence was executed at its fullest or not ( $v \in \mathsf {TerSt}(u,\sigma )$ implies ). Once again, the knowing how modality is global, making $\mathsf {A}$ the universal modality.

There are other ways to weaken the executability in the semantics, e.g., [Reference Wang58], where a notion of bisimulation was proposed, inspired by an earlier version of this paper.

4.2 Bisimulation for weakly knowing how

As before, defining a ${\mathcal {L}_{\mathsf {Khw}}}$ -bisimulation requires an extra piece of notation.

Below we introduce the notion of bisimulation for ${\mathcal {L}_{\mathsf {Khw}}}$ .

By reasoning as in the proofs of Theorems 2.20 and 3.28, it can be proved that ${\mathcal {L}_{\mathsf {Khw}}}$ -bisimilarity ( ) implies ${\mathcal {L}_{\mathsf {Khw}}}$ -equivalence ( $\equiv _{{\mathcal {L}_{\mathsf {Khw}}}}$ ), with the latter defined as in Definition 2.10 but for formulas in ${\mathcal {L}_{\mathsf {Khw}}}$ .

Theorem 4.38 ( ${\mathcal {L}_{\mathsf {Khw}}}$ Invariance)

Let $\mathcal {M}, w$ and $\mathcal {M}', w'$ be two pointed models, with $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ and $\mathcal {M}'=\langle W',\Sigma ',\operatorname {R}',\operatorname {V}' \rangle $ . Then,

Then, just as for ${\mathcal {L}_{\mathsf {Kh}}}$ and ${\mathcal {L}_{\mathsf {Khm}}}$ (Theorems 2.21 and 3.29, respectively), in finite-domain relational models, ${\mathcal {L}_{\mathsf {Khw}}}$ -equivalence implies ${\mathcal {L}_{\mathsf {Khw}}}$ -bisimilarity.

Theorem 4.39. Let $\mathcal {M}, w$ and $\mathcal {M}', w'$ be two pointed finite-domain models, with $\mathcal {M} = \langle W,\Sigma ,\operatorname {R},\operatorname {V} \rangle $ and $\mathcal {M}'=\langle W',\Sigma ',\operatorname {R}',\operatorname {V}' \rangle $ . Then,

4.3 Expressive power of ${\mathcal {L}_{\mathsf {Khw}}}$

In this section we compare the expressive power of ${\mathcal {L}_{\mathsf {Khw}}}$ with respect to ${\mathcal {L}_{\mathsf {Kh}}}$ and ${\mathcal {L}_{\mathsf {Khm}}}$ .

Proof. Consider the following models:

Dotted lines define a ${\mathcal {L}_{\mathsf {Khw}}}$ -bisimulation. The table below shows that the models satisfy the requirements for $\mathsf {Khw}$ -Zig from Definition 4.37 ( $\mathsf {Khw}$ -Zag can be similarly checked). Note that we only consider the non-trivial cases.

Since $\mathcal {M},w$ and $\mathcal {M}',w$ are ${\mathcal {L}_{\mathsf {Khw}}}$ -bisimilar, they satisfy the same ${\mathcal {L}_{\mathsf {Khw}}}$ -formulas (Theorem 4.38). However, they can be distinguished by ${\mathcal {L}_{\mathsf {Kh}}}$ , as but .

One might be tempted to think, then, that both ${\mathcal {L}_{\mathsf {Kh}}}$ and ${\mathcal {L}_{\mathsf {Khm}}}$ are strictly more expressive than ${\mathcal {L}_{\mathsf {Khw}}}$ , but actually this is not the case.

Proof. Consider the following models:

Dotted lines define both a ${\mathcal {L}_{\mathsf {Kh}}}$ -bisimulation and a ${\mathcal {L}_{\mathsf {Khm}}}$ -bisimulation (the only potentially meaningful differences between the models, the a-transition from u to z in $\mathcal {M}$ and the a-transition from $u'$ to itself in $\mathcal {M}'$ , can mimic each other). Thus, the models cannot be distinguished by ${\mathcal {L}_{\mathsf {Kh}}}$ , and neither by ${\mathcal {L}_{\mathsf {Khm}}}$ . However, ${\mathcal {L}_{\mathsf {Khw}}}$ can tell them apart, as but .

As a consequence, we get the following result:

5.1 The language ${\mathcal {L}_{\mathsf {Khs}}}$ and its semantics

Definition 5.43 (Language)

The language ${\mathcal {L}_{\mathsf {Khs}}}$ has two modalities, $\mathsf {K}$ for knowing that, and $\mathsf {Khs}$ for knowing how. Formally, formulas $\varphi $ of ${\mathcal {L}_{\mathsf {Khs}}}$ are given by the grammar:

$$ \begin{align*} \varphi:= \bot \mid p\mid \neg\varphi\mid \varphi\wedge\varphi \mid \mathsf{K}\varphi\mid \mathsf{Khs}(\varphi), \end{align*} $$

with $p\in \Pi $ .

Note again how no formula in ${\mathcal {L}_{\mathsf {Khs}}}$ refers to actions in $\Sigma $ . More importantly, ${\mathcal {L}_{\mathsf {Khs}}}$ has two epistemic operators, and each of them needs to be interpreted on a different dimension. For the $\mathsf {Khs}$ modality, the model must have one dimension representing ‘strategies’ (the ability map of before), whereas for $\mathsf {K}$ we need the classical indistinguishability relation used in classical epistemic logic. This produces richer models, defined formally in the following way.

Note how the relations $\sim $ and $\operatorname {R}_{a}$ are independent from each other, thus giving us the most general framework regarding the interaction between the two.

Let us start by defining the transitions between indistinguishable epistemic states.

In the next definition, we make precise the notion of strategy.

A strategy assigns an action not to a state, but rather to a $\sim $ -equivalence class; this we call uniformity. Equally important is the fact that the assigned action symbol should be executable in every state of the $\sim $ -equivalence class; without it, the knowledge-how may be trivialized. Note how the empty function is also a strategy: the empty strategy. We use $\texttt {dom}(\sigma )$ to denote the domain of $\sigma $ (i.e., the set of equivalence classes in $W/{{\hspace{-0.0001pt}}}_{\sim }$ on which $\sigma $ is defined).

Definition 5.49 (Semantics)

Let $\mathcal {M}=\langle W,\Sigma ,\sim ,\operatorname {R}_{},\operatorname {V} \rangle $ be a bi-dimensional relational model; take a state $w\in W$ . The satisfaction relation

between the pointed model $\mathcal {M},w$ and a formula $\varphi $ in ${\mathcal {L}_{\mathsf {Khs}}}$ is inductively defined as before for atoms, negation and conjunction; for the new modalities,

As we already mentioned, with this new logic we are capturing two epistemic properties, unlike the logics presented in previous sections. Notice that although the global universal modality definable in the previous frameworks can be viewed as a restricted form of knowing that operator, it can only express global background knowledge to some extent. Moreover, bi-dimensional models contain both epistemic uncertainty and action transitions; thus, one can talk about changes of knowledge after actions, which is essential to facilitate strategies based on local knowledge, compared to the quite restricted linear plans used by [Reference Wang59, Reference Wang62].

Finally, recall that the global operator $\mathsf {Kh}(\psi , \varphi )$ of Section 2 expresses that the agent knows how to achieve $\varphi $ given the condition $\psi $ . From the perspective of this section’s approach, the condition $\psi $ in the basic knowing how setting defines an initial uncertainty set, and $\mathsf {Kh}(\psi , \varphi )$ can be read rather as ‘the agent knows how to achieve $\varphi $ given that (s)he only knows $\psi $ ’. However, one might consider this a very weak notion of uncertainty. The strategically knowing how of this section deals with this issue by combining local modalities for different kinds of knowledge.

Example 5.50. Consider the bi-dimensional model below [Reference Fervari, Velázquez-Quesada and Wang22], example 1.1) (double dashed lines represent $\sim $ ; reflexive $\sim $ -edges omitted).

The model represents a scenario in which a doctor needs a plan to treat a patient and cure his pain (represented by the propositional symbol p), under the uncertainty about some possible allergy ( $q)$ . On the one hand, if there is no allergy (i.e., q fails) then taking some pills will cure the pain, with a surgery not being an option. On the other hand, in presence of the allergy (i.e., q holds), the pills may cure the pain or have no effect at all, while the surgery can cure the pain for sure. Notice that there is an action to test whether q is the case. The indistinguishability between $w_1$ and $w_2$ represents the initial uncertainty about the allergy. According to the model, in order to cure the pain (reaching $\neg p$ ), it makes sense to take the surgery if the test of whether q is positive, and take the pills otherwise. In this case, the doctor knows how to cure the pain, denoted $\mathsf {Khs}(\neg p)$ , thanks to the aforementioned strategic plan.

5.2 Bisimulation for strategically knowing how

First, we introduce some further notation.

Then, we introduce a notion of bisimulation for ${\mathcal {L}_{\mathsf {Khs}}}$ over bi-dimensional models.

The Zig and Zag conditions are inherited from the standard modal bisimulation [Reference Blackburn, de Rijke and Venema12], Section 2.2). The diagram below describes the way the $\mathsf {Khs}$ -Zig condition works. Gray circles represent the equivalence classes $[w]$ , $[w']$ , $[v']$ and $[u']$ , for the relations $\sim $ and $\sim '$ , respectively. Given $w\leadsto U$ (through the strategy $\sigma $ ), then $w'\leadsto U'$ should be the case (for some $U'$ and through some $\sigma '$ ). Moreover, each state in $U'$ (which, recall, might be the union of different equivalence classes due to the potential nondeterminism of the relations), must be the Z-image of some state in U (so $vZv'$ and $uZu'$ ). Clause $\mathsf {Khs}$ -Zag works analogously.

Notice that an ${\mathcal {L}_{\mathsf {Khs}}}$ -bisimulation takes care of two aspects. On the one hand, ${\mathcal {L}_{\mathsf {Khs}}}$ includes the standard knowing that operator $\mathsf {K}$ , so a ${\mathcal {L}_{\mathsf {Khs}}}$ -bisimulation matches pairs of states when they coincide in the structural information for their respective indistinguishability relations. The usual Zig and Zag conditions take care of this. On the other hand, only states coinciding in their executability should be matched. Unlike the bisimulations introduced before, the strategic reachability condition establishes a constraint not over a set of propositionally definable states, but on the states which are epistemically indistinguishable. This way, we are able to describe the proper interaction between the two kinds of knowledge the language considers.

The next theorem establishes that is an appropriate notion of bisimulation for ${\mathcal {L}_{\mathsf {Khs}}}$ . As usual, the notion of ${\mathcal {L}_{\mathsf {Khs}}}$ -equivalence, $\equiv _{{\mathcal {L}_{\mathsf {Khs}}}}$ , is defined as in Definition 2.10, but for formulas in ${\mathcal {L}_{\mathsf {Khs}}}$ .

Theorem 5.54 ( ${\mathcal {L}_{\mathsf {Khs}}}$ Invariance)

Let $\mathcal {M},w$ and $\mathcal {M}',w'$ be two pointed bi-dimensional models, with $\mathcal {M}=\langle W,\Sigma ,\sim ,\operatorname {R}_{},\operatorname {V} \rangle $ and $\mathcal {M}' = \langle W',\Sigma ',\sim ',\operatorname {R}_{}',\operatorname {V}' \rangle $ . Then,

We consider now the converse of Theorem 5.54; in finite models, ${\mathcal {L}_{\mathsf {Khs}}}$ -equivalence ( $\equiv _{{\mathcal {L}_{\mathsf {Khs}}}}$ ) implies ${\mathcal {L}_{\mathsf {Khs}}}$ -bisimilarity ( ).

Theorem 5.55. Let $\mathcal {M},w$ and $\mathcal {M}',w'$ be two pointed finite-domain bi-dimensional models, with $\mathcal {M}=\langle W,\Sigma ,\sim ,\operatorname {R}_{},\operatorname {V} \rangle $ and $\mathcal {M}' = \langle W',\Sigma ',\sim ',\operatorname {R}_{}',\operatorname {V}' \rangle $ . Then,