# Adding Proof Calculi to Epistemic Logics with Structured Knowledge

Mario Benevides, Alexandre Madeira, Manuel A. Martins

► To cite this version:

Mario Benevides, Alexandre Madeira, Manuel A. Martins. Adding Proof Calculi to Epistemic Logics with Structured Knowledge. 9th International Conference on Fundamentals of Software Engineering (FSEN), May 2021, Virtual, Iran. pp.53-68, 10.1007/978-3-030-89247-0_4. hal-04074528

HAL Id: hal-04074528

https://inria.hal.science/hal-04074528

Submitted on 19 Apr 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# Adding Proof Calculi to Epistemic Logics with Structured Knowledge

Mario Benevides<fnref n="1" />, Alexandre Madeira<fnref n="2" />, and Manuel A. Martins<fnref n="2" />

**Abstract.** Dynamic Epistemic Logic (DEL) is used in the analysis of a wide class of application scenarios involving multi-agents systems with local perceptions of information and knowledge. In its classical form, the knowledge of epistemic states is represented by sets of propositions. However, the complexity of the current systems, requires other richer structures, than sets of propositions, to represent knowledge on their epistemic states. Algebras, graphs or distributions are examples of useful structures for this end. Based on this observation, we introduced a parametric method to build dynamic epistemic logics on-demand, taking as parameter the specific knowledge representation framework (e.g., propositional, equational or even a modal logic) that better fits the problems in hand. In order to use the built logics in practices, tools support is needed. Based on this, we extended our previous method with a parametric construction of complete proof calculi. The complexity of the model checking and satisfiability problems for the achieved logics are provided.

## 1 Introduction

Multi-agent (dynamic) epistemic logics [5, 8, 14] play an important role in a number of applied areas of Computer Science, including the analysis of secure protocols, knowledge acquisition systems, or cooperative multi-agents platforms (see [25]). Dynamic epistemic logic was introduced to represent and reason about agents, or groups of agents, knowledge and beliefs. Models for these logics are Epistemic Kripke Structures - multi-modal Kripke structures, whose states formalize information as set of propositions, and, for each agent, an equivalence relation between edges, relating indistinguishable states from the point of view of each agent.

In order to deal with scenarios that involve information and knowledge better represented using richer structures than simple sets of propositions, we proposed in our previous paper [19] a method to construct more expressive epistemic logics. From this method, called 'epistemisation', we derived a number of epistemic logics able to represent the knowledge of states as the usual structures of computer science, including propositions, graphs or abstract data types. The parameter used in this method, called knowledge representation framework, is defined by a set of formulas, a set of models, and a satisfaction relation. The formulas of the lower level play the role of the (atomic) propositions of the epistemic logic in the upper level; and these structures are used to represent the knowledge in each epistemic state on the models of the achieved logic.

<footnote n="1">¹ Universidade Federal Fulminence, Brazil</footnote>

<footnote n="2">² CIDMA & Dep. Mathematics of Universidade de Aveiro, Portugal</footnote>
The instantiations of the method discussed in the paper [19], some of them recalled below, provide an interesting starting point for their application to real scale case studies. However, as usual, the effective handling of real cases needs some level of tools support. This paper, extends the work presented in [19] in two different directions: firstly, we study the complexity of the model checking and the SAT problems on generic epistemisations; secondly, we introduce a parametric construction of Hilbert style calculus and we establish its completeness and decidability. The structure of knowledge representation, as introduced in the reference [19], was further endowed with an entailment system adequate for the respective satisfaction relation. The parametric principle of the constructions of logic calculus and the respective characterisations are inspired in the approach we followed for parametrised hybrid logics in the reference [22].

There are works that use epistemic models, in which states have a structure (e.g. [1,13]). In the work reported in [1], a multi-agent epistemic logic is introduced in which states are positions in $\mathbb{R}^n$ and the accessibility relations represent the possible states (positions) compatible with the current one. Also in the works reported in [13, 15, 16], (dynamic) epistemic logics based on the notion of visibility or observability of propositional variables are presented, i.e., some propositional variable are observable and others are not. Other works deal with values in an epistemic setting (e.g. [6, 7, 26]). Here, states are equipped with register that can store values (as in the paper [6]) or with constants that can have their values updated (as done in references [7, 26]). In the case of the epistemisation of equational logic it reminds first order modal logic (see [10]), where epistemic states are relational structures.

**Outline.** The remaining of the paper is organized as follows: Section 2 overviews the epistemisation method introduced in [19] and a set of interesting instantiations is recalled. On view of the current paper aims, an enrichment of the notion of knowledge representation framework, the Boolean knowledge framework, was introduced. Then, in Section 3, we introduced a method to endow epistemisations with proof support. The method derive (complete) logical calculus for any epistemisation built on a (complete) calculus for the base knowledge representation framework. The complexity of the model checking and SAT problem for epistemisation is discussed in Section 4. Some final remarks are provided in Section 5.

## 2 Overview on parametric construction of Epistemic Logics with structured states

This section overviews and extends the parametric construction of Epistemic Logics with structured states that we introduced in [19].

### 2.1 The parameter

In order to represent knowledge of structured states, a generic notion of logic is needed. In our previous work [19], we introduced the *knowledge representation framework*. Basically, this framework will be used to express properties about the (local) knowledge in
states (e.g. if with propositions, equations or modal formulas), and to support its structure (if by valuations, algebras or graphs). Now, we enrich this notion with an inference relation satisfying the necessary conditions for the developments of the paper. This (local) inference relation will be used as the base of the (global) built logic.

**Definition 1** ((Boolean) Knowledge Representation Framework). A Knowledge Representation Framework is a tuple

$$ \mathcal{L} = (\mathrm{Fm}_{\mathcal{L}}, \mathrm{Mod}_{\mathcal{L}}, \models_{\mathcal{L}}, \vdash_{\mathcal{L}}) $$

where

- $\mathrm{Fm}_{\mathcal{L}}$ is a countable set of formulas,

- $\mathrm{Mod}_{\mathcal{L}}$ is a set of models for $\mathcal{L}$,

- relation $\models_{\mathcal{L}} \subseteq \mathrm{Mod}_{\mathcal{L}} \times \mathrm{Fm}_{\mathcal{L}}$ is a relation called satisfaction relation of $\mathcal{L}$. We write $\Gamma \models_{\mathcal{L}} \varphi$ whenever for any model $M \in \mathrm{Mod}_{\mathcal{L}}$ such that $M \models_{\mathcal{L}} \gamma$, for all $\gamma \in \Gamma$, it holds that $M \models_{\mathcal{L}} \varphi$;

- $\vdash_{\mathcal{L}} \subseteq \mathcal{P}(\mathrm{Fm}_{\mathcal{L}}) \times \mathrm{Fm}_{\mathcal{L}}$ is a relation called entailment of $\mathcal{L}$.

A knowledge representation framework $\mathcal{L}$ is a Boolean knowledge representation framework, knowledge framework for short, if:

- it has semantic negation i.e. for any formula $\varphi \in \mathrm{Fm}_{\mathcal{L}}$ there is a formula $\neg \varphi \in \mathrm{Fm}_{\mathcal{L}}$ such that, for any model $M \in \mathrm{Mod}_{\mathcal{L}}$:

$$ M \models_{\mathcal{L}} \neg \varphi \text{ iff it is false that } M \models_{\mathcal{L}} \varphi \quad (1) $$

- is has semantic conjunction, i.e. for any finite set of formulas $\Gamma \subseteq \mathrm{Fm}_{\mathcal{L}}$ there is a formula $\bigwedge \Gamma \in \mathrm{Fm}_{\mathcal{L}}$ such that, for any model $M \in \mathrm{Mod}_{\mathcal{L}}$,

$$ \text{for any } \gamma \in \Gamma, M \models \gamma, \text{ iff } M \models \bigwedge \Gamma \quad (2) $$

(if $\Gamma$ has exactly two formulas $\varphi$ and $\varphi'$ we denote $\bigwedge \Gamma$ by $\varphi \wedge \varphi'$).

- is has semantic implication, i.e. for any two formulas $\varphi, \varphi' \in \mathrm{Fm}_{\mathcal{L}}$ there is a formula $\varphi \rightarrow \varphi'$ such that, for any model $M \in \mathrm{Mod}_{\mathcal{L}}$,

$$ M \models \varphi \rightarrow \varphi' \text{ iff } M \models \varphi \text{ implies that } M \models \varphi' \quad (3) $$

We say that a knowledge framework $\mathcal{L}$ is *sound* if for any $\varphi \in \mathrm{Fm}_{\mathcal{L}}$,

$$ \text{if } \Gamma \vdash_{\mathcal{L}} \varphi \text{ then } \Gamma \models_{\mathcal{L}} \varphi \quad (4) $$

and we say that it is *complete* if for any $\varphi \in \mathrm{Fm}_{\mathcal{L}}$,

$$ \text{if } \Gamma \models_{\mathcal{L}} \varphi \text{ then } \Gamma \vdash_{\mathcal{L}} \varphi \quad (5) $$

Now we proved two lemmas that will be used for the proof of the completeness of the logics built from the epistemisation method.
**Lemma 1.** Let $\mathcal{L}$ be a knowledge framework and $\Gamma \subseteq \text{Fm}_\mathcal{L}$ be finite set of formulas. Then, the following properties hold:

1. $\Gamma \models_{\mathcal{L}} \bigwedge \Gamma$

2. $\Gamma \models_{\mathcal{L}} \varphi$ iff $\models_{\mathcal{L}} \bigwedge \Gamma \rightarrow \varphi$

3. $\Gamma \models_{\mathcal{L}} \varphi$ and $\Gamma \subseteq \Delta$, then $\Delta \models_{\mathcal{L}} \varphi$

A set of formulas $\Gamma \subseteq \text{Fm}_\mathcal{L}$ is said $\mathcal{L}$-consistent iff does not exists a formula $\varphi \in \text{Fm}_\mathcal{L}$ such that $\Gamma \vdash_{\mathcal{L}} \varphi$ and $\Gamma \vdash_{\mathcal{L}} \neg \varphi$. Moreover, $\Gamma \subseteq \text{Fm}_\mathcal{L}$ is said $\mathcal{L}$-maximal consistent if it is $\mathcal{L}$-consistent and there is no $\mathcal{L}$-consistent set that properly contains it.

**Lemma 2.** Let $\mathcal{L}$ be a sound and complete knowledge framework. For any finite consistent set of formulas $\Gamma \subseteq \text{Fm}_\mathcal{L}$, there is a model $M_\Gamma \in \text{Mod}_\mathcal{L}$ such that

$$M_\Gamma \models_{\mathcal{L}} \bigwedge \Gamma \qquad (6)$$

*Proof.* By 1. of Lemma 1, we know that $\Gamma \models_{\mathcal{L}} \bigwedge \Gamma$ and by (4) and (5) that by $\Gamma \vdash_{\mathcal{L}} \bigwedge \Gamma$. Since $\Gamma$ is $\mathcal{L}$-consistent, we have also that $\Gamma \vdash_{\mathcal{L}} \neg \Gamma$. By (4) and (5), $\Gamma \not\models_{\mathcal{L}} \neg \Gamma$ and hence, there is a model $M_\Gamma \in \text{Mod}_\mathcal{L}$ such that $M_\Gamma \models_{\mathcal{L}} \bigwedge \Gamma$ and $M_\Gamma \not\models_{\mathcal{L}} \neg \Gamma$. Therefore, $M_\Gamma \models_{\mathcal{L}} \bigwedge \Gamma$.

## 2.2 The method

As examples of Knowledge representation frameworks we can enumerate all the logics with a complete calculus. Classic Propositional, Equational Logic or the Hybrid Logic with Binders [3] can be useful in a number of application scenarios (see [19]).

Then, for a fixed knowledge representation $\mathcal{L}$ we define the epistemisation of $\mathcal{L}$ denoted by $\mathcal{E}(\mathcal{L})$. The set of formulas for the $\mathcal{L}$-epistemic logic for a finite set of agents Ag, in symbols $\text{Fm}_{\mathcal{E}(\mathcal{L})}$, is defined by the following grammar:

$$\varphi ::= \varphi_0 | \neg \varphi | \varphi \wedge \varphi | K_a \varphi | E_G | C_G \varphi$$

where $\varphi_0 \in \text{Fm}_\mathcal{L}$, $a \in \text{Ag}$ and $G \subseteq \text{Ag}$. If $\Gamma$ is a finite set of formulas, the expression $\bigwedge \Gamma$ denote the conjunction of all the formulas in $\Gamma$.

The standard connectives can be presented as abbreviations, namely $\varphi \vee \varphi' \equiv \neg(\neg \varphi \wedge \neg \varphi')$, $\varphi \rightarrow \varphi' \equiv \neg(\varphi \wedge \neg \varphi')$, $B_a \varphi \equiv \neg K_a \varphi$ and $E_G \varphi \equiv \bigwedge_{a \in G} K_a \varphi$. Here we are assuming that the Boolean connectives and the agent modalities symbols do not occur in the formulas $\text{Fm}_\mathcal{L}$. If this is not the case we make the renaming of symbols.

The intuitive meaning of the modal formulas are:

- $\varphi_0$ - is an assertion about the (structured) epistemic states, expressed in the knowledge representation framework $\mathcal{L}$;

- $K_a \varphi$ - agent $a$ knows $\varphi$;

- $E_G \varphi$ - every agent $a \in G$ knows $\varphi$;

- $C_G \varphi$ - it is common knowledge among all members of group $G$ that it is the case that $\varphi$.
An $\mathcal{L}$-epistemic model for a finite set of agents Ag, Ag-model for short, is a tuple
$\mathcal{M} = (W, \sim, M)$ where

- $W$ is a non-empty set of states;

- $\sim$ is an Ag-family of equivalence relations $(\sim_a \subseteq W \times W)_{a \in A_g}$; and

- $M: W \to \mathrm{Mod}_{\mathcal{L}}$ is a function, that assigns the knowledge structure of each state.

We also consider the relations $\sim_G = \bigcup_{a \in G} \sim_a$ and $\sim_G^* = (\sim_G)^*$, where $(\sim_G)^*$ is the reflexive, transitive closure of $\sim_G$. The set of $\mathcal{L}$-epistemic models for a set of agents Ag is denoted by $\mathrm{Mod}_{\mathcal{E}(\mathcal{L})}$.

For any Ag-model $\mathcal{M} = (W, \sim, M)$, for any $w \in W$, and $\varphi \in \mathrm{Fm}_{\mathcal{E}(\mathcal{L})}$, the
satisfaction relation

$$
\models \subseteq \mathrm{Mod}_{\mathcal{E}(\mathcal{L})} \times \mathrm{Fm}_{\mathcal{E}(\mathcal{L})}
$$

is recursively defined as follows:

- $\mathcal{M}, w \models \varphi_0$ iff $\mathcal{M}(w) \models_{\mathcal{L}} \varphi_0$, for any $\varphi_0 \in \mathrm{Fm}_{\mathcal{L}}$

- $\mathcal{M}, w \models \neg \varphi$ iff $\mathcal{M}, w \not\models \varphi$

- $\mathcal{M}, w \models \varphi \wedge \psi$ iff $\mathcal{M}, w \models \varphi$ and $\mathcal{M}, w \models \psi$

- $\mathcal{M}, w \models K_a \varphi$ iff for all $w' \in W : w \sim_a w' \Rightarrow \mathcal{M}, w' \models \varphi$

- $\mathcal{M}, w \models E_G \varphi$ iff for all $w' \in W$ we have $w \sim_G w' \Rightarrow \mathcal{M}, w' \models \varphi$

- $\mathcal{M}, w \models C_G \varphi$ iff for all $w' \in W : w \sim_G^* w' \Rightarrow \mathcal{M}, w' \models \varphi$

We write $\mathcal{M} \models \varphi$ whenever, for any $w \in W$, $\mathcal{M}, w \models \varphi$.

It is easy to see that

- $\mathcal{M}, w \models B_a \varphi$ iff there is a $w' \in W$ such that $w \sim_a w'$ and $\mathcal{M}, w' \models \varphi$.

Note that the semantic interpretation of the Boolean connectives in $\mathcal{E}(\mathcal{L})$ coincides
with the corresponding ones of the base logic $\mathcal{L}$.

Beyond of the Epistemisation of Propositional Logic $\mathcal{E}(\mathcal{PL})$, that captures the stan-
dard Epistemic Logic, we recall here a non standard epistemic logic obtained with this
method:

*Example 1.* Let us present the ‘epistemisation’ of equational logic, the logic $\mathcal{E}(\mathcal{EQ})$. For that we consider a similar game of the classic envelops example from [5] (see also [19]). From the four algebras (in a signature with a binary symbol $\odot$, an unary operation symbol *inv* and a constant symbol *e*) depicted in the model $\mathcal{N}$ represented below, one algebra is chosen. There are three players, Ana, Bob and Clara represented by the symbols *a*, *b* and *c*, that have some information about the chosen algebra. The epistemic representation of the scenario is depicted in the following diagram:

<figure><img src="image_3.png" /></figure>
The operations of the algebras of the top line are the usual integers sum and product and the respective inverses. The operations of the bottom left algebra are the standard sum and inverse on the cyclic field $\mathbb{Z}_2$. The binary operation $\star$ of the bottom right algebra is defined by

$$ \star(x, y) = \begin{cases} 1 & \text{if } x = 0, y = 1 \\ 0 & \text{otherwise} \end{cases}. $$

The following properties are valid in this model: Ana knows that $\odot$ is associative, expressed by the sentence $K_a((x \odot y) \odot z = x \odot (y \odot z))$; Bob knows that $e$ is a neutral element expressed by $K_b(x \odot e = x \wedge e \odot x = x)$; and finally, Clara knows that every element has an inverse, expressed by the sentence $K_c(x \odot x^{-1} = e \wedge x^{-1} \odot x = e)$.

## 3 Proof Calculus

In order to axiomatize the logic $\mathcal{E}(\mathcal{L})$, it is only necessary to add the epistemic axioms to the axioms of $\mathcal{L}$. This is exactly what the definition 2 does.

**Definition 2.** Hilbert style axioms and rules for $\mathcal{E}(\mathcal{L})$

**Axioms: (Epistemic)**

1. All instantiations of propositional tautologies replacing formulas for propositional symbols,

2. $\vdash K_a(\varphi \rightarrow \psi) \rightarrow (K_a\varphi \rightarrow K_a\psi)$,

3. $\vdash K_a\varphi \rightarrow \varphi$,

4. $\vdash K_a\varphi \rightarrow K_a K_a\varphi$ (+ introspection),

5. $\vdash \neg K_a\varphi \rightarrow K_a \neg K_a\varphi$ (- introspection),

6. $\vdash C_G\varphi \leftrightarrow E_G C_G\varphi$

7. $\vdash C_G(\varphi \rightarrow E_G\varphi) \rightarrow (\varphi \rightarrow C_G\varphi)$

(Local) $\vdash \varphi$, for all $\phi \in \text{Fm}_{\mathcal{L}}$ s.t. $\vdash_{\mathcal{L}} \varphi$

**Rules:**

(MP) If $\vdash \varphi \rightarrow \psi$ and $\vdash \varphi$ then $\vdash \psi$

(Gen) If $\vdash \varphi$ then $\vdash K_a\varphi$

The consequence relation $\Gamma \vdash \varphi$ is defined as usual (cf. [11]).

Axioms 2, 3, 4 and 5 are the standard S5 axioms. Axioms 6 and 7 are the well-known Segeberg axioms. They are called induction axioms. They define the common knowledge operator as reflexive transitive closure of the everybody knowledge.

Next, we will discuss the conditions under which the generated calculus $\vdash^{\mathcal{E}(\mathcal{L})}$ is sound and complete.

As expected, the soundness of the base calculus $\vdash_{\mathcal{L}}$ implies the soundness of $\vdash^{\mathcal{E}(\mathcal{L})}$. The proof is achieved by induction. The atomic case is exactly the soundness of the base calculus, and the induction steps are analogous to the ones of $\mathcal{E}$. Hence, whenever $\mathcal{L}$ is sound, we have:

**Theorem 1.** Let $\mathcal{L}$ be a sound knowledge framework. Then, for any formula $\varphi \in \text{Fm}_{\mathcal{E}(\mathcal{L})}$,

$$ \vdash^{\mathcal{E}(\mathcal{L})} \varphi \text{ implies } \models^{\mathcal{E}(\mathcal{L})} \varphi $$
**3.1 Completeness**

We are going to prove completeness using Fisher and Ladner constructions ([9]), because we are interested in studying the model checking problem of our resulting logics.

In this section, we use the abbreviations $D_G\varphi \equiv \neg C_G\neg\varphi$ and $F_G\varphi \equiv \neg E_G\neg\varphi$. They are the duals of the common knowledge operator, $C_G$, and the everybody in the group $G$ know operator $E_G$ respectively.

The canonical model construction for $\mathcal{E}(\mathcal{L})$ follows the same steps of the construction of the canonical model for Propositional Dynamic Logic [4, 11, 18]. Next, we define the Fischer and Ladner Closure, which is a set of (sub-)formulae that are used to build the canonical model.

**Definition 3.** (Fischer and Ladner Closure): Let $\Gamma$ be a set of formulas, $G = \{a_1, \dots, a_n\}$ be a finite set of agents. The closure of $\Gamma$, notation $C_{FL}(\Gamma)$, is the smallest set of formulas satisfying the following conditions:

1. $C_{FL}(\Gamma)$ is closed under subformulas,

2. if $D_G\varphi \in C_{FL}(\Gamma)$, then $F_G D_G\varphi \in C_{FL}(\Gamma)$,

3. if $F_G\varphi \in C_{FL}(\Gamma)$, then $B_{a_1}\varphi \lor \dots \lor B_{a_n}\varphi \in C_{FL}(\Gamma)$,

4. if $\varphi \in C_{FL}(\Gamma)$ and $\varphi$ is not of the form $\neg\psi$, then $\neg\varphi \in C_{FL}(\Gamma)$.

The proof that if $\Gamma$ is a finite set of formulas, then the closure $C_{FL}(\Gamma)$ of $\Gamma$ is also finite, is rather standard and it can be found in the reference [9].

Next definition, introduces the notion of atoms, which are the correspondent of maximal consistent sets in standard canonical model proofs.

**Definition 4.** Let $\Gamma$ be a set of formulas. A set of formulas $\mathcal{A}$ is said to be an **atom of** $\Gamma$ if it is a maximal consistent subset of $C_{FL}(\Gamma)$. The set of all atoms of $\Gamma$ is denoted by $At(\Gamma)$.

We need to guarantee that for every consistent set of formulas, we can build an atom which contains it.

**Lemma 3.** Let $\Gamma$ be a finite set of formulas. If $\psi \in C_{FL}(\Gamma)$ and $\psi$ is consistent then there exists an atom $\mathcal{A} \in At(\Gamma)$ such that $\psi \in \mathcal{A}$.

*Proof.* We can construct the atom $\mathcal{A}$ as follows. First, we enumerate the elements of $C_{FL}(\Gamma)$ as $\varphi_1, \dots, \varphi_n$. We start the construction making $\mathcal{A}_1 = \{\psi\}$, then for $1 < i < n$, we know that $\vdash \bigwedge \mathcal{A}_i \leftrightarrow (\bigwedge \mathcal{A}_i \wedge \varphi_{i+1}) \lor (\bigwedge \mathcal{A}_i \wedge \neg \varphi_{i+1})$ is a tautology and therefore either $\mathcal{A}_i \cup \{\varphi_{i+1}\}$ or $\mathcal{A}_i \cup \{\neg \varphi_{i+1}\}$ is consistent. We take $\mathcal{A}_{i+1}$ as the union of $\mathcal{A}_i$ with the consistent member of the previous disjunction. At the end, we make $\mathcal{A} = \mathcal{A}_n$.

For a given set of agents $Ag$, we defined $Ag^* = \{G|G \subseteq Ag\} \cup \{G^*|G \subseteq Ag\}$. The definition of the canonical relation have to consider the three modalities patterns:
**Definition 5.** Let $\Gamma \subseteq \mathrm{Fm}_{\mathcal{E}(\mathcal{L})}$ be finite. The canonical relation over $\Gamma$, $S^{\Gamma}$, is an Ag-family of relations ($S_{\alpha}^{\Gamma} \subseteq \mathrm{At}(\Gamma) \times \mathrm{At}(\Gamma))_{\alpha \in \mathrm{Ag}^{*}$ defined, for each $\alpha \in \mathrm{Ag}^{*}$, as follows:

If $\alpha = a \in \mathrm{Ag}$

$$ \mathcal{A}S_a^{\Gamma} \mathcal{B} \text{ iff } \bigwedge \mathcal{A} \wedge B_a \bigwedge \mathcal{B} \text{ is consistent.} \quad (7) $$

If $\alpha = G \subseteq \mathrm{Ag}$

$$ \mathcal{A}S_a^{\Gamma} \mathcal{B} \text{ iff } \bigwedge \mathcal{A} \wedge E_G \bigwedge \mathcal{B} \text{ is consistent.} \quad (8) $$

If $\alpha = G^{*}$ for some $G \subseteq \mathrm{Ag}$

$$ \mathcal{A}S_a^{\Gamma} \mathcal{B} \text{ iff } \bigwedge \mathcal{A} \wedge C_G \bigwedge \mathcal{B} \text{ is consistent.} \quad (9) $$

In order to introduce a notion of canonical model for $\mathcal{E}(\mathcal{L})$, next lemma states that for any $\mathcal{E}(\mathcal{L})$-consistent set of formulas $\Gamma \subseteq \mathrm{Fm}_{\mathcal{E}(\mathcal{L})}$, the subset $\Gamma_L \subseteq \Gamma$ of the $\mathcal{L}$-formulas of $\Gamma$ is $\mathcal{L}$-consistent. Hence, Lemma 2 assures the existence of a $\mathcal{L}$-model that satisfy it.

**Lemma 4.** Let $\Gamma \subseteq \mathrm{Fm}_{\mathcal{E}(\mathcal{L})}$ be finite and $\Gamma_L = \{\varphi|\varphi \in \Gamma \text{ and } \varphi \in \mathrm{Fm}_L\}$. Then, if $\Gamma$ is $\mathcal{E}(\mathcal{L})$-consistent, $\Gamma_L$ is $\mathcal{L}$-consistent.

*Proof.* Suppose that $\Gamma_L$ is not $\mathcal{E}(\mathcal{L})$-consistent. Hence, there is a $\varphi_L \in \Gamma_L$ such that $\Gamma_L \vdash_L \varphi_L$ and $\Gamma_L \vdash_L \neg \varphi_L$. Hence, we have

$$
\begin{align*}
\Gamma_L \vdash_L \varphi_L &\iff \Gamma_L \models_L \varphi_L && \text{by (4) and (5)} \\
&\iff \models_L \bigwedge \Gamma_L \rightarrow \varphi_L && \text{by 1. of Lemma 1} \\
&\iff \vdash_L \bigwedge \Gamma_L \rightarrow \varphi_L && \text{by (4) and (5)} \\
&\Rightarrow \vdash \bigwedge \Gamma_L \rightarrow \varphi_L && \text{by defn of $\vdash$} \\
&\Rightarrow \Gamma \vdash \varphi_L
\end{align*}
$$

Analogously, from $\Gamma_L \vdash_L \neg \varphi_L$ we obtain $\Gamma \vdash \neg \varphi_L$, contradicting the assumption about the $\mathcal{E}(\mathcal{L})$-consistency of $\Gamma$. Therefore $\Gamma_L$ is $\mathcal{L}$-consistent.

*Remark 1.* Note that as happens for $\mathcal{L}$, $\mathcal{E}(\mathcal{L})$ have semantic conjunction, negation and implication. Hence, Lemma 1 can be enunciated for $\mathcal{E}(\mathcal{L})$. Moreover, due its unicity, these connectives coincide.

Once we have defined atoms and canonical relations, we are ready to define our notion of model.

**Definition 6.** Let $\Gamma$ be a set of formulas, $\mathrm{At}(\Gamma) = \{\mathcal{A}_1, \dots, \mathcal{A}_n\}$. For each $1 \le i \le n$, $\mathcal{A}_i^L = \{\varphi_1^i, \dots, \varphi_{n_i}^i\} \subseteq \mathrm{Fm}_L$ denotes the set of all $\mathcal{L}$-formulas in $\mathcal{A}_i$ and $M_{\mathcal{A}_i^L}$ a $\mathcal{L}$-model that satisfies $\mathcal{A}_i^L$ (cf. Lemma 2). A **canonical model over $\Gamma$ is a tuple**

$$ \mathcal{M}^{\Gamma} = (\mathrm{At}(\Gamma), S^{\Gamma}, M^{\Gamma}) $$

such that $M^{\Gamma}(\mathcal{A}_i) = M_{\mathcal{A}_i^L}$.
Next lemma, ensures that our knowledge modalities are working as expected over canonical models.

**Lemma 5.** Let $\mathcal{A} \in \text{At}(\Gamma)$ and $B_a\varphi \in C_{\text{FL}}(\Gamma)$. Then:

$$B_a\varphi \in \mathcal{A} \text{ iff there exists } \mathcal{B} \in \text{At}(\Gamma) \text{ such that } \mathcal{A}S_a^\Gamma \mathcal{B} \text{ and } \varphi \in \mathcal{B}. \quad (10)$$

*Proof.* $\Rightarrow$: Suppose $B_a\varphi \in \mathcal{A}$. By Definition 4, we have that $\bigwedge \mathcal{A} \wedge B_a\varphi$ is consistent. Using the tautology $\vdash \varphi \leftrightarrow ((\varphi \wedge \phi) \vee (\varphi \wedge \neg\phi))$, we have that either $\bigwedge \mathcal{A} \wedge B_a(\varphi \wedge \phi)$ is consistent or $\bigwedge \mathcal{A} \wedge B_a(\varphi \wedge \neg\phi)$ is consistent. So, by the appropriate choice of $\phi$, for all formulas $\phi \in C_{\text{FL}}$, we can construct an atom $\mathcal{B}$ such that $\varphi \in \mathcal{B}$ and $\bigwedge \mathcal{A} \wedge B_a(\varphi \wedge \bigwedge \mathcal{B})$ is consistent and, by Definition 5, $\mathcal{A}S_a^\Gamma \mathcal{B}$.

$\Leftarrow$: Suppose there is $\mathcal{B}$ such that $\varphi \in \mathcal{B}$ and $\mathcal{A}S_a^\Gamma \mathcal{B}$. Then $\bigwedge \mathcal{A} \wedge B_a \wedge \mathcal{B}$ is consistent and also $\bigwedge \mathcal{A} \wedge B_a\varphi$ is consistent. But $B_a\varphi \in C_{\text{FL}}$ and by maximality $\langle a \rangle\varphi \in \mathcal{A}$.

Next lemma establishes that the canonical relation of a group of agents $G = \{a_1, \dots, a_n\}$ is the union of the canonical relation for each agent $a_i$ in the group in $G$.

**Lemma 6.** Let $\Gamma \subseteq \text{Fm}_\mathcal{E}(\mathcal{L})$ be a finite and $\mathcal{M}^\Gamma = (\text{At}(\Gamma), S^\Gamma, M^\Gamma)$ a canonical model over $\Gamma$. Then, $S_G^\Gamma = S_{a_1}^\Gamma \cup \dots \cup S_{a_n}^\Gamma$, for $G = \{a_1, \dots, a_n\}$.

*Proof.* $\Rightarrow$: Suppose $\mathcal{A}S^\Gamma \mathcal{B}$. This is iff $\bigwedge \mathcal{A} \wedge E_G \wedge \mathcal{B}$ is consistent. By definition $E_G\varphi \equiv B_{a_1}\varphi \vee \dots \vee B_{a_n}\varphi$ and so $\bigwedge \mathcal{A} \wedge B_{a_1} \wedge \mathcal{B} \vee \dots \vee B_{a_n} \wedge \mathcal{B}$ is consistent.

But for at least one $a_i$, $\bigwedge \mathcal{A} \wedge B_{a_i} \wedge \mathcal{B}$ is consistent. And then, $\mathcal{A}S_{a_i}^\Gamma \mathcal{B}$ and thus $\mathcal{A}(S_{a_1}^\Gamma \cup \dots \cup S_{a_n}^\Gamma)\mathcal{B}$.

$\Leftarrow$: Suppose $\mathcal{A}(S_{a_1} \cup \dots \cup S_{a_n})\mathcal{B}$, so for at least one $a_i$, $\mathcal{A}S_{a_i}\mathcal{B}$. This is iff $\bigwedge \mathcal{A} \wedge B_{a_i} \wedge \mathcal{B}$ is consistent. But $\bigwedge \mathcal{A} \wedge B_{a_1} \wedge \mathcal{B} \vee \dots \vee B_{a_n} \wedge \mathcal{B}$ is also consistent. By definition, $E_G\varphi \equiv B_{a_1}\varphi \vee \dots \vee B_{a_n}\varphi$ and so $\bigwedge \mathcal{A} \wedge E_G \wedge \mathcal{B}$ is consistent. Thus, $\mathcal{A}S_G\mathcal{B}$.

Next lemma, ensures that our group modalities are working as expected over canonical models.

**Lemma 7.** Let $\mathcal{A} \in \text{At}(\Gamma)$ and $E_G\varphi \in C_{\text{FL}}(\Gamma)$. Then,

$$E_G\varphi \in \mathcal{A} \text{ iff there exists } \mathcal{B} \in \text{At}(\Gamma) \text{ such that } \mathcal{A}S_G\mathcal{B} \text{ and } \varphi \in \mathcal{B}. \quad (11)$$

*Proof.* $\Leftarrow$: Suppose there exists $\mathcal{B} \in \text{At}(\Gamma)$ such that $\mathcal{A}S_G\mathcal{B}$ and $\varphi \in \mathcal{B}$. By Lemma 6, there exists $\mathcal{B} \in \text{At}(\Gamma)$ such that $(S_{a_1}^\Gamma \cup \dots \cup S_{a_n}^\Gamma)$ and $\varphi \in \mathcal{B}$. So for at least one $a_i$, there exists $\mathcal{B} \in \text{At}(\Gamma)$ such that $\mathcal{A}S_{a_i}^\Gamma \mathcal{B}$ and $\varphi \in \mathcal{B}$. By Lemma 5, $B_{a_i}\varphi \in \mathcal{A}$ and also $B_{a_1}\varphi \vee \dots \vee B_{a_i}\varphi \vee \dots \vee B_{a_n}\varphi \in \mathcal{A}$. By definition, $E_G\varphi \equiv B_{a_1}\varphi \vee \dots \vee B_{a_n}\varphi$. Thus, $E_G\varphi \in \mathcal{A}$.

$\Rightarrow$: Suppose $E_G\varphi \in \mathcal{A}$. Then, By definition $E_G\varphi \equiv B_{a_1}\varphi \vee \dots \vee B_{a_n}\varphi$, and so, by the definition of the closure, $B_{a_1}\varphi \vee \dots \vee B_{a_n}\varphi \in \mathcal{A}$. But for at least one $a_i$, $B_{a_i}\varphi \in \mathcal{A}$.
By Lemma 5, there exists $\mathcal{B} \in \text{At}(\Gamma)$ such that $\mathcal{A}S_{a_i}^{\Gamma}\mathcal{B}$ and $\varphi \in \mathcal{B}$. And also, there exists $\mathcal{B} \in \text{At}(\Gamma)$ such that $\mathcal{A}(S_{a_1}^{\Gamma} \cup \cdots \cup S_{a_n}^{\Gamma})\mathcal{B}$ and $\varphi \in \mathcal{B}$. By lemma 6, there exists $\mathcal{B} \in \text{At}(\Gamma)$ such that $\mathcal{A}S_G^{\Gamma}\mathcal{B}$ and $\varphi \in \mathcal{B}$.

This lemma, ensures that our common knowledge modalities are working as expected over canonical models.

**Lemma 8.** Let $\mathcal{A}, \mathcal{B} \in \text{At}(\Gamma)$ and $G \subseteq \text{Ag}$. Then,

$$ \text{if } \mathcal{A}S_{G^*}^{\Gamma}\mathcal{B}, \text{ then } \mathcal{A}S_G^{\Gamma^*}\mathcal{B}. \qquad (12) $$

*Proof.* Suppose $\mathcal{A}S_{G^*}^{\Gamma}\mathcal{B}$. Let $\mathbf{C} = \{\mathcal{C} \in \text{At}(\Gamma) \mid \mathcal{A}S_{G^*}^{\Gamma}\mathcal{C}\}$. We want to show that $\mathcal{B} \in \mathbf{C}$. Let $\mathbf{C}_{\downarrow}^{\wedge} = (\bigwedge C_1 \vee \cdots \vee \bigwedge C_n)$, where $C_i \in \mathbf{C}$ for $1 \le i \le n$, be the disjunction of the conjunctions of the atoms in $\mathbf{C}$.

It is true that $\mathbf{C}_{\downarrow}^{\wedge} \wedge E_G \neg \mathbf{C}_{\downarrow}^{\wedge}$ is inconsistent, otherwise for some $\mathcal{D}$ not reachable from $\mathcal{A}$, $\mathbf{C}_{\downarrow}^{\wedge} \wedge E_G \wedge \mathcal{D}$ would be consistent, and for some $C_i \in \mathbf{C}$, $\bigwedge C_i \wedge E_G \wedge \mathcal{D}$ was also consistent, which would mean that $\mathcal{D} \in \mathbf{C}$, which is not the case. From a similar reasoning we know that $\bigwedge \mathcal{A} \wedge E_G \neg \mathbf{C}_{\downarrow}^{\wedge}$ is also inconsistent and hence $\vdash \bigwedge \mathcal{A} \rightarrow F_G \mathbf{C}_{\downarrow}^{\wedge}$ is a theorem.

As $\mathbf{C}_{\downarrow}^{\wedge} \wedge E_G \neg \mathbf{C}_{\downarrow}^{\wedge}$ is inconsistent, so its negation is a theorem $\vdash \neg(\mathbf{C}_{\downarrow}^{\wedge} \wedge E_G \neg \mathbf{C}_{\downarrow}^{\wedge})$ and also $\vdash (\mathbf{C}_{\downarrow}^{\wedge} \rightarrow F_G \mathbf{C}_{\downarrow}^{\wedge})$ (1), applying generalization $\vdash D_G(\mathbf{C}_{\downarrow}^{\wedge} \rightarrow F_G \mathbf{C}_{\downarrow}^{\wedge})$. Using Segerberg axiom (axiom 6), we have $\vdash (F_G \mathbf{C}_{\downarrow}^{\wedge} \rightarrow D_G \mathbf{C}_{\downarrow}^{\wedge})$ and by (1) we obtain $\vdash (\mathbf{C}_{\downarrow}^{\wedge} \rightarrow D_G \mathbf{C}_{\downarrow}^{\wedge})$. As $\vdash \bigwedge \mathcal{A} \rightarrow F_G \mathbf{C}_{\downarrow}^{\wedge}$ is a theorem, then $\vdash \bigwedge \mathcal{A} \rightarrow D_G \mathbf{C}_{\downarrow}^{\wedge}$. By supposition, $\bigwedge \mathcal{A} \wedge C_G \wedge \mathcal{B}$ is consistent and so is $\bigwedge \mathcal{B} \wedge \mathbf{C}_{\downarrow}^{\wedge}$. Therefore, for at least one $C \in \mathbf{C}$, we know that $\bigwedge \mathcal{B} \wedge \bigwedge \mathbf{C}$ is consistent. By maximality, we have that $\mathcal{B} = \mathbf{C}$. And by the definition of $\mathbf{C}_{\downarrow}^{\wedge}$, we have $\mathcal{A}S_G^{\Gamma^*}\mathcal{B}$.

Below, we define our notion of standard models, which are the expected desired models.

**Definition 7.** Let $\Gamma \subseteq \text{Fm}_{\mathcal{E}}(\mathcal{L})$ be finite. A standard model over $\Gamma$ is the tuple $\mathcal{M}^{\Gamma} = (\text{At}(\Gamma), R, M^{\Gamma})$, where

- $R = (R_{\alpha} \subseteq W \times W)_{\alpha \in \text{Ag}^*}$ defined as follows:

$$ R_a = S_a^{\Gamma}; $$

$$ R_G = R_{a_1} \cup \cdots \cup R_{a_n}, \text{ for } G = \{a_1, \ldots, a_n\}; $$

$$ R_{G^*} = R_G^*. $$

- $M^{\Gamma}(\mathcal{A}) = M_{\mathcal{A}^{\mathcal{L}}}$

This lemma establishes the canonical model constructed is almost a standard model. But this result is enough to guarantee the construction of the standard canonical model need for the completeness proof.

**Lemma 9.** $S_G^{\Gamma} = R_G$ and $S_{G^*}^{\Gamma} \subseteq R_{G^*}$

*Proof.* This proof is straightforward from Definition 7 and Lemma 6 and Lemma 8.
This lemma ensures that our modalities also are working as expected over standard canonical models.

**Lemma 10 (Existence Lemma).** Let $\mathcal{A} \in \text{At}(\Gamma)$, $G \subseteq \text{Ag}$. Then,

$E_G \varphi \in \mathcal{A}$ iff there exists $\mathcal{B} \in \text{At}(\Gamma)$ such that $\mathcal{A}R_G\mathcal{B}$ and $\varphi \in \mathcal{B}$

and

$C_G \varphi \in \mathcal{A}$ iff there exists $\mathcal{B} \in \text{At}(\Gamma)$ such that $\mathcal{A}R_G\mathcal{B}$ and $\varphi \in \mathcal{B}$.

*Proof.* $\Rightarrow$: it is analogous to the one presented for basic programs in Lemma 5 and the previous Lemma 9 that states that $S_\alpha \subseteq R_\alpha$.

$\Leftarrow$: By induction on the structure of $\alpha$. This proof is rather standard in PDL literature (c.f. [11]).

Now we are in conditions to prove the Truth Lemma for $\mathcal{E}(\mathcal{L})$, a crucial piece to achieve the completeness. It states that for every formula in the closure, it belongs to an atom if and only if it is true at the correspondent state in the standard canonical model.

**Lemma 11 (Truth Lemma).**

Let $\psi \in \text{Fm}_{\mathcal{E}(\mathcal{L})}$ and $M^\psi$ the standard model over $\{\psi\}$. Then, for any $\mathcal{A} \in \text{At}(\{\psi\})$, and for all $\varphi \in C_{\text{FL}}(\psi)$,

$$ \mathcal{M}, \mathcal{A} \models_{\mathcal{E}(\mathcal{L})} \varphi \text{ iff } \varphi \in \mathcal{A}. $$

*Proof.* : The proof is by induction on the construction of $\varphi$.

- For $\mathcal{L}$-formulas the proof is straightforward from the definition of satisfaction and the definition of $\mathcal{M}$.

- For Boolean operators: the proof is straightforward from the definition of satisfaction and the induction hypothesis.

Modality $C_G$:

$\Rightarrow$ Suppose $\mathcal{M}, \mathcal{A} \models_{\mathcal{E}(\mathcal{L})} C_G \varphi$, then there exists $\mathcal{A}'$ such that $\mathcal{A}R_G\mathcal{A}'$ and $\mathcal{M}, \mathcal{A}' \models_{\mathcal{E}(\mathcal{L})} \varphi$. By the induction hypothesis we know that $\varphi \in \mathcal{A}'$, and by Lemma 10 we have $C_G \varphi \in \mathcal{A}$.

$\Leftarrow$ Suppose $\mathcal{M}, \mathcal{A} \not\models_{\mathcal{E}(\mathcal{L})} C_G \varphi$, by the definition of satisfaction we have $\mathcal{M}, \mathcal{A} \models_{\mathcal{E}(\mathcal{L})} \neg C_G \varphi$.

Then for all $\mathcal{A}', \mathcal{A}R_G\mathcal{A}'$ implies $\mathcal{M}, \mathcal{A}' \not\models_{\mathcal{E}(\mathcal{L})} \varphi$. By the induction hypothesis we know that $\varphi \notin \mathcal{A}'$, and by Lemma 10 we have $C_G \varphi \notin \mathcal{A}$.

The proof for the remaining modalities is analogous.

Now, we are ready to prove completeness showing that for every consistent formula we can build a standard canonical model which satisfies it.

Next, we state and prove the completeness theorem.

**Theorem 2 (Completeness).** $\mathcal{E}(\mathcal{L})$ is complete.

*Proof.* For every consistent formula $\varphi$ we can build a model over $\{\varphi\}$, $\mathcal{M}\{\varphi\}$. By Lemma 3, there exists an atom $\mathcal{A} \in \text{At}(\{\varphi\})$ such that $\varphi \in \mathcal{A}$, and by the Truth Lemma 11 $\mathcal{M}\{\varphi\}, \mathcal{A} \models_{\mathcal{E}(\mathcal{L})} \varphi$.
# 4 Model Checking and Satisfiability problem

In this section we are assuming that the model checking problem in $\mathcal{L}$ is decidable and its complexity is $\mathcal{MC}(\mathcal{L})$. We show that the model checking problem for $\mathcal{E}(\mathcal{L})$ is in PTime $\times \mathcal{MC}(\mathcal{L})$. It means that if $\mathcal{L}$ is a logic which the model checking problem is in PTime, then, this problem is also in PTime for $\mathcal{E}(\mathcal{L})$.

**Definition 8.** The model checking problem consist of, given a formula $\varphi$ and a finite $\mathcal{E}(\mathcal{L})$-model $\mathcal{M} = (W, \sim, M)$, determining the set $\mathcal{S}(\varphi) = \{v \in W \mid \mathcal{M}, v \models \varphi\}$

Next, we present the model checking algorithms for our epistemic logic for structured knowledge $\mathcal{E}(\mathcal{L})$ (Algorithm 1). Lets $\text{label}(v)$ denote the set of sub-formulas of $\phi$ that hold at state $v$, for all $v \in W$.

For the implementation of the algorithm CheckDIAM, we will use the notation $\langle x \rangle \varphi_1$, with $x = a, G, G^*$ as follows:

- $B_a\varphi$ is represented by $\langle a \rangle \varphi \equiv \langle \{a\} \rangle \varphi$;

- $F_G\varphi$, with $G = \{a_1, \dots, a_n\}$ is represented by $\langle G \rangle \varphi \equiv \langle a_1 \cup \dots \cup a_n \rangle \varphi$; and

- $C_G\varphi$ is represented by $\langle G^* \rangle \varphi$.

**Theorem 3.** The model-checking problem for $\mathcal{E}(\mathcal{L})$ is linear in the product of the size of the model, the length of the formula and the $\mathcal{MC}(\mathcal{L})$ (the computational complexity of model checking a $\mathcal{L}$ formula).

*Proof.* The algorithm Check_E(L)(φ) is called once for each sub-formula of φ which is O(|φ|) and each time it activates the algorithms Check_L, CheckNOT, CheckAND and CheckDIAM. The later, in worse case, has to search the whole model, this is O(|W| + |∼x|) (for x = a, G, G*), i.e., the order of the size of the model. So, the complexity of Check_E(L)(φ) is O(|φ| × (|W| + |∼x|)) × MC(\L). The algorithms CheckNOT and CheckAND take constant time.

Thus, the complexity of Check_E(L)(φ) is $O(|\phi| \times (|W| + |R_x|) \times \mathcal{MC}(\mathcal{L}))$.

In order to build the set $S(\phi)$ we only need to search $\text{label}(v)$ for all $v \in W$ and check if $\phi \in \text{label}(v)$.

# 5 Conclusion

This work aimed to endow the epistemic logics with structured states, build on the epistemisations method introduced in [19], as tool support. Firstly, a parametric way to define a logic calculus is introduced, on top of a calculus of the base knowledge representation framework. Moreover, we show that the method preserves the completeness of the base calculus under the natural conditions. This result paves the way for the implementation of dedicated theorem provers for specific epistemisations, but also for a parametric proof system, taking as parameter a base calculus. On the other hand, it studied the complexity of the Model Checking and of the SAT problem for generic epistemisations.

This is just part of a research agenda that we intends to pursue, for instance, by extending the calculus generation to other versions of epistemisation, including the variant with public announcement also introduced in the paper [19]. Moreover, as noted
**Algorithm 1 procedure Check.E(L)(φ)**

if φ ∈ L then

Check_L(φ)

end if

while |φ| ≥ 1 do

if φ = (¬φ₁) then

Check.E(L)(φ₁); CheckNOT(φ₁)

else if φ = (φ₁ ∧ φ₂) then

Check.E(L)(φ₁); Check.E(L)(φ₂); CheckAND(φ₁, φ₂)

else if φ = ⟨x⟩φ₁, for x = a, G, G* then

Check_E(L)(φ₁)

CheckDIAM(φ₁, x)

end if

end while

**Algorithm 2 procedure CheckNOT(φ)**

for all v ∈ W do

if φ ∉ label(v) then

label(v) := label(v) ∪ {¬φ}

end if

end for

**Algorithm 3 procedure CheckAND((φ₁ ∧ φ₂)**

for all v ∈ W do

if φ₁ ∈ label(v) and φ₂ ∈ label(s) then

label(v) := label(v) ∪ {(φ₁ ∧ φ₂)}

end if

end for

**Algorithm 4 procedure CheckDIAM(φ₁, x)**

if x = G then

∼x = ∼G = ⋃<sub>a∈G</sub> ∼a

end if

if x = G* then

∼x = (∼G)* = (∪<sub>a∈G</sub> ∼a)*, {where (∼G)* is the reflexive, transitive closure of ∼G.}

end if

T := {v | φ₁ ∈ label(v)} {T is the set of states to be visited.}

while T ≠ ∅ do

choose v ∈ T { v is a state in W where φ₁ holds.}

T := T \ {v}

for all t such that ⟨t, v⟩ ∈∼x, do

if ⟨x⟩φ₁ ∉ label(t) then

label(t) := label(t) ∪ {⟨x⟩φ₁}

end if

end for

end while
in the work [19], this method provide a significant potential on applications to be ex-
plored. For instance, its role in the modelling of an autonomous hybrid system, by
understanding sensors as agents that partially know the state of the system (e.g. some
of them known the vertical acceleration, some other the current position etc.), using as
knowledge representation framework the differential dynamic logic ( [24]), is a line in
our research agenda. There are other interesting extensions. For instance, to derive the
'epistemisation' for probabilistic logic presented in [23] or of fuzzy logics (e.g. [12])
and to analyse their relation with the probabilistic and multi-valued epistemic logics of
the references [2, 17].

Finally, it is worth noting that this work is framed in our long term research on
demand driven generation of specification logics, parametric to the specificities of some
classes of complex systems (e.g. [2, 20, 21]).

Acknowledgement

The first author is also partially supported by the Brazilian research agencies CNPq, CAPES and FAPERJ. Second and third authors are partially supported by the ERDF—European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project POCI-01-0145-FEDER-030947 and by UID/MAT/04106/2019 at CIDMA.

**References**

1. Balbiani, P., Gasquet, O., Schwarzentruber, F.: Agents that look at one another. Logic Journal of the IGPL 21(3), 438–467 (2013). https://doi.org/10.1093/jigpal/jzs052, http://dx.doi.org/10.1093/jigpal/jzs052

2. Benevides, M.R.F., Madeira, A., Martins, M.A.: A family of graded epistemic logics. In: Alves, S., Wasserman, R. (eds.) 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017. Electronic Notes in Theoretical Computer Science, vol. 338, pp. 45–59. Elsevier (2017). https://doi.org/10.1016/j.entcs.2018.10.004, https://doi.org/10.1016/j.entcs.2018.10.004

3. Blackburn, P., ten Cate, B.: Pure Extensions, Proof Rules and Hybrid Axiomatics. In: Schmidt, R., Pratt-Hartmann, I., Reynolds, M., Wansing, H. (eds.) Proceedings of the Advances in Modal Logic 2004 (AiML 2004) (2004)

4. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, UK (2001)

5. van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Synthese Library Series, volume 337, Springer, The Netherland (2008)

6. van Eijck, J., Gattinger, M.: Elements of epistemic crypto logic. In: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems. pp. 1795–1796. AAMAS ’15, International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC (2015), http://dl.acm.org/citation.cfm?id=2772879.2773441
7. van Eijck, J., Gattinger, M., Wang, Y.: Knowing values and public inspection. In: Ghosh, S., Prasad, S. (eds.) Logic and Its Applications. pp. 77–90. Springer Berlin Heidelberg, Berlin, Heidelberg (2017)

8. Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT Press, USA (1995)

9. Fisher, M.J., Ladner, R.F.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18 (1979)

10. Fitting, M., Mendelsohn, R.: First-Order Modal Logic. Synthese Library Studies in Epistemology Logic, Methodology, and Philosophy of Science Volume 277, Springer Netherlands (1998), https://books.google.com.br/books?id=JMV9ZOg3KkUC

11. Goldblatt, R.: Logics of Time and Computation. CSLI Lecture Notes 7, CSLI, Stanford (1992)

12. Hájek, P.: Basic fuzzy logic and bl-algebras. Soft Comput. 2(3), 124–128 (1998). https://doi.org/10.1007/s005000050043, https://doi.org/10.1007/s005000050043

13. Herzig, A., Lorini, E., Maffre, F.: A poor man’s epistemic logic based on propositional assignment and higher-order observation. In: van der Hoek, W., Holliday, W.H., Wang, W.f. (eds.) Logic, Rationality, and Interaction. pp. 156–168. Springer Berlin Heidelberg, Berlin, Heidelberg (2015)

14. Hintikka, J.: Knowledge and Belief. Cornell University Press, Ithaca, N.Y (1962)

15. van der Hoek, W., Iliev, P., Wooldridge, M.: A logic of revelation and concealment. In: International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2012, Valencia, Spain, June 4-8, 2012 (3 Volumes). pp. 1115–1122 (2012), http://dl.acm.org/citation.cfm?id=2343856

16. van der Hoek, W., Troquard, N., Wooldridge, M.: Knowledge and control. In: 10th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2011), Taipei, Taiwan, May 2-6, 2011, Volume 1-3. pp. 719–726 (2011), http://portal.acm.org/citation.cfm?id=2031720\&CFID=54178199\&CFToken=61392764

17. Kooi, B.P.: Probabilistic dynamic epistemic logic. Journal of Logic, Language and Information 12(4), 381–408 (Sep 2003). https://doi.org/10.1023/A:1025050800836, https://doi.org/10.1023/A:1025050800836

18. Kozen, D., Parikh, R.: An elementary proof of the completeness of pdl. Theoretical Computer Science 14, 113–118 (1981)

19. Madeira, A., Martins, M.A., Benevides, M.R.F.: Epistemic logics with structured knowledge. In: Accattoli, B., Olarte, C. (eds.) Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2018, Fortaleza, Brazil, September 26-28, 2018. Electronic Notes in Theoretical Computer Science, vol. 344, pp. 137–149. Elsevier (2018). https://doi.org/10.1016/j.entcs.2019.07.009, https://doi.org/10.1016/j.entcs.2019.07.009

20. Madeira, A., Neves, R., Barbosa, L.S., Martins, M.A.: A method for rigorous design of reconfigurable systems. Sci. Comput. Program. 132, 50–76 (2016). https://doi.org/10.1016/j.scico.2016.05.001, https://doi.org/10.1016/j.scico.2016.05.001

21. Madeira, A., Neves, R., Martins, M.A.: An exercise on the generation of many-valued dynamic logics. J. Log. Algebr. Meth. Program. 85(5), 1011–1037 (2016). https://doi.org/10.1016/j.jlamp.2016.03.004, http://dx.doi.org/10.1016/j.jlamp.2016.03.004

22. Neves, R., Madeira, A., Martins, M.A., Barbosa, L.S.: Proof theory for hybrid(ised) logics. Sci. Comput. Program. 126, 73–93 (2016). https://doi.org/10.1016/j.scico.2016.03.001, https://doi.org/10.1016/j.scico.2016.03.001
23. Nilsson, N.J.: Probabilistic logic. Artif. Intell. **28**(1), 71–88 (Feb 1986).
https://doi.org/10.1016/0004-3702(86)90031-7, http://dx.doi.org/10.1016/
0004-3702(86)90031-7

24. Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Switzerland (2018),
http://www.springer.com/978-3-319-63587-3

25. van Ditmarsch, H., van der Hoek, W., Halpern, J., Kooi, B. (eds.): Handbook of Epistemic Logic. College Publications (2015)

26. Wang, Y.: Beyond Knowing That: A New Generation of Epistemic Logics, pp. 499–533.
Springer International Publishing, Cham (2018). https://doi.org/10.1007/978-3-319-62864-6_21, https://doi.org/10.1007/978-3-319-62864-6\_21